UDC 51.07 : 164

MATHEMATICS

G. E. MINTS

HERBRAND’S THEOREM FOR THE PREDICATE CALCULUS WITH EQUALITY AND FUNCTIONAL SYMBOLS

(Presented by Academician P. S. Novikov on 29 X 1965)

All terms and notation not specially explained are understood in the same way as in (¹). If (P_1,\ldots,P_s) are predicate symbols and (f_1,\ldots,f_r) are functional symbols, then the expression (Eq(=,P_1,\ldots,P_s,f_1,\ldots,f_r)) has the same meaning as in § 73 of (²), i.e., denotes the conjunction of closed formulas expressing reflexivity and transitivity of equality, as well as the possibility of replacing equal objects by one another in any argument places of (P_1,\ldots,P_s,f_1,\ldots,f_r). The expression (Eq(A)) denotes the same as (Eq(=,U)), where (U) is the complete list of predicate and functional symbols occurring in (A). From the known theorems on the relation between derivability in the predicate calculus with equality and in the pure predicate calculus (for example, theorem 41 (c) of (²)) it follows that a formula (A) is derivable in (LK^{=}) if and only if the sequent (Eq(A)\to A) is derivable in (LK).

If (A) is an arbitrary formula, then the formula (\mathfrak{S}(A,x_1,\ldots,x_k)), where (x_1,\ldots,x_k) is the complete list of (A)-positive variables, will be called, following (³), the functional form of the formula (A) and denoted by (\Phi(A)). From theorem 2 of (¹) and the theorem on monotone replacement it follows that a formula is derivable in (LK^{=}) if and only if its functional form is derivable in (LK^{=}).

The main purpose of the present article is to formulate and prove for (LK^{=}) a theorem analogous to Herbrand’s theorem. The proof of this theorem may be of additional interest in view of the fact that, as indicated in (⁴), in Herbrand’s own proof there are quite substantial errors*, and therefore at present there is no constructive proof of Herbrand’s theorem for arbitrary formulas in the literature.

Below we shall describe the operation of an algorithm (R) which constructs, for each pair ((m,A)), where (m) is a natural number and (A) is a formula, the (m)-th reduction (réduite in J. Herbrand’s terminology) of the formula (A). We introduce several auxiliary algorithms useful in what follows. We shall describe their operation only for the case when the last argument (it will always be a formula) contains no positive complexes. In the general case we shall, by definition, regard the result of applying any of these algorithms as unchanged when the last argument is replaced by its functional form. The algorithm (D) assigns to each pair ((m,A)) a list of terms. (D(0,A)) consists of all free variables occurring in (A), and in the case where there are no such variables, of the variable (z_1)**. Every term occurring in (D(m,A)) occurs in (D(m+1,A)). If (f) is a (k)-ary functional sign occurring in (A), and the terms (t_1,\ldots,t_k) occur in (D(m,A)), then (f(t_1,\ldots,t_k)) occurs in (D(m+1,A)). The lexicon of the formula (A) is the union of all the sets (D(m,A)) ((m=0,1,\ldots)) (cf. (³)).

The algorithm (R_1) assigns to each triple ((m,E,A)), where (A) is a formula

* In (⁴) a way of correcting these errors is indicated and a complete proof is announced.

** (z_j) denotes the (j)-th free variable in order.

and (E') is a quasi-formula, a list of quasi-formulas, or a sequent, some quasi-formula (we shall call it the (m)-th quasi-reduction of the expression (E) with respect to (A)) (in the description below it is assumed that (m) and (A) are fixed, and we speak simply of a quasi-reduction). If (E) is a quasi-formula in which no logical connectives occur, then the quasi-reduction of (E) coincides with (E). The quasi-reduction of a conjunction (disjunction, implication, negation) coincides with the conjunction (respectively with the disjunction, implication, negation) of the quasi-reductions. The quasi-reduction of the quasi-formula (\forall x B) coincides with the expression

[
\underset{t\in D(m,A)}{\&}\ [R_1(m,B,A)]^x_t,
]

and the quasi-reduction of the formula (\exists x B) with the expression

[
\underset{t\in D(m,A)}{\vee}\ [R_1(m,B,A)]^x_t .
]

The quasi-reduction of a list of formulas (a sequent) is constructed termwise, i.e., it is a list of formulas (respectively, sequents) composed of the quasi-reductions of the terms.

The expression (R^(m,A)) denotes the same thing as (R_1(m,\Phi(A),A)). Let us note that, if (A) is a reduced formula, then (R^(m,A)) is the disjunction of the lexical examples (see (3)) of the formula (A).

Let (A) be an arbitrary formula, (n) the number of function signs occurring in the functional form of the formula (A) (this includes both the signs occurring in (A) and the signs introduced in passing to the functional form). Let

[
\varphi_1,\ldots,\varphi_n
\tag{1}
]

be a list of arithmetical functions, and for each (i) let the arity (i.e., the number of arguments) of the function (\varphi_i) coincide with the arity of the (i)-th function sign occurring in the functional form of the formula (A). We shall say that the list (1) is a Skolem system of functions for (A) (s.f.S. for (A)) if the following conditions are satisfied: a) if the variable (z_j) occurs in the lexicon of the formula (A), then the value of any function from the list (1), for any set of arguments, is distinct from (j); b) whatever functions (f) and (g) from the list (1) and natural numbers (m_1,\ldots,m_p,s_1,\ldots,s_q) may be, if (f(m_1,\ldots,m_p)=g(s_1,\ldots,s_q)), then (f) coincides with (g) and (m_1=s_1,\ldots,m_p=s_p). If (t) is an arbitrary term belonging to the lexicon of the formula (A), then by the number of the term (t) with respect to the s.f.S. (1) we shall mean the value of the arithmetical term obtained from (t) by replacing all free variables by their indices (i.e., (z_j) by (j)), and all function signs by the corresponding arithmetical functions from the list (1).

We shall assume that some algorithm is fixed which constructs, for each formula (A), some s.f.S. for (A). The result of applying it to (A) will be called the standard s.f.S. for (A).

Let us describe the algorithm (R). Let (A) be an arbitrary formula, (m) a natural number. Write as (r_1,\ldots,r_n) the complete list of terms occurring in (R^(m,A)) and beginning with function signs not occurring in (A) (i.e., with signs used for the construction of the functional form of the formula (A)). The result of applying the algorithm (R) to the pair ((m,A)) is, by definition, the result of replacing in (R^(m,A)) the terms (r_1,\ldots,r_n), respectively, by the variables (z_{k_1},\ldots,z_{k_n}), where for each (i), (k_i) denotes the number of the term (r_i) with respect to the standard s.f.S. for (A).

We shall also consider an algorithm (R^{*}), whose description is obtained from the description of the algorithm (R) if one writes, as (r_1,\ldots,r_n), the complete list of all terms occurring in (R^(m,A)).

The immediate analogue of Herbrand’s theorem for the predicate calculus with equality is the following assertion.

Theorem 1. Whatever the formula (A), for (A) to be derivable in (LK^{=}) (in (LK)) it is necessary and sufficient that, for some (m), the formula (R(m,A)) be derivable in (LK^{=}) (in (LK)).

We shall prove the part of the theorem concerning (LK^{=}) (the part concerning (LK) is easily obtained from it).

Necessity. If (A) is derivable in (LK^{=}), then the sequent (Eq(A)\to A) is derivable in (LK). By the monotone-substitution theorem, the sequent (Eq(A)\to \Phi(A)) is derivable in (LK). Denote by (D) an arbitrary cut-free derivation of the last sequent in (LK). It is always possible to arrange that all terms occurring in (D) belong to the lexicon of the formula (A). Let (m) denote the maximum of the degrees* of the terms occurring in (D). Replace every sequent (T) occurring in (D) by the sequent (R_1(m,T,A)). As a result, axioms pass into axioms, applications of nonquantifier rules pass into applications of the same rules (see the part of the definition of the algorithm (R_1) concerning the signs (\&, \vee, \supset, \neg)), and applications of quantifier rules pass into figures that can be transformed into chains of applications of the rule of introducing (\&) into the antecedent or (\vee) into the succedent. Therefore the figure into which (D) passes can be completed to a proof of the sequent

[
R_1(m,Eq(A),A)\to R_1(m,\Phi(A),A).
\tag{2}
]

By the monotone-substitution theorem, it follows from this that the sequent (Eq(A)\to R^(m,A)) is derivable in (LK) (since (R^(m,A)), by definition, coincides with the succedent of sequent (2)). The sequent (Eq(A)\to R(m,A)) is obtained from the last sequent by replacing terms beginning with function symbols not occurring in (Eq(A)) (i.e., in the “quantifier part” of the last sequent) by variables, and therefore is derivable in (LK). The sequent (Eq(R(m,A))\to R(m,A)) is obtained from this by refinement. Therefore the formula (R(m,A)) is derivable in (LK^{=}).

Sufficiency. Suppose (R(m,A)) is derivable in (LK^{=}). Then, by the substitution rule in place of free variables, (R^*(m,A)) is derivable. By the monotone-substitution theorem, (\Phi(A)) is derivable, whence it follows that (A) is derivable.

Theorem 2. Whatever the formula (A), for (A) to be derivable in (LK^{=}) (in (LK)) it is necessary and sufficient that, for some (m), the formula (R^*(m,A)) be derivable in (LK^{=}) (respectively in (LK)).

Necessity follows from Theorem 1, and sufficiency from the monotone-substitution theorem.

Theorem 3. Whatever the formula (A), for (A) to be derivable in (LK) it is necessary and sufficient that, for some (m), the formula (R^{**}(m,A)) be derivable in (LK).

The proof is completely analogous to the proof of Theorem 1.

As consideration of the formula (a=b\supset f(a)=f(b)) shows, the assertion obtained from Theorem 3 by replacing (LK) with (LK^{=}) is false. Theorem 3 coincides with Herbrand’s theorem. If the formula (A) contains no function symbols, then (R^{**}(m,A)) coincides with (R(m,A)). Therefore Theorem 3 carries over verbatim to formulas with equality but without function symbols. In the author’s opinion, the most natural version of Herbrand’s theorem for predicate calculus with function symbols is Theorem 2.

Leningrad Branch
of the V. A. Steklov Mathematical Institute
Academy of Sciences of the USSR

Received
7 X 1965

CITED LITERATURE

1. G. E. Mints, DAN, 169, No. 1 (1966).
2. S. K. Kleene, Introduction to Metamathematics, Moscow, 1957.
3. W. V. Quine, J. Symbolic Logic, 20, 2, 141 (1955).
4. V. Dreben, P. Andrews, S. Aanderaa, Bull. Am. Math. Soc., 69, 699 (1963).
5. J. Herbrand, Recherches sur la théorie de la démonstration, Warsaw, 1930.

* The degree of a free variable is (0). The degree of the term (f(t_1,\ldots,t_k)) is one greater than the maximum of the degrees of the terms (t_1,\ldots,t_k).