508 Mathematical Logic

On mathematical logic

THORALF SKOLEM n/a

(1928)

1928 *Über die mathematische Logik, Norsk matematisk tidsskrift 10, 125–142 (508–524 of the present volume).

This is the text of a lecture delivered before the Norwegian Mathematical Association on 22 October 1928. Skolem briefly presents Boolean algebra and the first-order predicate calculus, and makes some remarks about the second-order predicate calculus. He presents a few rules for the first-order predicate calculus but then says: "I do not go into this more deeply, especially since I believe that it is possible to deal with deduction problems in another, more expedient way". We shall see in a moment what this other way is.

In the first-order predicate calculus Skolem considers an arbitrary closed well-formed formula Z in prenex form. He puts the formula into what we shall call its functional form for satisfiability: all quantifiers are dropped, and the occurrences of each variable bound by an existential quantifier are replaced by a functional term^a containing the variables that in Z are bound by universal quantitiers preceding the existential quantifier. A formula U is thus obtained. Skolem then introduces constants of various levels. "0" is the constant of the 0th level. The constants of the nth level are the expressions obtained when in each functional term of U the variables are replaced by constants that include at least one constant of, but no constant beyond, the level. Thus, the functional terms of U, indefinitely compounded, generate from "0" the lexicon^b of U; the subset of the lexicon of U consisting of all constants of levels will be called the lexicon of level n.

If W is U or any truth-functional part of U, by a lexical instance of W will be meant the formula obtained when all the variables of W are replaced by elements from the lexicon of U. Skolem calls an assignment of truth-values to lexical instances of atomic parts of U a solution of the nth level if and only if the assignment verifies the conjunction of all the lexical instances of U formed from the lexicon of level of U. Clearly, any solution of the nth level is an extension of a solution of the level.^c

Either for some nthere is no solution of the nth level or for every n there is a solution of the nth level. In the first case, Skolem claims, Z "contains a contradiction" ("enthält einen Widerspruch"). If to the present paper we add the evidence furnished by other papers of Skolem’s,^d 509 we should take "contains a contradiction" to mean that Z is not satisfiable, and Skolem indeed establishes in those papers^e that, if Z is satisfiable, there is, for every n, a solution of the nth level. (In the present paper Skolem’s argument rests upon an implicit use of the axiom of choice" see below, p. 518.) In his other papers Skolem also establishes the (deeper) converse, namely, if for every nthere is a solution of the nth level, Z is satisfiable.^f (What he actually proves is that Z is -satisfiable.) We now see what Skolem’s other way is. It is a proof procedure for the first-order predicate calculus: given a formula Z in prenex form and a number n, we can effectively decide whether or not there is a solution of the nth level for Z; if for some nthere is no solution of the nth level, Z is not satisfiable, hence ~ Z is valid. This approach furnishes an alternative to the axiomatic approach to the first-order predicate calculus (that is, the approach that follows the lines of Whitehead and Russell 1910 or Hilbert and Ackermann 1928). Note that this alternative provides proofs that are cut-free and have the subformula property. What Skolem has in fact established in these various papers is that his proof procedure is sound and complete, in the sense of Quine (1955a, p. 145)—except for one minor point: it has to be shown that a formula is satisfiable if and only if one of its prenex forms is satisfiable. Skolem does not explicitly discuss this question, but the transformation rules that in the present paper (p. 130; below, p. 516) he gives as examples of rules for the first-order predicate calculus are precisely the rules that allow us to pass from a formula to any of its prenex forms and conversely.^g

The present paper contains an obscure passage (below, p. 519, lines 6–17) that deals with the second ease mentioned above, namely, the case in which for every n there is a solution of the nth level. Skolem seems to be arguing—and arguing finitistically—that, if such is the case, the "theory" obtained when Z is added as an axiom to quantification theory is syntactically consistent. (Two passages in Skolem 1929^h very similar to the one under discussion and somewhat less obscure lend weight to this reading.) Thus Skolem seems to be arguing for a proposition that is the main consequence of Herbrand’s fundamental theorem (see Herbrand 1930, p. 120 (below, p. 561), and also footnote 103 below, p. 561). Moreover, in § 5 and § 6 of 1929 Skolem uses this proposition to study consistency properties of first-order theories in a way quite analogous to Herbrand’s. (See Kalmár’s discussion of what he calls the Skolem-Herbrand lemma in Kalmár 1951.)

In 1962, p. 47, Skolem writes: "The 510 theorem of Löwenheim says that, if F is a well-formed formula of the first-order predicate calculus with certain predicate variables A, B, C, . . ., either ~ F is provable or F can be satisfied in the natural number series by suitable determination of A, B, C, . . . in that domain of individuals". If "provable" is understood as derivable from axioms by rules of inference in an axiomatic version of quantification theory, that result was established by Gödel (1930a). If "provable" refers to some informal version of quantification theory, some of Skolem’s arguments, when taken together, provide a sketch of a proof for the result. Finally, if by "~ F is provable" we understand, in the sense of the proof procedure, that for some nthere is no solution of the nth level for F, the result was firmly established by Skolem in 1922 for any F in Skolem normal form and in 1929 (p. 27, line 12, to p. 28, line 9) for any prenex F.ⁱ Compare also 6.2 of Herbrand 1930 (below, p. 558).

Let us observe that in these 1922 and 1929 proofs Skolem is able to dispense with the use of the axiom of choice by suitably ordering, for every n, the solutions of the nth level. In 1929, p. 25, lines 9u-6u, he notes that use could be made of the following proposition of set theory: If a set M of finite sets is such that every element of M is a subset of another element of M, then M contains as a subset an infinite sequence such that, for every i, m_i is a subset of This proposition,^j which is related to König’s infinity lemma (1926, 1927), can be regarded as a version of the axiom of dependent choices (Tarski 1948, p. 96; see also Bernays 1937–1954, 7, p. 86). Skolem adds that, if the use of the axiom of choice is permitted, there is a much simpler proof of the Löwenheim theorem, namely the proof that he gave in 1920 and, in a somewhat different version, in 1929 (p. 24, lines 20-10u).^k In Gβdel’s completeness proof (1930a), when the argument requires that from the existence of an infinite sequence of satisfying assignments (Skolem’s "solutions") the existence of a satisfying assignment in an infinite domain be inferred, an appeal is made to "familiar arguments" ("bekannten SchluΒweisen"; see below, p. 589). In a conversation in April 1964 Professor Gödel told the editor that 511 these words refer to König’s infinity lemma.¹

It should be observed that Herbrand’s fundamental theorem (1929a, 1930, 1931; see below, p. 554) can be taken to establish the completeness of an axiomatic formulation of quantification theory once Skolem’s proof procedure is seen to be complete. For Skolem’s result of 1929, partially translated into Herbrand’s terms (see above p. 508, footnote c), reads: If for no n a prenex formula Z has property C of order n, then ~ Z is satisfiable. And Herbrand’s theorem states, in part, that, if for some n the formula Z has property C of order n, Z is provable (in an axiomatic system), or, by contraposition, if Z is not provable, for no n does Z have property C of order n. Hence, by transitivity, if Z is not provable, ~ Z is satisfiable, or, if Z is valid, Z is provable which for prenex Z is Gödel’s 1930 completeness result. The impact of Herbrand’s errors upon this argument is discussed by Dreben in Note H below (pp. 578–580).

In the present paper Skolem approaches the decision problem from the point of view of his proof procedure. For certain classes of formulas we can effectively decide whether or not for every n there is a solution of the nth level. Skolem first considers a formula whose prefix consists of a single universal quantifier followed by any number of existential quantifiers, and he shows that in that case we are able to conclude to the satisfiability or nonsatisfiability of the given formula. The subcase of the prefix (x) (Ey) had already been solved by Bernays and Schönfinkel (1928). A paper of Ackermann’s (1928a) containing a solution of the case studied by Skolem was published soon after Skolem’s lecture. (Ackermann’s paper was received for publication on 9 February 1928 and the fascicle of the periodical was made ready for the press on 28 December 1928.) Ackermann’s result goes beyond Skolem’s; he obtains an upper bound for the number of individuals of the finite domain in which the formula is satisfiable, if it is satisfiable at all. He also solves the more general case of the prefix and finds an upper bound for that case too. Ackermann’s method is somewhat similar to Skolem’s. (Later, in 1954, pp. 72–74, Ackermarm follows an entirely different approach.) In a review of Ackermann’s paper Skolem (1928b) gives an argument that simplifies Ackermann’s proofs and yields a smaller upper bound. Skolem expands these remarks in a subsequent paper (1935); there he also presents his 1928 proof in a more detailed and precise form, and he generalizes his result in a new direction, namely, to formulas of the form

where L(x₁, x₂, x₃) contains only binary predicates and is a conjunction stating that each R_i, is symmetric and transitive. (For the significance of this result see Skolem 1935a.) For the case of the prefix Herbrand was able (1931, pp. 45–47; see also 1930, pp. 118–119 (below, pp. 558–560)), through the use of his fundamental theorem, to simplify Ackermann’s proof and obtain a smaller upper bound; he also extended the result to a formula consisting of the prefix followed by a conjunction of prenex formulas of the form

The present paper shows also that it is possible to decide the satisfiability of a prenex formula if the prefix is of the form 512 and all of the variables occur in each of the atomic parts of the matrix. A few years later (1935) Skolem again presents a proof of this result and points out that it can easily be extended to the case in which either all of the variables or at least one of the variables occurs in each atomic formula of the matrix. Below, Skolem observes that, for the prefix in question, the satis-liability of a formula can be decided if at least distinct variables occur in each atomic part of the matrix. At the end of the paper Skolem presents Lang-ford’s result that the theory of open dense order is decidable.

Professor Skolem pointed out a number of corrections that should be introduced into the German text:

Page 132, line 9u, there should be a bar over the second occurrence of "V";

Page 136, line 1u, there should be a bar over the second occurrence of "B";

Page 137, line 7u, the third occurrence of "y" should have the subscript "1", not "n";

Page 137, line 6u, the first occurrence of "y" should have the subscript "1", and " . . ." should be deleted before the first and third occurrences of "y";

Page 139, lines 8u and 7u, the three occurrences of "+" should be deleted and the resulting spaces closed up;

Page 139, line 4u, "einfacheren" should be replaced by "gegebenen";

Page 139, the last three lines should be replaced by: "dadurch zu zeigen, dass man für jedes Paar x₁, x₂ ein und x₂ wählt und allgemein wählt so oft dagegen so oft ".

These corrections have been incorporated into the translation below.

The translation is by Stefan Bauer-Mengelberg and Dagfinn Føllesdal, and it is printed here with the kind permission of Professor Skolem and the editing secretary of Nordisk Matematisk Tidskrift.

B. Dreben and the editor

Logic, as is well known, was established as a science by Aristotle. Everyone knows the Aristotelian syllogism. During the entire Middle Ages Aristotle’s syllogistic figures constituted the principal content of logic. Kant is said to have remarked once that logic was the only science that had made no progress at all since antiquity. Perhaps this was true at the time, but today it is no longer so.

For recent times have seen the development of the calculus of logic, as it is called, or mathematical logic, a theory that has gone far beyond Aristotelian logic. It has been developed by mathematicians; professional philosophers have taken very little interest in it, presumably because they found it too mathematical. On the other hand, most mathematicians, too, have taken very little interest in it, because they found it too philosophical.

I do not intend to give a precise account of the history of this discipline here. I mention the names of Leibniz, Lambert, Boole, Peirce, Macfarlane, and Frege. The German mathematician Schröder wrote a large work, Algebra der Logik (three volumes: 1890, 1891, 1895), which is very valuable. A different tendency was initiated by the Italian mathematician Peano, as well as by Frege, and carefully developed in all details by the Englishmen Russell and Whitehead. They wrote a large work, Principia mathematica (1910, 1912, 1913); in it they attempt to develop all of mathematics as a part of mathematical logic. Of the more recent writers I would like to mention Löwenheim, Behmann, Schönfinkel, Chwistek, Ramsey, and Langford. Finally, some of the investigations in the foundations of mathematics by Hilbert and his collaborators, Bernays, von Neumann, and Ackermann, belong here.

513

First I would like to discuss one of the simplest parts of the calculus of logic, the identical calculus [identischen Kalkul],¹ in some detail. It can be developed as a calculus of classes or regions (in a plane, say). We consider a totality of objects; this totality is called the universal class and is denoted by 1. On the other hand there is to be a null class, 0; it contains no element at all. If a and b are two arbitrary classes, it may happen that every object occurring in a also occurs in b; for that relation I write If both and I write From the classes a and b we can separate the greatest common part; this class will be denoted by ab. Likewise we can combine the objects occurring in a or b into a class, which will be denoted by Finally, the objects not occurring in a form a class, which we shall denote by Then we can develop an algebra in which occurs as the fundamental relation and we have the three operations mentioned. Among others, the following laws hold:

and, besides, the rules of inference

We must remark, however, that the operations of identical multiplication and identical addition can be extended to infinitely many operands, too. By the identical product of arbitrarily many classes where κ ranges over a certain supply of values, we understand the class of all elements that are common to all a_k. By the identical sum we understand the class of all objects that occur in at least one of the a_k.

I shall not dwell on this calculus for long, but I would like to show, by way of an example, how equations containing unknowns can be solved in it. If an equation of the form

is given (every equation can be brought into the form and every system of simultaneous equations can be written as a single equation), we find that is the necessary and sufficient condition for the existence of a solution and that the general solution is given by

where u stands for an arbitrary class.

Proof. If then since both ax and are equal to 0. Hence every solution has the form If it follows that, when

514

But we can also solve equations with an entirely arbitrary number of unknowns. For example, let the equation

be given, where the subscripts range over a given supply of values; assume that the classes a are given but that the x are unknowns. Here we find that

is the necessary and sufficient condition for the existence of a solution and that

is the general solution.

Another example is

where the prime on Σ means that μ and ν shall always take different values. The necessary and sufficient condition for the existence of a solution here is

where P ranges over all possible finite products of the coefficients a in which the pairs of subscripts μ, ν form a cycle with an odd number of terms. Hence this shows that in such problems we are led to peculiar combinatorial questions.

But I shall not go into problems of this kind in more detail; rather, I shall proceed to discuss the general notions and operations of the more recent mathematical logic.

The fundamental notions of mathematical logic are the following:

(1) Propositions; true and false;

(2) Propositional functions of variables; properties (classes) and relations [Beziehungen] (relations [Relationen] and correspondences).²

The logical operations are

(1) The elementary ones: conjunction, disjunction, and negation;

(2) The higher ones: "all" and "there exists".

We assume that, if a sentence has meaning,³ it is either true or false. If a proposition expresses something about an object x—I then write it A(x)—it may happen that it has meaning for all values of x within a certain domain. Then we say that A(x) is a propositional function if x is a variable that can take arbitrary values in that domain. If a specific value is substituted for x, we obtain a proposition, which will be true or false, depending on the circumstances. In a similar way we can form propositional functions of two, three, or more variables: A(x, y), A(x, y, z), . . . If a specific value is substituted for y in A(x, y), we obtain a propositional function of x alone; if specific values are substituted for x as well as y, we obtain a proposition. The propositional 515 function "x is a prime number" is a function P(x) of x; for example, P(3) is true but P(6) false. The propositional function "x and y are relatively prime" has two arguments; for and for example, it yields a true proposition, and for and a false one.

A propositional function like A(x) represents what is called a "property"; we say that the objects x for which A(x) becomes a true proposition form a "class". The propositional functions of several variables represent "relations" ["Beziehungen" oder "Relationen"].

The three elementary operations are those that in ordinary language are rendered by the words "and", "or", and "not". In Schröder’s notation the propositions "A as well as B", "either A or B", and "not A", where A and B are given propositions, are written AB, and respectively.

Hence the expression means "either not A or B". That is clearly the same as "if A holds, so does B", or "from A, B follows". This is what is called implication, and it is therefore reducible to the first three operations mentioned. Disjunction, moreover, can be reduced to conjunction and negation, since means the same as

These elementary operations are clearly applicable to propositions as well as to propositional functions. The two higher operations, which are expressed by the words "all" and "there exists", are, however, applicable only to propositional functions. They have the effect that for one or more variables substitutions become impossible, the variables being transformed from "real", or "free", variables into "apparent", or "bound", ones.

If A(x) is a propositional function, we can form the propositions "A(x) is true for all x" and "there exists an x such that A(x) is true"; following Schröder, we write these as and respectively. Clearly, no substitution can be made for x here; hence x has become an apparent variable, just like a variable of integration. From a propositional function A(x, y) we can first form the propositional functions and the first two are functions of x (but not of y), the latter two are functions of y. From these, then, the propositions and so forth can in turn be formed. We readily see that the proposition means that there exists an x such that, when this x is held constant, A(x, y) is true for all y, while the proposition means that for every y there exists an x, which in general depends on y, such that A(x, y) holds. Of course, we can form propositions such as and so forth.

Here are some simple examples from arithmetic:

where the variables range over the sequence of natural numbers. The first proposition means that for every number there exists a greater one, the second that there exists a least natural number, and the third that among all the numbers that are greater than x there exists a least.

516

Now we can not only give a precise formulation to mathematical propositions but also represent mathematical proofs as transformations of such logical expressions according to certain rules. For example, we have the rules

But I do not go into this more deeply, especially since I believe that it is possible to deal with the deduction problems [Deduktionsprobleme] in another, more expedient way, to which I shall return in a moment.

If certain propositional functions are given, together with a range for the values of the variables, we are now in a position to form from them further propositional functions and propositions by means of the five logical operations. The values of the variables may be called "individuals". Propositional functions and propositions that have individuals as arguments and in which "all" and "there exists" are applied only to variable individuals are often called first-order propositional functions [Zählaussagen-funktionen] and first-order propositions [Zählaussagen], respectively.⁴ It must be noted, however, that the logical construction of propositions does not end here. For we can have a variable propositional function in a propositional expression, and then "all" and "there exists" can be applied to it, too. So, for example,

where U and V are variable propositional functions, is a proposition about U and V; that is, the expression is a propositional function of a higher logical kind, having first-order propositional functions as arguments. But we can also obtain functions of a higher kind whose arguments are still individuals. A simple example is

this expression represents a propositional function whose arguments are x and y, since in it the universal quantifier governs the variable propositional function U. In this way the construction of propositional functions becomes quite complicated; and it cannot be denied that questions arise here that are very difficult to answer. If "all" and "there exists" are applied to variable propositional functions, the question arises: what is the totality of all propositional functions? It seems to me that only two conceptions are scientifically tenable here; these I now indicate.

1. We can start from certain actually given, that is, listed, primitive propositional functions. Other functions are formed from these, first, by means of the five operations in such a way that "all" and "there exists" are applied only to individuals. This yields the totality of propositional functions of the first level [Stufe] (the first-order functions [Zählfunktionen]). After this totality has been formed, it is meaningful, on 517 the one hand, to form functions whose arguments are functions of the first level; on the other hand, we can form functions that have individuals as arguments but that result from the application of "all" and "there exists" to functions of the first level. Thus we obtain functions of the second level, but of two essentially different kinds. Whenever the constructible functions of a certain "level", or "type", are collected into a totality, the formation of new functions is made possible.

2. We can attempt to introduce the notion of propositional function (which, after all, corresponds rather precisely to the notion "set") by means of an axiomatization, just as we axiomatize set theory. The axioms will then become first-order propositions, since the objects of the axiomatization (here the "propositional functions", in set theory the "sets") will assume the role of individuals. The relations between arguments and functions will then appear in the axiomatization as primitive functions, just as the relation ε (element of) appears as primitive function in axiomatic set theory.

I here permit myself a remark about the relation between the fundamental notions of logic and those of arithmetic. No matter whether we introduce the notion of propositional function in the first or the second way, we are confronted with the idea of the integer. For, even when the notion of propositional function is introduced axiomatically, we shall have to consider (for instance, in investigations concerning consistency) what we can derive by using the axioms an arbitrary finite number of times. On the other hand, it is not possible to characterize the number sequence logically without the notion of propositional function. For such a characterization must be equivalent to the principle of mathematical induction, and this reads as follows: If a propositional function A(x) holds for and if is true whenever A(x) is true, then A(x) is true for every x. In signs, it takes the form

This proposition clearly involves the totality of propositional functions. Therefore, the attempt to base the notions of logic upon those of arithmetic, or vice versa, seems to me to be mistaken. The foundations for both must be laid simultaneously and in an interrelated way.

I shall not go into these difficult questions more deeply; instead, I shall indicate how the deduction problems for first-order propositions can be reduced to a problem of combinatorial arithmetic [eine arithmetisch-kombinatorische Frage]. If U and V are first-order propositions and if we pose the question whether V follows from U, this is equivalent to asking whether is a contradiction or not. It is therefore clear that everything depends upon our being able to decide whether a given first-order proposition is contradictory or not.

Let a first-order proposition Z(A, B, C, . . .) be given, where A, B, C, . . . are the given propositional functions occurring in it; I call these the primitive functions. I can assume that Z has the form

This axiom obviously means that, if are arbitrarily given, it is possible to introduce where the y depend only on the x, the u 518 only on the x and the z, and so on, and to determine the truth values of the functions A, B, C, . . . for these arguments in such a way that U turns out to be true. Since it does not matter what notation we use for the symbols, we can introduce the following symbolism, which is probably more advantageous for almost all investigations. Instead of I write instead of I write and so on. The given first-order proposition then means that

is true for arbitrary values of within a certain domain.

If we now wish to investigate whether this axiom is satisfiable or not, we can proceed as follows. Let us form, starting from the symbol 0, the symbols and so on. 0 will be said to be the individual-symbol of the 0th level, while the symbols and so on will be said to be of the 1st level. Once the individual-symbols are defined up to the nth level, the symbols of the level shall be those that result from the insertion of symbols up to the nth level as arguments in the "functions" and that do not already occur among the symbols of the 0th to the nth level. The sequences formed by the symbols up to the nth level I call argument sequences of the nth level. Now we must try to assign values to the functions A, B, C, . . . in such a way that, for each argument sequence in turn, U comes out true. To translate everything into ordinary mathematical language I denote the propositional values "false" and "true" by 0 and 1, respectively. If I now denote the truth value of A by wA, the following relations hold:

We thus come to the following purely arithmetic problem.

A, B, C, . . . are functions of a finite number of arguments; they can take only the values 0 and 1. Further U is a function constructed from A, B, C, . . . (these being written with certain arguments) by means of the operations min, max, and 1 −; the arguments are As all the argument sequences mentioned above come to be substituted successively for the point is to assign values to A, B, C, . . . in such a way that U takes the value 1 for each argument sequence.

First, we put 0 for Perhaps it is already impossible at this point to assign values to A, B, C, . . . in such a way that In that case the first-order proposition is not satisfiable; there is a contradiction. Otherwise there exist some choices of values for A, B, C, . . . such that U will have the value 1.⁵ These possibilities I call solutions of the 1st level. Next we have to insert all argument sequences of the 1st level. Perhaps it is impossible at this point to choose values for A, B, C, . . . in such a way—the values for the different argument sequences must, of course, be chosen in agreement with one another whenever these sequences have symbols in common—that U will always = 1; if so, we have a contradiction. Otherwise 519 there must again be some possibilities available; I call them solutions of the 2nd level. Every solution of the 2nd level is the continuation of a solution of the 1st level, in the sense that it contains such a solution within itself. In this way we continue indefinitely. The real question now is whether there are solutions of an arbitrarily high level or whether for a certain n there exists no solution of the nth level. In the latter case the given first-order proposition contains a contradiction. In the former case, on the ether hand, it is consistent [widerspruchslos]. The following will make this clear. Every consequence of the axiom results from repeated and combined uses of it. Every theorem derived can therefore be formulated as a proposition formed by means of the functions A, B, C, . . . and in these functions there will occur, on the one hand, indeterminate symbols a, b, c, . . . and, on the other, further symbols that have been obtained from these by possibly repeated substitutions in the functional expressions Every such proposition must, however, retain its validity when a, b, c, . . . all are replaced by 0. Thus, if a contradiction is derivable, a contradiction must be provable in which there occur both 0 and the symbols obtained from 0 by substitution in up to, say, the nth level. Hence there cannot then exist any solution of the nth level.

To be sure, this procedure is infinite; but there are some cases in which it is possible to make the procedure finite. For example, let a first-order proposition of the form

be given. Here, instead of I simply write 1, 2, . . ., n; instead of I write 2n; instead of I write 3n; and so on, until, instead of I write First, let 0 be substituted for x and therefore 1, 2, . . ., n for respectively; the values that can then be chosen for A, B, C, . . . so as to make will, when taken together, yield certain alternatives When at the next step the values 1, 2, . . ., n are substituted for x, the only possibilities that we then have are those that result whenever an alternative is compatible, for each r in the sequence 1, 2, . . . n, with at least one of the alternatives Let be those of the alternatives for which this is the case. If the continuation to the next level is possible, the only alternatives that have to be considered are the Now again let be those, from among the alternatives that are compatible, for , with at least one of the alternatives Then only the will have to be considered, and let be those, from among the alternatives that are compatible, for , with at least one of the alternatives And so on. Since only a finite number of alternatives with is available, this process must actually terminate; that is, after a finite number of steps we arrive at a number s such that the alternatives are the same as the It may be that at this point no alternative is available any more; in that case the given first-order proposition is contradictory. But, if there is at least one alternative the first-order proposition is consistent. For we recognize that it is then possible, for each new argument sequence of the 520 individual variables to form a corresponding alternative that is consistently compatible with the alternatives set up for the earlier argument sequences. That it is so simple here is due to the fact that an argument sequence R_n, of the nth level, that does not already occur at the level has an element in common with only a single argument sequence of the level, if we disregard argument sequences of levels above the nth. Therefore the determination of the functions A, B, C, . . . for R_n is independent of the determination of these functions for all earlier argument sequences with the sole exception of

Example 1. Let us investigate whether or not the first-order proposition

is contradictory. Here we can put 1 for y if 0 is put for x, and in general for y whenever n is put for x.

In the arithmetic formulation the problem is: Investigate whether it is possible to determine the function A(x, y), whose values shall be restricted to 0 and 1, in such a way that for all

The alternatives here are these two:

Hence

Thus is here compatible with both and while is compatible only with But, since both can be continued and at the same time both can occur as continuations, the coincide with the already at this point. Hence the given proposition is consistent. Indeed, we already obtain a solution of the arithmetic problem if we set for all n, no matter what values the function has otherwise.

Example 2. Let us examine whether or not the first-order proposition

is consistent. Here we obtain

as alternatives of the first level. Hence

Here is compatible with but not with cannot be continued at all. Thus there is only one namely but there does not occur any at all. Hence the proposition contains a contradiction.

521

There are some other propositions in ΠΣ-form that can be treated in a precisely analogous way.⁶ Let

be such a first-order proposition Z. It can be written in such a way that we need take only distinct elements x into consideration. That is immediately the case if the truth of U for two identical x always follows from the truth of U for distinct x; otherwise we can transform the proposition. Let be m distinct individuals; let be the different permutations with repetitions of these individuals taken m at a time. According to the proposition Z there then exists, for each sequence a sequence of individuals such that is true. Now let

Then Z can obviously be written thus:

where now only the various combinations of individuals taken m at a time from the domain in question are to be substituted for Hence we need only consider propositions of the form just mentioned, for example,

In order to investigate satisfiability we can first substitute the symbols 1, 2, . . ., m for and the numbers for this yields the argument sequence of the 1st level. Next, let all the combinations of the numbers taken m at a time that differ from the combination 1, 2, . . ., m be formed and ordered (say lexicographically). To the first combination let us assign the numbers as y-values; to the second let us assign as y-values the numbers and so on. Thus we obtain the argument sequences of the 2nd level. Then let us form all new combinations of all the numbers, taken m at a time, that we have considered so far (that is, all the combinations that have not yet occurred as values for the x); and so on.

I now make the assumption that all the primitive functions occurring in our first-order proposition possess at least m distinct argument symbols; then it is possible to decide the question of satisfiability by a finite procedure. This is due to the fact that every argument sequence of the νth level has, if we disregard argument sequences of higher levels, an argument system in common with only a single argument sequence of the level.

Let be the alternatives that are possible for the argument sequence where all a and b are distinct symbols. Further, let the 522 sequence be any one of the combinations, of the symbols taken m at a time, that are different from the combination with each such combination we associate a sequence of n distinct symbols in such a way that the sequences and that correspond to two different combinations are completely distinct and that all d are distinct from all a and b. Then we have to select from the set of alternatives those that, for each combination are compatible with at least one of the alternatives to select from these alternatives again the that, for each combination are compatible with at least one of the alternatives and so on. Just as before, we arrive at a number s such that the alternatives coincide with the If at this point there exist alternatives the given proposition is consistent; otherwise it represents a contradiction.

I give a simple example. Assume that in the proposition

U(x₁, x₂, y) has the following form:

Since U(x₁, x₂, y) is symmetric with respect to x₁ and x₂, and U(x₁, x₁, y)U(x₂, x₂, y) is [logically] contained in U(x₁, x₂, y), the given proposition can at once be written in the form

where the pair (x₁, x₂) must run through all unordered pairs of the domain considered. Here 1, 2, 3 is the argument sequence of the 1st level; the argument sequences of the 2nd level are 1, 3, 4 and 2, 3, 5. One of the alternatives here is which means and This alternative is compatible with that is, and as well as with that is and This already proves the consistency.

If on the other hand the proposition

were given, then, by the rule of transformation explained above, it would turn into

We can then show the consistency of this proposition by the systematic method; but it is simpler to show the consistency of the given proposition by choosing for each pair (x₁, x₂) a y greater than x₁ and x₂, and by taking in general whenever but whenever

523

If all primitive functions of the ΠΣ-proposition

have at least distinct argument symbols, the proposition is consistent if and only if U is consistent. For, the distinct argument sequences that we obtain by the procedure applied on page 519 never have more than m symbols in common, so that values are assigned to the primitive functions for each of the argument sequences, as they successively appear, independently of all the others.

It is possible, of course, to pose further problems concerning first-order propositions. An interesting question is whether an axiom, or axiom system, given as a first-order proposition Z is categorical [kategorisch]; we say that Z is categorical if it is possible to show, for an arbitrary first-order proposition Z′ formed by means of the same primitive functions as Z, that it is true or false.⁷ C. H. Langford has recently (1926, 1926a) given some examples of such categorical axiom systems. I would like to give a very simple but nevertheless not too trivial example of this here. I consider the following axioms:

If we write I(x, y) for R(x, y)R(y, x), we recognize on account of 3 that Φ(y) always follows from I(x, y)Φ(x), where Φ is an arbitrary first-order propositional function that can be formed from R, and likewise that Φ(x) follows from I(x, y)Φ(y). The propositional function I therefore deserves to be called "identity" in the domain of the first-order propositions derivable from R. Since x and y are no longer distinguished when I(x, y) holds, it is easy to see that the axioms listed determine an ordering of all individuals in an open and dense sequence.

Let us now consider the expression

where U is an elementary propositional function⁸ formed from R. I will show that this expression, by virtue of the axioms, is always equivalent to an elementary propositional function that is, that both always have the same truth value. In order to show that, I of course need only consider the case in which U is constructed 524 by means of negation and conjunction alone. Moreover, propositional conjuncts like R(x_i, x_j) can be moved to the left of the If the propositional conjunct occurs, the proposition is always false. If the conjunct R(y, y) occurs, it can be omitted, since on account of 2 it is always true. If we let denote the x that occur in U, we obtain

and follow from this proposition for all α, β, γ, and δ. I assert that, conversely, the truth of the follows from the conjunction of all R(α, β) and For we can imagine that the subscripts of the letters are so chosen that R(α, α₁), holds for all α, and likewise R(β₁, β) for all β, R(γ₁γ) for all γ, and R(δ, δ₁), for all δ. Now four cases are possible: (1) We have Since holds, there exists, by 6, a y such that obtains, from which we can easily derive the truth of the (2) holds. Then the already holds if we substitute β₁ for y. (3) We have Then the holds if we substitute α₁ for y. (4) holds. If R(β₁, α₁) is true, the holds if α or β is substituted for y. If is true, there exists a y such that obtains, and from this the truth of the follows.

It is easy to discover how the matter stands in the simpler cases in which not all four of the sequences α, β, γ, and δ occur.

Hence any propositional function is false for all x, true for all x, or surely replaceable by an elementary function If we use negation, we see that the same holds for Consequently the apparent variables occurring in an arbitrary first-order proposition can gradually be eliminated. When all but one have been eliminated, the last elimination directly yields the result "true" or "false".

I hope hereby to have given a little insight into some of the most important problems of mathematical logic.

^a We find it convenient to use here the expression "functional term", although it is not Skolem’s. A functional term is a formula consisting of a function letter followed by variables, with the proper parentheses and commas.

^b This term, not in Skolem, is borrowed from Quine 1955a, p. 141.

^c Compare the notions introduced here by Skolem with Herbrand’s property C: there is a solution of the nth level for prenex Z if and only if ~ Z does not have property C of order n (see below, p. 544).

^d In 1920 "ist . . . ein Widerspruch" (p. 6, lines 7u-6u; "is a contradiction", above, p. 256, line 7u) is opposed to "innerhalb eines gegebenen Denkbereich für gewisse Werte der Relative erfüllt ist" (p. 7, lines 9–10; "is satisfied in a given domain for certain values of the relatives", above, p. 257, lines 6–7). In 1922 "innerhalb irgend eines Denkbereichs erfüllt ist" (p. 220, lines 5–6; "is satisfied in any domain at all", above, p. 293, line 13) is equated to "ist . . . widerspruchsfrei" (p. 222, lines 4u-3u; "is consistent", above, p. 295, line 5). In 1929the assumption that Z "is contradictory" ("ist . . . widerspruchsvoll", p. 23, line 3 of § 4) is taken to be the negation of "the assumption that Z is satisfied in a domain " ("die Annahme des Erfülltseins yon Z in einem Bereich ", p. 23. line 6u). In these papers of Skolem’s there is a constant ambiguity whether the expressions that are equated are to be taken as synonymous or as logically equivalent by a tacit argument.

^e1922, p. 221, lines 10-9u (above, p. 294, lines 1–17); 1929, p. 25, lines 4–21, p. 26, lines 8–16, and especially p. 27, lines 12-1u. The first three passages deal with a formula in Skolem normal form, the last with an arbitrary prenex formula. Note that in the last two passages no use is made of the axiom of choice.

^f1922, p. 221, line 8u, to p. 222, line 20 (above, p. 294, lines 18-7u); 1929, p. 25, line 22, to p. 27, line 11, and p. 27, line 13u, to p. 28, line 9. The first two passages deal with a formula in Skolem normal form, the last with an arbitrary prenex formula.

^g Compare these rules with Herbrand’s rules of passage (below, pp. 528–529).

^h P. 15, line 6u, to p. 16, line 4, and p. 29, line 10 to bottom of page.

ⁱ After having pointed out that their formulation of the first-order predicate calculus is not syntactically complete, that is, that it contains well-formed formulas, even closed well-formed formulas, such that neither the formula nor its negation is provable, Hilbert and Ackermann (1928, p. 68) raised the question of the completeness of the calculus in another sense: "Whether the system of axioms is complete at least in the sense that all the logical formulas that are true in every domain of individuals can actually be derived in it is a question that has not yet been solved. We can only say, in a purely empirical way, that this system of axioms has always been sufficient in all applications ". Professor Gödel has noted that at the time when these lines were written a substantial part of this problem had implicitly been solved already by Skolem in his 1922. On 14 August 1964 he wrote to the editor: "As for Skolem, what he could justly claim, but apparently does not claim, is that, in his 1922 paper, he implicitly proved: ’Either A is provable or ~ A is satisfiable’ (’provable’ taken in an informal sense). However, since he did not clearly formulate this result (nor, apparently had made it clear to himself), it seems to have remained completely unknown, as follows from the fact that Hilbert and Ackermann in 1928 do not mention it in connection with their completeness problem".

^j Compare 1958, p. 129, lines 5u-3u.

^k This proof requires the general axiom of choice: we have a set, of arbitrary cardinality, of sets of arbitrary cardinality, and simultaneous choices have to be performed. It is known that the axiom of dependent choices does not imply the general axiom of choice (for systems with urelements see Mostowski 1948; for more general systems the result can be established with the help of Cohen’s techniques (1963, 1963a, 1964). König (1936, p. 82, footnote 1) observes that his proof of the infinity lemma makes use of the principle of choice (actually, the axiom of dependent choices). But he adds: "In most applications of the infinity lemma, however, this principle can be avoided".

^l A number of remarks about Löwenheim’s and Skolem’s arguments, in particular about their use of the axiom of choice, can be found in Skolem 1938. Let us note that in that paper Skolem states the Löwenheim theorem thus: If a first-order expression is satisfiable ("réalis-able"), it is satisfiable in a denumerable domain (p. 25). Skolem also says that the results obtained by Löwenheim and him concern "a predicate logic based upon set theory" ("une logique du prédicat fondée sur la théorie des ensembles", p. 25).

¹ [Schroder introduced (1890, p. 157) the expression "identical calculus" ("identischer Kallkul") for his version of Boolean algebra. He speaks of identical sum and identical product when we would say "logical sum" and "logical product". He avoided the word "logical" here because he regards the identical calculus as "an auxiliary discipline that precedes logic proper or runs parallel . . . and is of purely mathematical nature".]

² [Skolem’s use of the two words "Beziehungen" and "Relationen" perhaps corresponds to his distinction between properties and classes, that is, between the intensional notion and the extensional notion. However, a few lines below he writes: "’Beziehungen’ oder ’Relationen’".]

³ [The German text says: "Falls eine Aussage einen Sinn hat", and here the translators had to depart from the standard translation "proposition" for "Aussage".]

⁴ It is, of course, understood that in all these expressions the logical operations are used only a finite number of times.

⁵ It is convenient to write U as an alternation of terms constructed by means of negation and conjunction (Boolean expansion).

⁶ I proved earlier (1920) that the problem whether or not a first-order proposition Z is satisfiable can be reduced to the same question for a first-order proposition Z′ in ΠΣ-form.

⁷ The word "categorical", incidentally, is used also in another sense.

⁸ [That is, a function constructed by means of the "elementary" logical operations, namely, conjunction, disjunction, and negation.]