Thoralf Skolem

Thoralf Skolem

Logician and mathematician · 1887–1963 · Norway

A formal theory, the structure interpreting it, and an external description of that structure are different objects. Skolem's work makes those distinctions unavoidable. It also gives a practical tool for automated reasoning: replace existential choices by new function symbols while preserving satisfiability.

Historical bearings

Thoralf Skolem was born on 23 May 1887 and died on 23 March 1963. He studied in Kristiania, worked as an assistant to the physicist Kristian Birkeland, and studied in Göttingen during 1915–1916. He became a docent and a member of the Norwegian Academy of Science and Letters in 1918. His doctorate followed in 1926. His work included lattices, number theory, first-order logic, and arithmetic. The academy date was not 1930, and the physics assistantship should not be reassigned to Axel Thue. MacTutor biography

Skolem developed results now associated with the Löwenheim–Skolem theorems, examined the interpretation of axiomatic set theory, and constructed nonstandard arithmetic models. These achievements are connected by a discipline of separating what a formal language can express from what an observer assumes its symbols must mean.

A model is an interpretation

A first-order language specifies symbols for relations, functions, and constants. A structure supplies a nonempty domain and interpretations for those symbols. A sentence is true in a structure according to these interpretations and quantifiers that range over its domain. A theory is a set of sentences; its models satisfy all of them.

For a countable first-order language, a theory with an infinite model has a countably infinite model. The countability condition is not decoration. If a language contains uncountably many constants and a theory requires every pair of distinct constants to denote different objects, a countable model is impossible. More general Löwenheim–Skolem statements account explicitly for the language's cardinality. The theorem and its setting

Different models of one theory need not agree on every sentence. They agree on the theory's axioms and consequences, but an incomplete theory may leave further sentences unsettled. Likewise, an arbitrary model of Peano arithmetic need not satisfy every sentence true in the standard natural numbers. Models of true arithmetic, the full first-order theory of the standard natural numbers, satisfy that stronger requirement.

Worked mechanism: choose the right dependencies

This is an original example in modern notation. Consider

∀x ∃y ∀z ∃w R(x,y,z,w).

The value chosen for y may depend on x, but it must work before z is chosen. The later w may depend on both x and z. Introduce fresh symbols f and g:

∀x ∀z R(x,f(x),z,g(x,z)).

These formulas are equisatisfiable in their respective languages. A model of the transformed formula gives a model of the original when the new symbols are forgotten. In the other direction, satisfying witnesses can be selected to interpret the new functions, in the usual classical metatheoretic setting. This is not equivalence for every arbitrary interpretation of f and g. Skolemization lecture

Take integer arithmetic and define R by the two conditions y=x+1 and w=y+z. Then f(x)=x+1 and g(x,z)=x+1+z work. At x=4,z=9, the witnesses are y=5 and w=14. At the same x but z=0, y stays 5 while w becomes 5. Allowing y to change with z would incorrectly weaken the dependency requirement of the original quantifier order.

Replacing y by one constant would go the other way: it would impose an unjustified restriction. No single integer can equal x+1 for every x. A transformation can therefore go wrong either by allowing too much dependency or by allowing too little.

The symbol f is not automatically executable code. A model interprets it as a mathematical function; a proof that such an interpretation exists is not necessarily an algorithm for computing it. In the example we supplied an explicit computable formula, which is additional information.

Why Skolem's paradox is not a contradiction

Assume that first-order ZFC has a model. Because its language is countable, it then has a countable model M. Inside M there is an object that M regards as uncountable. From outside, the collection of domain elements that M regards as members of that object is countable, since it is contained in M's countable domain.

The two assertions quantify over different collections of candidate functions. Internally, “countable” requires an appropriate function represented inside M. An external enumeration of the relevant domain elements need not be represented by any such object. For a general model, even membership is an interpreted relation, not automatically the observer's actual set membership. The paradox disappears once these semantic levels are kept separate. This argument does not prove that ZFC has a model or that it is consistent. Detailed account

A useful software analogy is a database query ranging over stored rows: an external object not stored in the database is unavailable to its quantifier. This is only an analogy. A finite database is not a model of ZFC, and database permissions do not explain the mathematics by themselves.

Arithmetic terminology

Skolem's work on primitive recursive arithmetic uses explicitly defined functions and restricted forms of induction. Do not identify it with “Skolem arithmetic,” a name commonly used for the first-order theory of natural numbers with multiplication alone. The two subjects have different signatures and purposes. Historical arithmetic work, Research usage of Skolem arithmetic

Exercises

1. Skolemize ∃u ∀x ∃y ∀z P(u,x,y,z) using the standard dependency rule. Explain why u cannot depend on x and why y need not depend on z. Construct a counterexample to replacing y by a constant using P(u,x,y,z) defined as y=x+u over integers.
2. A colleague says, “A countable model of set theory contains a function listing its reals, because I can list the whole domain.” Identify the invalid step. Does the model theorem prove that set theory is consistent?
3. Add a new constant c to true arithmetic and the sentences c>0,c>1,c>2,.... Explain why every finite subset is satisfiable, what compactness implies, and why the resulting c is not a standard natural number. State where an infinite collection of sentences enters the argument.

Compare your reasoning with the worked solutions

1. Use a fresh constant a and a fresh function f: ∀x∀z P(a,x,f(x),z). The first witness is selected before any universal variable; y may depend on x and the fixed a, which can be built into the interpretation of f. It cannot depend on the later z. In the arithmetic example choose a=2 and f(x)=x+2. A constant y=b cannot work for both x=0 and x=1, which would require b=2 and b=3 simultaneously.
2. External listing does not imply that an internal object represents that listing as a function with the model's required properties. Internal quantifiers cannot automatically range over every externally definable relation. The theorem is conditional on the existence of a model; it does not establish that condition for ZFC. Confusing external access with internal representation causes both errors.
3. A finite subset mentions only finitely many lower bounds. Interpret c as a standard integer larger than all those bounds, keeping the usual natural-number structure. Compactness then yields a model satisfying the entire infinite set. Its c exceeds every standard numeral, so it cannot correspond to any standard natural number: any such n fails c>n. The compactness step, not a single giant finite conjunction, accommodates all bounds at once. Because true arithmetic was included, the reduct agrees with the standard structure on every first-order arithmetic sentence, despite having a nonstandard element.