Supplementary Text Topics
Skolem, like Löwenheim, adopts the notation of Schröder. The 1919 paper has three important parts:
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. 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.
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.
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. His main achievement here is to give an algorithm to decide which universally quantified statements are consequences of the lattice axioms.
In this section he looks at some consequences of first-order axioms for geometry.
Shifting gears he shows that the -categoricity of (Q,<), the rationals with the usual ordering (proved by Cantor), could be generalized by adding finitely many dense and cofinal subsets which partition Q.
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
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.
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.
Up: Supplementary Text TopicsMon Feb 3 18:32:11 EST 1997