                                         Notes prepared by
                                            Stanley Burris
                                              July 3, 2001

Clarification: Skolem

Thoralf Skolem (1887–1963)

1919 - Investigation on the axioms of the calculus of classes and on product and

sum problems which are connected with certain classes of statements. 1920 - Logico-combinatorial investigations on the satisfiability and provability of

mathematical theorems plus a theorem on dense sets. 1922 - Some remarks on the axiomatic formulation of set theory. 1928 - On mathematical logic.

The 1919 paper Skolem, like Löwenheim, adopts the notation of Schröder. The 1919 paper has three important parts:

• He gives a thorough analysis of the dependence/independence of the various axioms for the Calculus of Classes due to Peirce, as presented in Schröder, using simple structures which he can easily sketch.^{1}

• Skolem shows that by adding predicates for “has at least n elements” to the language of the Calculus of Classes he is able to eliminate quantifiers. As we mentioned Schröder devoted much effort to the elimination problem for the Calculus of Classes. However it is first in Skolem’s paper that we see it clearly formulated as taking a formula of the form ∃x ψ(x, y⃗), where ψ is quantifier-free, and finding an equivalent quantifier-free formula φ. Skolem notes that this means that every first-order formula is then equivalent to a quantifier-free formula. This is of course the modern meaning of the elimination of quantifiers.

And Skolem notes that the final form of such a quantifier-free formula is equivalent to a Boolean combination of assertions about the sizes of the constituents. Thus he has a precise handle on the expressive power of the Calculus of Classes.^{2} Because of the clarity of Skolem’s work he is often regarded as the inventor of quantifier elimination. This seems rather unfair to the pioneering work of Boole and Schröder.

1This reminds one of Löwenheim’s claim in section 2 of his paper, that he would analyze the dependence/independence of several axiom systems for the Calculus of Classes.

2Schröder had worked out some simple cases involving a couple of negated equations — and sketched a combinatorial procedure for the elimination in general. However, because

• Finally Skolem shows that one can easily translate back and forth between the first-order Calculus of Classes and first-order monadic predicate logic. In particular it follows that a statement can only assert a Boolean combination of statements about the size of the universe. Consequently if a statement in the first-order monadic predicate logic holds for all finite domains, it must hold for all domains. This proves the assertion in Löwenheim’s section three.

The 1920 paper \underline{Section 1} In this paper Skolem first introduces what is now called the Skolem normal form, namely to each first-order statement φ he associates an ∀∃ sentence ψ which is obtained via a simple combinatorial procedure, and has the essential property that φ is satisfiable on a given domain iff ψ is satisfiable on the same domain. He shows that if an ∀∃ statement is satisfiable on an infinite domain, it must also be satisfiable on a countable subdomain. Thus he has a slick proof of Löwenheim’s theorem on countermodels. His proof technique is completely different from that of Löwenheim, making use of the notion of “subuniverse generated by” which he has learned from Dedekind’s work. For model theorists it gives more information than Löwenheim’s theorem — but it requires stronger methods, namely the Axiom of Choice. Also he generalizes Löwenheim’s theorem to cover a countable set of statements. This will later be needed for the Skolem Paradox in set theory.

\underline{Section 2} Now Skolem turns to an analysis of the Calculus of Groups as presented in Schröder — in modern terminology this is just lattice theory, whereas the Calculus of Classes is the theory of power sets, as Boolean algebras. He is interested in determining the first-order consequences of the Calculus of Groups — in modern terminology he is studying the (first-order) theory of lattices.^{3} His main achievement here is to give an algorithm to decide which universally quantified statements are consequences of the lattice axioms.^{4} \underline{Section 3} In this section he looks at some consequences of first-order axioms for geometry.

he wanted to keep precise track of all the combinations involved he failed to note the nature of the final result — instead he dwelt on the incredibly complicated nature of the calculations that needed to be done.

3The fact that the Gruppenkalül is nothing other than lattice theory seems to have escaped everyone’s attention.

4We now know that the first-order theory of lattices is undecidable, so a general algo-

\underline{Section 4} Shifting gears he shows that the ℵ_{0}-categoricity of (Q, <), the rationals with the usual ordering (proved by Cantor), could be generalized by adding finitely many dense and cofinal subsets Q_{i} which partition Q.

The 1922 paper We have already spoken about the importance of this paper in the section on set theory — the recommendation that first-order properties be used, that a stronger axiom (replacement) be added, and the observation that if Zermelo’s set theory has a model, it has a countable model by the Löwenheim-Skolem theorem.

Also in this paper he returns to the proof of Löwenheim’s countermodel theorem, noting that his 1920 proof had used the Axiom of Choice; and now, in a paper on set theory, he finds it appropriate to eliminate this usage. He gives a very clean version of Löwenheim’s proof for a first-order statement (without equality). Except for the use of his normal form from the 1920 paper, it is essentially Löwenheim’s proof, the canonical construction of a countermodel.

The 1928 paper This paper is based on a talk Skolem gave earlier that year. And in it we see him describe an alternative to the ususal method of “derivation from axioms” that has become common in logic, an alternative that he suggests is superior. Actually, he only gives an example, but the idea is clearly that of Löwenheim, namely to use the countermodel construction. It is surprising that he doesn’t mention Löwenheim here.

The technique of replacing the existential quantifiers by appropriate functions symbols to get a universal sentence is clearly explained by example — and becomes known as Skolemization. He goes on to show how one can build up the elements of the potential countermodel using these Skolem functions — this will become known as the Herbrand universe. Skolem’s example does not indicate the full power of Löwenheim’s method because he does not deal with equality.

rithm would be impossible.

References

[1] Th. Skolem, Untersuchung über die Axiome des Klassenkalküls und über Produktations– und Summationsprobleme, welche gewisse Klassen von Aussagen betreffen. Videnskabsakademiet i Kristiania, Skrifter I, No. 3, 1919, pp. 37. Also in “Selected Works in Logic by Th. Skolem”, ed. by Jens Erik Fenstak, Scand. Univ. Books, Universitetsforlaget, Oslo, 1970.

[2] Th. Skolem, Logisch-kombinatorische Untersuchungen über die Erfüllbarkeit und Beweisbarkeit mathematischen Sätze nebst einem Theoreme über dichte Mengen. Videnskabsakademiet i Kristiania, Skrifter I, No. 4, 1919, 1–36. Also in “Selected Works in Logic by Th. Skolem”, ed. by Jens Erik Fenstak, Scand. Univ. Books, Universitetsforlaget, Oslo, 1970, pp. 103–136. [The first section is translated in: From Frege to Gödel, van Heijenoort, Harvard Univ. Press, 1971, 252–263.]

[3] Th. Skolem, Einige Bemerkung zur axiomatischen Begrundung der Mengenlehre. Proc. 5^{th} Scand. Math. Congr. Helsinki, 1922, 217–232. [translation in From Frege to Gödel, van Heijenoort, Harvard Univ. Press, 1971.]

[4] Th. Skolem, Über die mathematische Logik. NMT 10, 1928, 125–142. 1928. [translation in From Frege to Gödel, van Heijenoort, Harvard Univ. Press, 1971.]