A partial computable function is the function computed by a finite program, with an undefined value when its computation never terminates. A total computable function terminates on every input. Fix an effective enumeration of the partial computable functions, with a universal partial computable function . Composition, primitive recursion and unbounded minimization give a machine-independent description of this class. Unbounded minimization is allowed to diverge. The S-m-n theorem permits parameters in a program to be specialized effectively: an algorithm described uniformly in has an index obtained computably from .
The halting set is computably enumerable: simulate all computations in parallel and enumerate each index whose diagonal computation terminates. It is not a computable set. Otherwise the program which terminates exactly when the proposed decision procedure says its own diagonal computation does not terminate gives a contradiction. There is also no effective enumeration consisting exactly of all total computable functions: from such an enumeration the total computable function differs from every listed function. Thus the effective enumeration of partial programs cannot be replaced by a decidable catalogue of total ones.
For the Rice theorem, let be a nontrivial property of partial computable functions, depending on the computed function rather than the program text. First suppose the nowhere-defined function is not in , and choose a program computing some . Uniformly in , define a program which, on input , first waits for to terminate and then runs the computation of . The S-m-n theorem gives a computable index map , andConsequently a decision procedure for membership in would decide the halting set. If the nowhere-defined function belongs to , apply the same argument to its complement. Every nontrivial extensional property of partial computable functions has an undecidable index set. Syntactic properties of program descriptions are outside this assertion, and the theorem concerns unrestricted program indices, not merely an assumed list of terminating programs.
Here is an explicit Jockusch triple coloring computing the halting set. Choose computable increasing finite stages with union . For , putThis is a computable colouring. An infinite monochromatic set cannot have color : fix its first element and choose two later elements beyond the stage at which stabilizes. Their triple has color .
Suppose is infinite and homogeneous of color . To decide whether using , find with , and then with . For every above , homogeneity gives . Such are unbounded, so . Testing therefore decides . Hence every homogeneous set computes the halting set, and there is no infinite recursive monochromatic set. The infinity qualification is essential: finite homogeneous sets are recursive.
Work in a ground first-order model of set theory satisfying ZF, and let be a definable bijection of its universe, whose inverse is also definable. Write and replace membership byIn this Rieger-Bernays permutation model, an object having prescribed extension is represented by . The Axiom schema of replacement in the ground model guarantees that images of sets under and are sets. The axiom of extensionality follows from injectivity of ; the new empty set is , and the new pair of is .
For the Axiom of union and Axiom of power set, representatives are respectivelyIndeed, is an -subset of exactly when . Translate every first-order formula by replacing membership with membership in . Ground separation then forms each desired subextension of , and ground replacement forms each functional image; applying supplies its representative. To verify the axiom of infinity, define by ground recursionThen is an -inductive set. Thus every ZF axiom except possibly the Axiom of foundation survives.
Interchange two distinct objects and , fixing everything else. Then , so is a Quine atom: internally . The nonempty set has no member disjoint from itself, violating the Axiom of foundation. The original membership model satisfies that axiom. Foundation is therefore relatively independent of the other ZF axioms.
A full Rieger-Bernays permutation model of a choice model still satisfies the axiom of choice: choose an old member of each nonempty extension and encode the resulting choice graph with the new ordered-pair operations. To obtain failure of choice, an additional restriction by symmetries is necessary.
Start instead with ZFC and use the definable permutation interchanging every with . These transpositions are disjoint and produce an infinite set of Quine atoms. Inside the resulting membership model build the cumulative universe over , closing at successive stages under sets of previously constructed objects, represented by . Atomic objects are kept as the designated base objects; for . Every permutation of extends recursively to an automorphism of this universe, with the atomic self-loops fixed by the recursive convention.
An object has finite support if every permutation fixing some finite pointwise fixes it. Retain the objects which have finite support and whose members recursively also have finite support, interpreting the atomic self-loops as the base case. This is the hereditarily finite-supported Quine-atom model. It is transitive for the new membership relation. Extensionality is inherited. Pairs and unions have supports contained in the union of the finitely many relevant supports. For a supported set , the collection of all retained subsets of is a ground set, by the full model's power set axiom, and is fixed by every permutation fixing a support of . Its members are retained, so this collection supplies the internal power set. A first-order formula with retained parameters is invariant under their common stabilizer. Consequently its definable subset of , and the range of a functional relation on , have that same finite support; ground separation and replacement first ensure that they are sets. The pure natural-number hierarchy supplies infinity. These arguments verify all of ZF except Axiom of foundation, which fails at the Quine atoms.
The family of all two-element subsets is retained and has empty support. If it had a retained choice function , choose two distinct Quine atoms outside a finite support of . The transposition of fixes and fixes the unordered pair , but moves either possible value . This is impossible. Thus ZF without Foundation has both choice models and models in which Choice fails, relative to the usual consistency assumption. The construction also explains why twisting membership alone was insufficient.
Use rooted-tree homeomorphic embedding: edges may be stretched into downward paths, different child branches stay disjoint, and the source root may map to any target vertex. Write for this relation. More generally allow labels in a well-quasi-ordering and require every source label to be at most its image label. We prove this labelled version, which includes the unlabelled case by taking one label.
First, every infinite sequence in a well-quasi-ordering has an infinite nondecreasing subsequence. In every infinite set of indices there is an index with infinitely many later successors above its value. Otherwise repeatedly discard the finitely many successors of each chosen index, obtaining a bad sequence. Applying this observation successively within the infinite successor set produces the required subsequence.
We also need the Higman lemma, and prove it here. If finite words over admitted a bad sequence, choose one with each word of least possible length among choices permitting a bad continuation of its fixed prefix. No word is empty. Write , and extract indices with . The sequenceis bad: an earlier embedding into some would embed into , while together with would give . This contradicts the minimal length of , since is shorter. Hence finite words are well-quasi-ordered under subsequence embedding with increased labels.
Now suppose labelled rooted trees admitted a bad sequence , chosen minimally by number of vertices at each successive position. Let consist of all immediate child subtrees of all the , with the inherited labels. We claim is a well-quasi-ordering. Otherwise take a bad sequence of members of . Only finitely many distinct rooted trees occur among the children of any finite initial list of , so, by discarding terms and selecting a subsequence, we may arrange its members to come from strictly increasing parent indices . Thenis bad. A prefix rooted tree embedding into would embed into its parent ; embeddings between the are excluded by their choice. But has fewer vertices than , contradicting minimality. This proves the claim.
List the child subtrees of each in any order. By the Higman lemma these child lists are well-quasi-ordered. Extract an infinite subsequence with nondecreasing root labels, and then compare two child lists on that subsequence. Their subsequence embedding gives distinct target child branches into which the source child subtrees embed. Map the source root to the target root and join each embedded child root to it by the corresponding downward path. The paths are disjoint except at the root, and labels increase. Thus for some , contradicting badness. This proves Kruskal's tree theorem and its labelled version. If root preservation is required, mark the root with a special label incomparable with all ordinary labels; the same proof then forces root to map to root.
For Friedman's finite form of Kruskal's theorem, fix and suppose there are arbitrarily long bad lists satisfying for . Make a finite bad-sequence tree whose nodes are these lists, using one representative of each finite rooted-rooted tree isomorphism type. At each position only finitely many choices satisfy the size bound, so the rooted tree is finitely branching. An infinite path exists: at every stage choose a child having extensions of arbitrarily large length, which must exist because there are finitely many children. The path is an infinite bad sequence, contradicting Kruskal's tree theorem. ThereforeThe identical argument works with finitely many labels and any fixed finite size bound at each position.
The axiom of determinacy, abbreviated AD, asserts that every length- infinite game of perfect information in which the two players alternately choose natural numbers is determined. For a payoff set , player I wins exactly when the completed play belongs to . A strategy specifies the next move at every finite position where its player is to move; determination means that one player has a winning strategy.
Finite games are determined by backward induction, choosing the least move leading to a guaranteed win when several are available. In ZF one can also prove open determinacy, hence determinacy for closed payoffs. Here is the full open-payoff argument. Let be the finite positions with , so reaching ensures a win for I. Starting with , repeatedly add an I-position with some child already in , and a II-position with every child already in ; take unions at limit stages. This increasing process stabilizes because the set of finite positions is a set: continuing strict enlargement through its Hartogs number would choose distinct new positions, contradicting that bound. Assign to each admitted position its least entry stage.
At an I-position in the final , choose the least child of smaller entry stage. At a II-position in , every child has smaller entry stage. A play following this I-strategy cannot remain outside forever, since that would give an infinite strictly descending sequence of ordinals. It reaches and wins. Outside , every child of an I-position remains outside , and a II-position has at least one child outside . Player II chooses the least such child. The play never reaches , so it cannot belong to the open set . The initial position is either inside or outside , proving determination. For a closed payoff apply the same argument to the open complementary payoff for the other player, with the appropriate player assigned to each level. None of these strategies needs a choice principle because moves are natural numbers and least available moves are definable.
To refute simultaneous AD and the axiom of choice, assume choice and well-order all strategies of either player in length . There are exactly strategies for each player, and any fixed strategy has exactly compatible plays, since the opponent's successive moves are arbitrary. At stage , choose two fresh plays: compatible with I's th strategy, and compatible with II's th strategy. Fewer than plays have previously been excluded, so this is possible even if is singular. Put . No ever enters . I's th strategy loses on , and II's th strategy loses on . Thus this game has no winning strategy for either player, and
All assertions of independence below are relative consistency assertions. We construct structures satisfying the other ZF axioms but falsifying the indicated axiom; an ordinary model of ZF supplies the positive side. The convenient ground theory is ZFC, which has the same consistency strength as ZF by the constructible universe theorem.
For the Axiom of union, put and use the hereditarily locally small membership modelIt is a transitive class. The condition requires each individual set in the membership ancestry to have size below ; it does not require its entire transitive closure to have size below . Extensionality and foundation are inherited. Pairs and subsets of members remain in the class, giving pairing and separation, and witnesses infinity. For , the actual also belongs to : if , then by the strong-limit property, while every subset of and every member further below it remains locally small. This verifies the full power set axiom. If an internally definable functional relation has domain , ground replacement, applied to the relativized first-order formula, gives its range . Since and every value is already in , its range is also locally small. Thus every replacement instance holds.
However, belongs to : its members have cardinalities , and their members are smaller still. Its actual union is , of cardinality , which is not in . Transitivity makes any internal union witness equal to this actual union. Hence Union fails while all the other ZF axioms hold.
For the Axiom of power set, use the hereditarily countable sets in the ground choice universe. This is transitive and contains . Pairs, subsets and unions have countable transitive closure. For replacement, a functional image of a countable domain is countable, and the union of countably many countable transitive closures is countable; hence that image is again hereditarily countable. These observations, with inherited extensionality and foundation, verify all the remaining axioms. Every real, viewed as a subset of , belongs to . A power-set witness for would therefore contain every such real, but a hereditarily countable set has only countably many members, whereas is uncountable by Cantor's theorem. Power set fails.
For the Axiom schema of replacement, use with actual membership. This limit-rank structure contains and is closed under pairs, unions and power sets: every relevant finite increase in rank stays below . A separated subset has rank no higher than that of the original set. Extensionality and foundation are inherited. The internally definable functionis obtained by successive power-set operations starting with the parameter . Each finite iteration, including its finite history, belongs to the structure. Its range has rank and is not an element of . Thus the replacement instance for this first-order formula fails, although every other ZF axiom holds.
For the axiom of extensionality, take the well-founded cumulative set universe over two distinct urelements, and forget the predicate distinguishing urelements from sets. Each urelement has no members, just as the ordinary empty set has no members, so extensionality fails. Every other axiom survives in this pure membership language. Pairing, union, separation and replacement are witnessed by the corresponding ordinary sets of urelements and sets; foundation follows from their well-founded ranks, and the pure supplies infinity. Here foundation is written with “has a member” as its nonemptiness antecedent, and disjointness means having no common member. Formulations using inequality to one designated empty object are not equivalent after removing extensionality. There is also one necessary adjustment to power set: an urelement is vacuously a subset of every object because it has no members. Thus the power-set witness for is the ordinary set of all usual subsets of its extension, together with both urelements. This is still a set, and contains exactly the objects satisfying the unrestricted subset first-order formula. Consequently the countermodel falsifies Extensionality alone, without silently weakening Power set to sets only.
Finally, the hereditarily finite sets satisfy extensionality, foundation, pairing, union, power set and separation. Every functional image of a finite domain is a finite set of hereditarily finite objects, hence also belongs to , giving all replacement instances. No finite set contains and is closed under successor: it would then contain every finite von Neumann ordinal. Infinity fails while the remaining axioms hold.
Let be an externally countable model of ZFC, and let . In form the forcing orderThis is the finite-function collapse to countable size. For every and , the internal setsare dense: extend a finite function by assigning a missing input, and use a fresh input to put any required value in its range.
Externally enumerate all the dense subsets of which recognizes as dense. There are only countably many, because is countable. Recursively choose in the th such dense set and let be the upward closure of this descending chain. This produces a generic filter over . By the forcing theorem, its generic extension satisfies ZFC. The canonical forcing name is forced to be a function with domain and range : the dense sets and ensure exactly these assertions. ThereforeIts new first uncountable ordinal is accordingly different from .
For a transitive , ordinary evaluation of names gives the familiar literal extension. The question only assumes a countable model, so one must also cover externally ill-founded models. In that case use the quotient of the internally defined forcing names by forced equality modulo , with membership defined by forced membership. The internal forcing identities and the forcing theorem hold in and give a well-defined first-order structure satisfying every standard ZFC axiom. Check names embed the original membership structure, so identify their images with . Its domain is a quotient of a subset of the countable domain of , hence is externally countable. Thus the required extension exists even without assuming transitivity. It is a membership extension, not an elementary extension: the assertion that the parameter is uncountable changes truth value.
For nonempty first-order structures in a common language and an ultrafilter on , identify product functions byThe ultraproduct has these equivalence classes as elements. Functions are interpreted coordinatewise, and a relation holds of classes exactly when its coordinatewise truth set belongs to . Closure under finite intersections makes these interpretations independent of representatives.
The Łoś theorem assertsProve it by induction on first-order formulas. Atomic first-order formulas hold by the definitions and induction on terms. Conjunction uses intersections, and negation uses the fact that an ultrafilter contains exactly one of a set and its complement. For an existential first-order formula, a product witness gives a coordinate witness on a -large set. Conversely, on the -large set where a coordinate witness exists, choose one in each factor, and choose arbitrary values elsewhere. Its class is a product witness by the induction hypothesis. This is the only witness-selection step; the surrounding argument is made in a choice metatheory. The special case with all factors equal is an ultrapower, and constant functions give an elementary embedding.
Here is a direct compactness theorem proof. Suppose every finite subset of a theory has a model. Index factors by the finite subsets , choosing . For finite , the cone is nonempty, and . Extend the generated proper filter to an ultrafilter . For every sentence , its truth set contains , so the Łoś theorem gives . Finite satisfiability therefore implies satisfiability, directly from the ultraproduct construction rather than from a syntactic completeness argument.
For saturated models, a structure is -saturated if every complete type over fewer than parameters is realized. A useful concrete case is countable saturation of a nonprincipal ultraproduct over omega. In a countable language, enumerate any finitely satisfiable type over countably many parameters as , and represent its parameters by product functions. By the Łoś theorem, the set of coordinates where the first first-order formulas have a simultaneous witness belongs to the nonprincipal ultrafilter . PutThese are decreasing -large sets. At coordinate , let be the largest with , or zero if none exists, and choose a witness for the first first-order formulas. For fixed , every coordinate in has , so the resulting product function satisfies on a -large set. Its class realizes the whole type. Thus such an ultraproduct is -saturated.
There is also an existence construction at every prescribed degree . Given an infinite model , choose a regular cardinal and construct an elementary chain . At a successor stage, add a new constant for a realization of every type over every subset of of size below , together with the elementary diagram of . Every finite part is satisfiable: only finitely many types and finitely many first-order formulas from each are involved, and each finite type fragment has a witness in . Compactness therefore supplies a simultaneous elementary extension. At limits take unions. To justify elementarity of a union, any existential first-order formula with parameters in an earlier stage has a witness in that stage whenever it has one at a later stage, by elementarity; this is the Tarski-Vaught test.
Any fewer-than- parameters of occur together in some , by regularity of . A type over them which is finitely satisfiable in is finitely satisfiable in , again by elementarity, and was realized in . Hence every infinite structure has a -saturated elementary extension for any prescribed cardinal . No bound on the size of this extension is asserted; full saturation at the model's own cardinality has additional cardinal-arithmetic issues.
For the Ehrenfeucht-Mostowski theorem, start with an infinite structure and a total order . Choose a Skolem expansion , and adjoin constants for . Require the elementary diagram of , distinctness of these new constants, and the order-indiscernible sequence schema: any two increasing tuples of the of the same length satisfy the same first-order formulas in the expanded language. Every finite fragment mentions finitely many new constants and finitely many first-order formulas. Enumerate a countably infinite subset of . For each of the finitely many first-order formulas, color its increasing tuples by its truth value in , including whatever fixed parameters occur in the fragment. Successive applications of the infinite Ramsey theorem leave an infinite subset homogeneous for all these colorings. Assign the finitely many new constants to distinct elements of this subset in their index order. Their finite indiscernibility requirements and the elementary diagram are then simultaneously satisfied.
The compactness theorem supplies an elementary extension containing the required distinct indiscernibles. Their Skolem hull is an elementary substructure: an existential first-order formula true of its elements has its chosen Skolem-function witness in the hull, so the Tarski-Vaught test applies. Any order automorphism of acts on this hull byIndiscernibility makes this well defined, since every equality of two term representations is preserved. The same argument preserves every first-order formula; the inverse is given by . Thus it is an automorphism, uniquely determined in the language of the chosen Skolem expansion by its values on the generators. This proves both the indiscernible-model and automorphism forms of the Ehrenfeucht-Mostowski theorem. Uniqueness is not claimed for automorphisms of the reduct which need not preserve the chosen Skolem functions.
For simple typed set theory with atoms, write for the set predicate at sort . Members have sort one lower; urelements have no typed members, extensionality applies to sets, and every well-typed first-order formula defines a set at the next sort. Typical ambiguity adds for each closed sentence, where raises every sort by one. We prove finite satisfiability using Ramsey theorem, rather than assuming that adjacent sorts have the same cardinality.
Let . If , then . For increasing integers , interpret sort by , interpret by the objects of , and interpret adjacent-sort membership by actual membership restricted to these designated sets. All other objects of a sort are typed urelements. Every subset of is a designated set in , so comprehension holds for every first-order formula, including first-order formulas with quantifiers and parameters at other sorts. Two designated sets with the same members are equal, while the other objects have no typed members. Thus this is a full model of the typed axioms for every increasing sequence of levels. The extra preceding level gives a consistent interpretation of the bottom set predicate as well.
Take finitely many ambiguity sentences and let bound their highest sort before raising. Color increasing -tuples by the vector of truth values of these sentences in the corresponding finite sorted structure. There are finitely many colors. The infinite Ramsey theorem supplies an homogeneous set of indices. Choose the level sequence from it. The sentence is evaluated in the window , while is evaluated in the next window ; homogeneity makes their truth values equal. Sentences using fewer sorts simply ignore the unused final levels. Thus every finite family of ambiguity axioms has a model satisfying all the typed axioms. Apply many-sorted first-order compactness theorem to obtainThis is a relative consistency construction in the ordinary set-theoretic metatheory. Allowing urelements is essential here: skipping ranks leaves objects outside the represented power sets, and those objects must be permitted as urelements.
An uncountable cardinal is a measurable cardinal if there is a nonprincipal -complete ultrafilter on : intersections of fewer than members of remain in . Such an ultrafilter is uniform. No singleton belongs to it, and intersecting the complements of fewer than singletons shows that no set of cardinality below belongs to it.
Form the ultrapower of the universe by , with classes of functions , and exactly when . The Łoś theorem proves that the map taking to the constant function with value is elementary. The ultrapower relation is well-founded: from an infinite descending sequence , countable completeness gives a coordinate satisfying all the membership relations, producing an actual infinite descending membership sequence and contradicting foundation. It is also set-like. Predecessors of can be represented by functions whose value at lies in ; these functions form a set. The Mostowski collapse theorem therefore gives a transitive class and an elementary embeddingThe usual class-ultrapower notation is understood via set-sized representatives and this set-like collapse.
For , any function into is constant on a -large set: if none of its fewer-than- fibers belonged to , intersect their complements to get the empty set in . Consequently every member of the ultrapower ordinal represented by the constant is represented by a constant ordinal below . Induction on now gives .
On the other hand the identity function represents an ordinal below . For every , the tail belongs to , so the collapsed ordinal is above . HenceThis proves nonidentity explicitly. The collapsed identity class is at least ; it need not equal unless an additional normality convention is imposed on .
Conversely, an elementary embedding into a transitive class with critical point yieldsFor the converse use the usual amenability assumption on the class embedding, so this collection is a set. Since , exactly one of and contains , proving the ultrafilter condition. Singletons are excluded because . If and for , then fixes and every index below it, giving ; the intersection still contains . Thus is -complete and is measurable.
In particular the first moved ordinal is a strongly inaccessible cardinal. If , partition into fewer than bounded intervals. Each is too small to lie in , contradicting completeness. Thus is regular. If for some , choose distinct subsets for . For each , choose the -large side of the question . Intersect these fewer-than- large sides. The intersection belongs to , but all its indices have identical , so it contains at most one index, contradicting nonprincipality. Therefore for every , as required.
For an infinite cardinal put and . The Erdős-Rado theorem for finite arities isThe partition relation requires a homogeneous subset of order type for every coloring of -element subsets by at most colors. In particular it gives uncountable homogeneous sets. The case is the infinite pigeonhole principle: a union of sets each of size at most cannot have size .
We give the induction step by a closed elementary-submodel construction of an end-homogeneous sequence. Let be infinite, , and with . Choose a sufficiently large regular and an elementary submodel with , all ordinals below in , , and closure under externally given sequences of length at most . To construct it, take successive elementary Skolem-hull closures, at each step including all such sequences from the preceding stage. Cardinality stays because . In the final union every sequence of length at most has all its entries in some earlier stage, by regularity of , and so was included at the next stage.
Put . Regularity of gives , and since otherwise its successor would contradict the definition of the supremum. Recursively, for choose above all earlier and satisfyingThere are at most constraints. Their parameters and their colors belong to , and closure puts their complete code in . The point witnesses their simultaneous satisfiability in ; elementarity supplies a witness in . This gives an increasing end-homogeneous sequence of length : on it, the color of an -tuple depends only on the first entries.
For the induction from arity to , take and . Color the -tuples of the resulting sequence by their common color with a later point, equivalently by their color with . Its index order has type , so the induction hypothesis supplies a homogeneous index set of type . The original -tuples on those indices have that same color. This completes the proof without substituting the theorem's name for its induction.
A useful ordinal partition-bound function isIt is total: choose an infinite cardinal with ; the pairs case supplies with the required homogeneous order type for all these color numbers. It is nondecreasing and satisfies . Start iterating and take a supremum at a limit stage. If the increasing iterates do not attain that supremum, then for every some iterate satisfies , andIf the iterates have already stabilized, their supremum is a fixed point directly. Thus the relevant nontrivial case is an uncountable cardinal closed below itself under .
Such closure implies that is a strong limit. Suppose is infinite and . Take distinct binary strings of length , indexed in order by , and color a pair by its first differing coordinate. No three strings are homogeneous: three bits cannot be pairwise different at the same coordinate. Closure would give , and its restriction would have a homogeneous subset of order type in colors, a contradiction. Hence ; finite exponents are harmless for an uncountable .
Use the usual tree property: every set-theoretic tree of height with nonempty levels of cardinality below has a cofinal branch. For an uncountable cardinal satisfying this all-set-theoretic trees convention, must be regular. If it were singular with cofinality , attach to one root chains whose lengths increase cofinally to . Every level has at most nodes, the height is , and no branch is cofinal. This contradiction proves regularity. Combined with the preceding closure argument it proves that the cardinal under discussion is strongly inaccessible.
For any , , make a separated set-theoretic tree of functions. Its level consists of the functions realized as for some , with . Order these functions by restriction. Levels are nonempty and have size at most , using the strong-limit property. The tree property gives a branch . Recursively select for , larger than all earlier selections, whose coloring function agrees with through a level above those earlier selections; regularity allows that level to remain below , and its node has a realizing point. Then for . One of the fewer-than- colors occurs on selected points, by regularity. These points are homogeneous, proving for every . ConsequentlyA strictly increasing countable iteration has a supremum of countable cofinality, so it cannot meet this regular set-theoretic tree-property condition; no continuity of has been assumed.
The final printed assertion needs its convention specified. The usual tree property alone does not imply strong inaccessibility; it can consistently hold at successor cardinals. In the argument just given, strong inaccessibility follows from function closure together with that set-theoretic tree property. There is also a stronger branching form of the tree property for which the assertion holds literally: require a cofinal branch in every separated rooted height- set-theoretic tree whose nodes each have fewer than immediate successors, without restricting level sizes. The singular-chain example proves regularity under this convention too. If for , take the full binary set-theoretic tree through level , choose distinct nodes on that level, and attach to its th chosen node a chain of length , for . It has height and at most two successors per node, but every branch has length below . Thus this branching property implies the strong-limit condition and hence strong inaccessibility. At a strongly inaccessible cardinal it agrees, for separated set-theoretic trees, with the usual level-size convention: regularity bounds the union of fewer than successor sets, and strong-limit arithmetic bounds the possible predecessor sequences at limit levels.
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.