The Norwegian mathematician Thoralf Skolem (1887–1963) made extensive contributions to the development of logic, maintaining a steady output of important papers from 1920 until his death. Skolem's first major result was an extension of the above-mentioned theorem of Löwenheim that if a formula of the first-order functional calculus (with identity) is valid in a denumerably infinite domain, it is valid in every nonempty domain and that, equivalently, if such a formula is satisfiable at all, then it is satisfiable in a domain comprising at most a denumerable infinity of elements. In 1920, Skolem generalized this theorem to the case of classes (possibly infinite) of formulas, establishing that if a class of formulas is simultaneously satisfiable, then it is satisfiable in a denumerably infinite domain. Skolem's proof makes use of the axiom of choice and the Skolem normal form of a formula—a type of prenex normal form in which no...