Löwenheim’s theorem
Lwenheim’s theorem
The theorem, first proved by Lwenheim, that if a formula of the pure functional calculus of first order (see Logic, formal 3), containing no free individual variables, is satisfiable (see ibid.) at all, it is satisfiable in a domain of individuals which is at most enumerable. Other, simpler, proofs of the theorem were afterwards given by Skolem, who also obtained the generalization that, if an enumerable set of such formulas are simultaneously satisfiable, they are simultaneously satisfiable in a domain of individuals at most enumerable.
There follows the existence of an interpretation of the Zermelo set theory (see Logic, formal, 9) — consistency of the theory assumed — according to which the domain of sets is only enumerable; although there are theorems of the Zermelo set theory which, under the usual interpretation, assert the existence of the non-enumerable infinite.
A like result may be obtained for the functional calculus of order omega (theory of types) by utilizing a representation of it within the Zermelo set theory. It is thus in a certain sense impossible to postulate the non-enumerable infiniteany set of postulates designed to do so will have an unintended interpretation within the enumerable. Usual sets of mathematical postulates for the real number system (see number) have an appearance to the contrary only because they are incompletely formalized (i.e., the mathematical concepts are formalized, while the underlying logic remains unformalized and indefinite).
The situation described in the preceding paragraph is sometimes called Skolem’s paradox, although it is not a paradox in the sense of formal self-contradiction, but only in the sense of being unexpected or at variance with preconceived ideas. — A.C.
Th. Skolem,
Sur la portee du theoreme de Lwenheim-Skolem, Les Entretiens de Zurich sur les Fondements et la Methode des Sciences Mathematiques, Zurich 1941, pp. 25-52.