We prove the Ehrenfeucht-Mostowski theorem by ultraproducts, with no application of Ramsey theorem. Expand the infinite structure by Skolem functions, choose distinct elements , and choose a nonprincipal ultrafilter on . Let be the desired total index order and put .
For every finite ordered subset , define an ultrafilter on by the ordered Fubini product of ultrafilters: a set belongs to exactly whenHere means , with the quantifiers nested in the displayed order. The resulting collection is an ultrafilter, by induction using the ultrafilter laws for negation and conjunction. For , the inverse image of under coordinate projection belongs to exactly when : quantifiers on unused coordinates leave a truth value unchanged.
Consequently there is a well-defined ultrafilter on the Boolean algebra of finite-coordinate cylinders in , declaring a cylinder large by this test. Coherence proves finite intersection closure and ensures that the empty cylinder is not large. Extend its generated filter to an ultrafilter on all subsets of . Form the ultrapower , and for let be the class of .
If , the coordinate equality test belongs to no corresponding two-coordinate product ultrafilter: for every value of the outer coordinate, the inner equality set is a singleton, excluded by nonprincipality. Hence the are distinct. For any first-order formula and any , the Łoś theorem givesThe right side is independent of the actual increasing index tuple, so the form an order-indiscernible sequence. Constant functions embed elementarily into . Take the Skolem hull of the generators. The Tarski-Vaught test gives an elementary substructure, and transporting terms along an index-order automorphism gives a well-defined automorphism of the hull, with inverse obtained by transporting along the inverse index automorphism. Equality of term representations is preserved by indiscernibility. This is the indiscernible and automorphism conclusion of Ehrenfeucht–Mostowski, obtained entirely from ultrafilters and Łoś's theorem. The ordered Fubini products need not be symmetric; order indiscernibility is exactly what their coherence supplies.
Use the bounded successor characterization of finite ordinals. Let assert that is transitive, each of its members is transitive, and any two members are equal or comparable by membership. This is a bounded first-order formula; foundation makes its linear membership order well-founded, so it is precisely the Von Neumann ordinal predicate. Defineand putFor an ordinal, having a greatest member says exactly . The displayed definition makes no reference to an infinite inductive set or to ; all quantifiers are bounded within the candidate and its members. Occurrences of can also be expressed as , so no unbounded quantifier is hidden in empty-set notation.
Every usual natural number satisfies this predicate, by induction: it is a finite ordinal, and every nonzero initial segment is a successor. Conversely, suppose an ordinal is not a usual natural number. Ordinal comparability gives . If , it has no greatest member, contradicting . If , then has no greatest member, contradicting the corresponding bounded requirement on members of . Hence holds exactly for the usual natural numbers. The axiom of infinity and separation therefore collect this class as the usual set . This is a bounded definition of membership in the natural-number class; it does not claim that the infinite set itself can be produced without the infinity axiom.
An inner model of ZF is a transitive class containing all ordinals and satisfying ZF with the inherited membership relation. The “all ordinals” requirement is important: an arbitrary transitive set model or a rank segment is not an inner model in this sense.
Every such inner model contains the ambient constructible universe . Here is the reason. Inductively . The zero stage is the same empty set. If the stages at agree, satisfaction for the common set structure is absolute: atomic first-order formulas agree, Boolean operations agree, and quantified variables range over the identical set. The codes of finite first-order formulas are also the same because a transitive model of ZF has the actual natural numbers. Consequently definability with parameters from produces exactly the same subsets in both models, so their successor constructible stages agree. At a limit ordinal both constructions take the union of the same earlier stages. This proves agreement at every stage and hence .
The constructible universe theorem provides models of ZF satisfying and the axiom of choice, whenever ZF is consistent. In such a universe any inner model of ZF satisfiesso and it also satisfies choice. ThereforePassing to proves the consistency of choice, but the same downward method cannot prove its negation from an arbitrary starting model: it has no possible output when the starting universe is constructible. This is the precise obstruction intended in an inner-model independence argument. It is not a claim that every inner model of every choice universe satisfies choice; symmetric submodels of suitable forcing extensions can fail choice, and that method first changes the ambient universe.
Articles by others on the same topic
There are currently no matching articles.