Syntax

Definition 4.1 (Alphabet of a First-Order Language)   The alphabet of a first-order language contains, first, a set of non-logical symbols that are part of every such language, namely,

• $v_1, v_2, v_3, \ldots$ (variables);
• $\neg, \vee, \wedge, \rightarrow, \leftrightarrow$ (truth-functional connectives);
• $\forall, \exists$ (quantifiers);
• = (equality symbol);
• (, ) (parentheses);

The alphabet for a first-order language also includes the symbols that vary from language to language. Let us call such a set a symbol set, and denote it by S; it contains the following.

• for each $n \in$ N, a (possibly empty) set of n-ary relation symbols;
• for each $n \in$ N, a (possibly empty) set of n-ary function symbols;
• a (possibly empty) set of constants.

The specification of S constitutes the creation of a first-order language for a particular purpose. The HYPERPROOF system reflects a particular $S^{\mbox{{\tiny {\sc Hyperproof}}}}$. For example, the relation symbol Between is an element of $S^{\mbox{{\tiny {\sc Hyperproof}}}}$.

Definition 4.2 (Terms)   Terms are those strings that can be obtained by finitely many applications of the following rules.

• variables are terms;
• constants are terms;
• If $t_1, \ldots, t_n$ are terms, and f is an n-ary function symbol, then $f t_1 \dots t_n$ is a term.

It is easy and useful to associate with every term t the set of variables occurring in it by way of the function var.

Definition 4.3 (Variables in Terms)   The function is defined by three cases:

var(x) = {x}

var(c) = $\emptyset$

var $(f t_1 \dots t_n)$ = var(t₁) $\cup \cdots \cup$ var(t_n)

Definition 4.4 (Formulas)   Formulas are those strings that can be obtained by finitely many applications of the following rules.

• If t₁ and t₂ are terms, then t₁ = t₂ is a formula.
• If R is an n-ary relation symbols, and $t_1, \ldots, t_n$ are terms, then $R t_1 \ldots t_n$ is a fomula.
• If $\phi$ is a wff, then so is $\neg\phi$.
• If $\phi$ and $\psi$ are wffs, then the following are wffs as well:
  • $\phi \vee \psi$
  • $\phi \wedge \psi$
  • $\phi \rightarrow \psi$
  • $\phi \leftrightarrow \psi$

Within a formula, some variables are bound, and some are free. Intuitively, free variables are those that are not associated with any quantifier, and bound variables are those that are. The formal definition of the set of free variables in a given formula $\phi$, which we denote by free($\phi$), follows.

Definition 4.5 (Free Variables)   The definition is an inductive one based on six cases:

free(t₁ = t₂) = var(t₁) $\cup$ var(t₂)

free $(R t_1 \cdots t_n) =$ var $(t_1) \cup \cdots \cup$ var(t_n)

free$(\neg \phi)$ = free$(\phi)$

free $((\phi \ast \psi))$ = free$(\phi)$ $\cup$ free$(\psi)$ where $\ast = \vee, \wedge, \rightarrow, \leftrightarrow$

free $(\forall x \phi)$ = free $(\phi) - \{x\}$

free $(\exists x \phi)$ = free $(\phi) - \{x\}$