582 Mathematical Logic

The completeness of the axioms of the functional calculus of logic¹

KURT GÖDEL n/a

(1930a)

1930a *Die Vollständigkeit der Axiome des logischen Funktionenkalküls, Monatshefte für Mathematik und Physik 37, 349–360 (582–591 of the present volume).

In his doctoral dissertation at the University of Vienna (1930)^a Gödel proved that the predicate calculus of first order is complete, in the sense that every valid formula is provable. The present paper is a rewritten version of this dissertation.

At the beginning of the paper Gödel mentions Whitehead and Russell’s method of deriving logic and mathematics from axioms by means of purely formal rules, and he writes: "Of course, when such a procedure is followed the question at once arises whether the initially postulated system of axioms and principles of inference is complete". One must acknowledge that Whitehead and Russell had not shown much concern for that problem, any more than they did in general for questions that, being semantic in character, went beyond provability in their system.

The statement that the pure predicate calculus of first order is complete, that is, that every valid formula is provable, is equivalent to the statement that every formula is either refutable or satisfiable.

Gödel actually proves a stronger statement, namely, that every formula is either refutable or Hence his proof yields, besides completeness, the Löwenheim-Skolem theorem, which states that a satisfiable formula is The proof makes use of a number of devices introduced by Löwenheim (1915) and Skolem (1920; see also 1922, 1928, and 1929) but contains a step (Theorem VI) through which semantic arguments are connected with provability in a definite system. At about the same time, Herbrand, too, was expanding Löwenheim’s and Skolem’s work; the relation between Gödel’s methods and results and those of Herbrand (1930) was brought out by Dreben (1952; see also above, pp. 510 and 579). Gödel generalizes his result—that every formula is either refutable or satisfiable—in two directions, to the predicate calculus of first order with identity (in which some irrefutable formulas are finitely satisfiable without being and to infinite sets of formulas. The second generalization (Theorem IX) is derived from the result now known as the finiteness, or compactness, theorem (Theorem X), of which Gödel gives a semantic proof.

By using the procedure of arithmetization introduced by Gödel in another paper (1931), Hilbert and Bernays (1939, pp. 205–253) were able to give what they call a "proof-theoretic" version of Gödel’s completeness theorem: if a formula is irrefutable in the pure predicate calculus of first order, it is irrefutable 583 also in every consistent system S that remains consistent when the axioms of number theory, as well as any verifiable formulas of the theory, are added to the axioms of S (p. 252; see also Theorem 36 in Kleene 1952, p. 395).

This proof-theoretic form of Gödel’s completeness theorem was extended to the case of infinitely many formulas by Wang (1951; see also 1950, p. 449, Theorem 5, and 1962, pp. 345–352) and modified so as to give a sharp form of the Löwenheim-Skolem theorem. If Con(Σ) is the usual formula expressing the consistency of a first-order system Σ, the result, called Bernays’s lemma by Wang, says that, if we add Con(Σ) to number theory as a new axiom, we can prove in the resulting system arithmetic translations of all theorems of Σ. This lemma has been applied in several directions (see, for instance, Wang 1952 and 1955).

The Löwenheim-Skolem theorem shows that, if the predicates assigned to predicate letters in accordance with the definition of validity are just number-theoretic predicates, the class of formulas that turn out to be always true coincides with the class of valid formulas. Kleene (1952, pp. 394–395), making explicit some results obtained by Hilbert and Bernays in their arithmetization of Gödel’s completeness proof, showed that the predicates can be further restricted to the class (in the hierarchy of arithmetic predicates). Putnam (1961 and 1965) refined Kleene’s result; he restricted the predicates to the class the smallest class that contains the recursively enumerable predicates and is closed under truth functions; earlier Kreisel (1953) and Mostowski (1955) had shown that the predicates could not be restricted to the class of recursive predicates, and Putnam (1956) that they could not be restricted to the class

Another proof of the completeness of first-order logic, along lines somewhat different from those of Gödel’s proof, was given by Henkin (1949).

The translation is by Stefan Bauer-Mengelberg, and it is printed here with the kind permission of Professor Gödel and Springer Verlag.

Whitehead and Russell, as is well known, constructed logic and mathematics by initially taking certain evident propositions as axioms and deriving the theorems of logic and mathematics from these by means of some precisely formulated principles of inference in a purely formal way (that is, without making further use of the meaning of the symbols). Of course, when such a procedure is followed the question at once arises whether the initially postulated system of axioms and principles of inference is complete, that is, whether it actually suffices for the derivation of every true logico-mathematical proposition, or whether, perhaps, it is conceivable that there are true propositions (which may even be provable by means of other principles) that cannot be derived in the system under consideration. For the formulas of the propositional calculus the question has been settled affirmatively; that is, it has been shown² that every true formula of the propositional calculus does indeed follow from the axioms given in Principia mathematica. The same will be done here for a wider realm of formulas, namely, those of the "restricted functional calculus";³ that is, we shall prove

584

THEOREM I. Every valid⁴formula of the restricted functional calculus is provable. We lay down the following system of axioms⁵ as a basis:

Undefined primitive notions:

and (x). (By means of these, &, → ~, and (Ex) can be defined in a well-known way.)

Formal axioms:

Rules of inference:⁶

1. The inferential schema: From A and B may be inferred;

2. The rule of substitution for propositional and functional variables;

3. From A(x), (x)A(x) may be inferred;

4. Individual variables (free or bound) may be replaced by any others, so long as this does not cause overlapping of the scopes of variables denoted by the same sign. For what follows, it will be expedient to introduce some abbreviated notations.

(P), (Q), (R), and so on mean prefixes constructed in any way whatever, that is, finite sequences of signs of the form (x)(Ey), (y)(x)(Ez)(u), and the like.

Lower-case German letters, and so on, mean n-tuples of individual variables, that is, sequences of signs of the form x, y, z, or x₂, x₁, x₂, x₃, and the like, where the same variable may occur several times. The signs and so on are to be understood accordingly. Should a variable occur several times in we must, of course, think of it as written only once in or

Furthermore we require a number of lemmas, which are collected here. The proofs are not given, since they are in part well known, in part easy to supply.

1. For every n-tuple

are provable.

2. If and differ only in the order of the variables, then

is provable.

585

3. If consists entirely of distinct variables and if has the same number of terms as then

is provable, even when a number of identical variables occur in

4. If (p_i) means one of the prefixes (x_i) or (Ex_i) and if (q_i) means one of the prefixes (y_i) or (Ey_i), then

is provable⁷ for every prefix (P) that is formed from the (p_i) and the (q_i) and satisfies the condition that, for precedes (p_k) and, for precedes (q_k).

5. Every expression can be brought into normal form; that is, for every expression A there is a normal formula N such that is provable.⁸

6. If is provable, so is where represents an arbitrary expression containing A as a part (see Hilbert and Ackermann 1928, chap. 3, § 7).

7. Every valid formula of the propositional calculus is provable; that is, Axioms 1–4 form a complete axiom system for the propositional calculus.⁹

We now proceed to the proof of Theorem I and first note that the theorem can also be stated in the following form:

THEOREM II. Every formula of the restricted functional calculus is either refutable¹⁰or satisfiable (and, moreover, satisfiable in the denumerable domain of individuals).

That I follows from II can be seen as follows: Let A be a valid expression; then is not satisfiable, hence according to II it is refutable; that is, is provable and, consequently, so is A. The converse is as apparent.

We now define a class of expressions K by means of the following stipulations:

1. K is a normal formula;

2. K contains no free individual variable;

3. The prefix of K begins with a universal quantifier and ends with an existential quantifier.

Then we have

THEOREM III. If every is either refutable or satisfiable,¹¹so is every expression.

Proof. Let A be an expression not belonging to Let it contain the free variables As is immediately obvious, the refutability of follows from that of A, and conversely (by Lemma 1(c), and either Rule of inference 3 or, for the converse, Axiom 5); the same holds, according to the stipulation in footnote 4, for satisfiability. Let (P)N be the normal form of so that

586

is provable. Further let

¹²

Then

is provable (on the basis of Lemma 4 and the provability of B belongs to and thus according to the assumption is either satisfiable or refutable. But, by (1) and (2), the satisfiability of B entails that of hence also that of A; the same holds for refutability. Thus A, too, is either satisfiable or refutable.

Because of Theorem III, therefore, it suffices to show that

Everyis either satisfiable or refutable.

For this purpose we define the degree of a ¹³ to be the number of blocks in its prefix that consist of universal quantifiers and are separated from each other by existential quantifiers, and we first prove

THEOREM IV. If every expression of degree k is either satisfiable or refutable, so is every expression of degree

Proof. Let (P)A be a of degree Let and let where (Q) is of degree k and (R) of degree Further let F be a functional variable not occurring in A. If we now put¹⁴

and

¹⁵

then a double application of Lemma 4 in combination with Lemma 6 yields the provability of

furthermore,

is obviously valid. Now C is of degree k and by assumption is therefore either satisfiable or refutable. If it is satisfiable, so is (P)A (by (3) and (4)). If it is refutable, so is B (by (3)); that is, is then provable. In that case, if we substitute (Q)A for F in it follows that

is provable.

But since, of course

is provable, so is that is, in that case (P)A is refutable. (P)A is therefore indeed either refutable or satisfiable.

587

It now remains only to prove

THEOREM V. Every formula of degree 1 is either satisfiable or refutable.

A few definitions are required for the proof. Let (abbreviated as (P)A) be any formula of degree 1. Let stand for an r-tuple and for an s-tuple of variables. We think of the r-tuples taken from the sequence as forming a sequence ordered according to increasing sum of the subscripts [and for equal sums according to some convention]:

and so forth; we now define a sequence {A_n } of formulas derived from (P)A as follows:

Let the s-tuple be denoted by so that we have

Further we define (P_n)A_n by the stipulation

As we can easily convince ourselves, it is precisely the variables x_o to x_ns that occur in A_n; hence they all are bound by (P_n). Further it is apparent that the variables of the r-tuple already occur in (P_n) (and therefore certainly differ from those occurring in ). Denote by what remains of (P_n) when the variables of the r-tuple are omitted, so that, except for the order of the variables,

This notation once assumed, we have

THEOREM VI. For every n

is provable.

For the proof we use mathematical induction.

I. is provable, for we have

(by Lemma 3 and Rule of inference 4) and

(by Lemma 1(a)).

II. For every n, (P)A & is provable, for we have

(by Lemma 3 and Rule of inference 4) and

588

(by Lemma 2). Furthermore,

(by Lemma 1(b) with the substitutions for F and for G).

If we observe that the antecedent of the implication (8) is the conjunction of the consequents of (6) and (7), it is clear that

is provable. Furthermore, from (5) and Lemmas 4, 6, and 2 the provability of

follows. II follows from (9) and (10), and from II, together with I, Theorem VI follows.

Assume that the functional variables and the propositional variables X₁, occur in A. Then A_n consists of elementary components of the form

compounded solely by means of the operations and With each A_n we associate a formula B_n of the propositional calculus by replacing the elementary components of A_n by propositional variables, making certain that different components (even if they differ only in the notation of the individual variables) are replaced by different propositional variables. Furthermore, we understand by "satisfying system of level n [Erfüllungssystem n-ter Stufe] of (P)A" a system of functions defined in the domain of integers z as well as of truth values for the propositional variables X₁, such that a true proposition results if in A_n the F_i arc replaced by the the x_i by the numbers i, and the X_i by the corresponding truth values Satisfying systems of level n obviously exist if and only if B_n is satisfiable.

Each B_n, being a formula of the propositional calculus, is either satisfiable or refutable (Lemma 7). Thus only two cases are conceivable:

1. At least one B_n is refutable. Then, as we can easily convince ourselves (Rules of inference 2 and 3, Lemma 1(c)), the corresponding (P_n)A_n is refutable also, and consequently, because of the provabitity of so is (P)A.

2. No B_n is refutable; hence all are satisfiable. Then there exist satisfying systems of every level. But, since for each level there is only a finite number of satisfying systems (because the associated domains of individuals are finite) and since furthermore every satisfying system of level contains one of level n as a part¹⁶ (as is clear from the fact that the An are formed by successive conjunctions), it follows by 589 familiar arguments^16a that in this case there exists a sequence of satisfying systems (S_k being of level k) such that each contains the preceding one as a part. We now define in the domain of all integers a system by means of the following stipulations:

1. holds if and only if for at least one S_m of the sequence above (and then for all subsequent ones also) holds;

2. for at least one S_m (and then also for all those that follow).

Then it is evident at once that S makes the formula (P)A true. In this case, therefore, (P)A is satisfiable, which concludes the proof of the completeness of the system of axioms given above. Let us note that the equivalence now proved, "valid = provable", contains, for the decision problem, a reduction of the nondenumerable to the denumerable, since "valid" refers to the nondenumerable totality of functions, while "provable" presupposes only the denumerable totality of formal proofs.

Theorem I, as well as Theorem II, can be generalized in various directions. First, it is easy to bring the notion of identity (between individuals) into consideration by adding to Axioms 1–6 above two more:

An analogue of what we had above now holds for the extended realm of formulas too:

THEOREM VII. Every formula of the extended realm is provable if it is valid (more precisely, if it is valid in every domain of individuals), and, equivalent to VII, THEOREM VIII. Every formula of the extended realm is either refutable or satisfiable (and, moreover, satisfiable in a finite or denumerable domain of individuals).

For the proof, let A denote an arbitrary formula of the extended realm. We construct a formula B as the product (conjunction) of A, and all the formulas that we obtain from Axiom 8 by substituting for F the functional variables occurring in A, that is, more precisely,

for all singulary functional variables of A,

for all binary functional variables of A (including "=" itself), and corresponding formulas for the n-ary functional variables of A for which Let B′ be the formula resulting from B when the sign "=" is replaced by a functional variable G not otherwise occurring in B. Then the sign "=" no longer occurs in the expression B′, which, therefore, according to what was proved above, is either refutable or satisfiable. If it is refutable, so is B, since it results from B′ through the substitution of "=" for G. But B is the logical product of A and a subformula that is obviously provable from Axioms 7 and 8. In this case, therefore, A is also refutable. Let us now assume that B′ is satisfiable in the denumerable domain X of individuals for a certain system S of functions.¹⁷ From the way in which B′ is formed it is clear that g (that is, 590 the function of the system S that is to be substituted for G) is a reflexive, symmetric, and transitive relation; hence it generates a partition of the elements of Σ, in such a way, moreover, that a function occurring in the system S continues to hold, or not to hold, as the case may be, when elements of the same class are substituted for one another. If, therefore, we identify with one another all elements belonging to the same class (perhaps by taking the classes themselves as elements of a new domain of individuals), then g goes over into the identity relation and we have a satisfying system of B, hence also of A. Consequently, A is indeed either satisfiable¹⁸ or refutable.

We obtain a different generalization of Theorem I by considering denumerably infinite sets of logical expressions. For these, too, an analogue of Theorems I and II holds, namely

THEOREM IX. Every denumerably infinite set of formulas of the restricted functional calculus either is satisfiable (that is, all formulas of the system are simultancously satisfiable) or possesses a finite subsystem whose logical product is refutable.

IX follows immediately from

THEOREM X. For a denumerably infinite system of formulas to be satisfiable it is necessary and sufficient that every finite subsystem be satisfiable.

Concerning Theorem X we first note that in proving it we can confine ourselves to systems of normal formulas of degree 1, for, by repeated application of the procedure used in the proofs of Theorems III and IV to the individual formulas, we can specify for every system Σ of formulas a system Σ′ of normal formulas of degree 1 such that the satisfiability of any subsystem of Σ is equivalent to that of the corresponding subsystem of Σ′.

Thus let

be a denumerable system Σ of normal expression of degree 1, and let be an γ_i-tuple, an s_i-tuple of variables. Let be the sequence of all γ_i-tuples taken from the sequence and ordered according to increasing sum of the subscripts [and for equal sums according to some convention]; furthermore, let be an s_i-tuple of variables, of the sequence above, such that the sequence of variables

becomes identical with the sequence if every is replaced by the corresponding s_i-tuple of the x. Further we define, in a way analogous to what was done above, a sequence {B_n } of formulas by means of the stipulations

We can easily see that (P_n)B_n (that is, the formula that results from B_n when all 591 individual variables occurring in it are bound by existential quantifiers) is a consequence of the first n expressions of the system Σ given above. If, therefore, every finite subsystem of Σ is satisfiable, so is every B_n. But, if every B_n is satisfiable, so is the entire system Σ (as follows by the argument used in the proof of Theorem V (see p. 588)), and Theorem X is thus proved. Theorems IX and X can be extended without difficulty, by the procedure used in the proof of Theorem VIII, to systems of formulas containing the sign "=".

We can also give a somewhat different turn to Theorem IX if we confine ourselves to systems of formulas without propositional variables and regard them as systems of axioms whose primitive notions are the functional variables occurring in them. Then Theorem IX clearly asserts that every finite or denumerable axiom system in whose axioms "all" and "there exists" never refer to classes or relations but only to individuals¹⁹ either is inconsistent (that is, a contradiction can be constructed in a finite number of formal steps) or possesses a model [Realisierung].

Finally, let us also discuss the question of the independence of Axioms 1–8. So far as Axioms 1–4 (those of the propositional calculus) are concerned, it has already been shown by P. Bernays²⁰ that none of them follows from the other three. That their independence is not affected even by the addition of Axioms 5–8 can be shown by means of the very same interpretations that Bernays uses, provided that, in order to extend them to formulas containing functional variables and the sign "=", we make the following stipulations:

1. The prefixes and individual variables are omitted;

2. In what remains of each formula the functional variables are to be treated just like propositional variables;

3. Only "distinguished" values may ever be substituted for the sign "=".

To demonstrate the independence of Axiom 5, we associate with each formula another one, which we obtain by replacing components of the form

²¹

should such occur, by Then Axioms 1–4 and 6–8 go over into valid formulas, and the same holds, as we can convince ourselves by mathematical induction, of all formulas derived from these axioms by Rules of inference 1–4; Axiom 5, however, does not possess this property. The independence of Axiom 6 can be shown in exactly the same way, except that here (x)F(x), (y)F(y), . . ., and so on must be replaced by X & To prove the independence of Axiom 7 we note that Axioms 1–6 and 8 (and therefore also all formulas derived from them) remain valid if the identity relation is replaced by the empty relation, whereas this is not the case for Axiom 7. Similarly, the formulas derived from Axioms 1–7 remain valid when the identity relation is replaced by the universal relation, whereas this is not the case for Axiom 8 (in a domain of at least two individuals). We can also readily see that none of the Rules of inference 1–4 is redundant, but we shall not look into this more closely here.

¹ I am indebted to Professor H. Hahn for several valuable suggestions that were of help to me in writing this paper.

^a The degree was granted on 6 February 1930.

² See Bernays 1926.

³ In terminology and symbolism this paper follows Hilbert and Ackermann 1928. According to that work, the restricted functional calculus contains the logical expressions that are constructed from propositional variables, X, Y, Z, . . ., and functional variables (that is, variables for properties and relations) of type 1, F(x), G(x, y), H(x, y, z), . . ., by means of the operations (x) (for all), (Ex) (there exists), with the variable in the prefixes (x) or (Ex) ranging over individuals only, not over functions. A formula of this kind is said to be valid (tautological) if a true proposition results from every substitution of specific propositions and functions for X, Y, Z, . . . and F(x), G(x, y), . . ., respectively (for example,

⁴ To be more precise, we should say "valid in every domain of individuals", which, according to well-known theorems, means the same as "valid in the denumerable domain of individuals". For a formula with free individual variables, A(x, y, . . ., w), "valid" means that (x)(y) . . . (w)A (x, y, . . ., w) is valid and "satisfiable" that (Ex)(Ey) . . . (Ew)A(x, y, . . ., w) is satisfiable, so that the following holds without exception: "A is valid" is equivalent to "A is not satisfiable".

⁵ It coincides (except for the associative principle, which P. Bernays proved to be redundant) with that given in Whitehead and Russell 1910, *1 and *10.

⁶ Although Whitehead and Russell use these rules throughout their derivations, they do not formulate all of them explicitly.

⁷ An analogous theorem holds with instead of &.

⁸ See Hilbert and Ackermann 1928, chap. 3, § 8.

⁹ See Bernays 1926.

¹⁰ "A is refutable" is to mean " is provable".

¹¹ "Satisfiable" without additional specification here and in what follows always means "satisfiable in the denumerable domain of individuals". The same holds for "valid".

¹² The variables x and y must not occur in (P).

¹³ The term "degree of a prefix" is used in the same sense.

¹⁴ An analogous procedure was used by Skolem (1920) in proving Löwenheim’s theorem.

¹⁵ The variable-sequences are of course, assumed to be pairwise disjoint.

¹⁶ That a system is part of another, is to mean that

1. The domain of individuals of the f_i is part of the domain of individuals of the g_i;

2. The f_i and the g_i coincide within the narrower domain;

3. For every i,

^16a [Apparently by König’s infinity lemma (1926, p. 120; see also 1927), which was becoming known among mathematicians at the time Gödel was writing.]

¹⁷ If propositional variables also occur in A, S will, of course, have to contain, besides functions, truth values for these propositional variables.

¹⁸ And, moreover, in an at most denumerable domain (for it consists of disjoint, classes of the denumerable domain Σ of individuals).

¹⁹ Hilbert’s axiom system for geometry, without the axiom of continuity, can perhaps serve as an example.

²⁰ See Bernays 1926.

²¹ That is, the singulary functional variables F, G, . . . preceded by a universal quantifier whose scope is just the F, G, . . . in question, along with the associated individual variable.