An inner model of ZF is a transitive class containing every ordinal, with inherited membership, such that each ZF axiom holds with all quantifiers restricted to . Here transitivity means . For a proper class this is an axiom-by-axiom assertion, not an internal truth predicate for the whole class. An inner model can have fewer subsets of a given set than the surrounding universe; it need not have the same cardinals or the same continuum function.
Inner models prove relative consistency. If a theory proves that a definable class satisfies every axiom of , an inconsistency proof from could be relativized to and become an inconsistency proof from . Thus . This reasoning concerns formal interpretations and needs no assumption that a given model of is externally well-founded.
The central example is the constructible universe. Define
where contains exactly the subsets definable over using parameters from . Satisfaction for a set structure is definable, so this recursion is available in ZF. Induction shows that the levels are transitive and increasing: if , the subset is , so . The ordinal part of is , giving all ordinals in .
For completeness, the main axiom mechanisms explain why this example works. Finite set operations on constructible parameters are definable at finitely many further stages. For a fixed finite family of formulas and parameters, close a sequence of levels under their least constructible witness stages and take its union; induction on formulas gives a reflecting level. Separation of a constructible set then occurs at the next definability stage. For replacement, ambient replacement bounds the construction stages of the unique constructible outputs; a reflecting level above that bound makes the range definable. For the internal power set of , use ambient separation to form , bound the construction stages of its members, and at a sufficiently high level define the family of all subsets of in that level. Thus the internal power set is constructible even though some ambient subsets may not be. Foundation is inherited by transitivity, and infinity comes from and its successor stages.
There is a canonical well-order of : order by first construction stage, then by the least definition code and finite parameter tuple, using the previously constructed well-orders for parameters. Each set in can be well-ordered by the restriction of this set-like class order; hence satisfies AC. Moreover the hierarchy computed inside is the same hierarchy, because definability over a fixed set structure and limit unions are absolute. Thus satisfies . The further cardinal analysis of this hierarchy, encapsulated in the constructible universe theorem, gives GCH. Consequently
This proves the relative consistency of choice, CH and GCH; in particular none can be refuted by ZF if ZF is consistent. The assertions here are internal to : they do not assert CH in the ambient universe.
Inner models also isolate definable information. The relative constructible universe built with a set parameter retains that parameter and all ordinals while discarding unrelated sets. Such constructions help compare relative consistency strengths and identify which hypotheses survive passage to smaller universes; preservation of a large-cardinal property must be checked separately, not inferred merely from transitivity.
There is an important limitation, the constructible-universe obstruction to a uniform inner-model proof of failure of choice. Every inner model of ZF contains the ambient . Indeed by induction: the same set structure has the same definable subsets at a successor stage, and both hierarchies take the same union at a limit. If the ambient universe satisfies , this forces . Thus inner models cannot uniformly produce a model of or from every ZF universe. To prove the opposite independence directions one needs an outer-model or other interpretation technique, such as forcing or the non-well-founded symmetry construction in Question 2.
The independence statements are relative consistency statements. We construct models from an ambient model of ZFC; the construction is an interpretation and does not assume that the ambient model is transitive. Foundation is already true in the ordinary ambient membership structure, so its positive consistency direction is immediate.
For the negative direction, construct an extensional cumulative universe over Quine atoms. Let be a countably infinite set of formal symbols . Give each the extension . For a set of already constructed objects, let be its unique representative: set , and otherwise use a fresh tagged code . Atom codes have a different tag. Begin with and put
Set . The interpreted membership relation gives exactly the members , and gives exactly the member . This convention matters: creating a second representative for would violate extensionality. Every object is uniquely determined by its extension, so satisfies full extensionality. Every set-sized collection of objects has bounded construction rank, by ambient replacement, and hence has its representative in .
Here are the remaining axiom verifications. Empty set and pairing use and . If , its interpreted union is . Its interpreted power set is
since every subset extension has a unique representative. The pure, atom-free finite hierarchy supplies a copy of and an inductive set. For separation, translate an -formula into the ambient language, with quantifiers restricted to the definable class ; ambient separation gives the appropriate subset of , and represents it. For replacement, uniqueness in the interpreted functional relation gives an ambient definable functional image of the set . Ambient replacement makes that image set-sized, and again represents it. These arguments also establish that all the operations used have bounded construction rank.
Ambient choice gives choice in : choose a member from each nonempty extension in a set-sized family and represent the graph, using interpreted ordered pairs. But , and the nonempty set with extension has no -minimal member. Thus
Together with the ordinary model, this proves independence of foundation from the other ZF axioms, even when choice is retained.
To extend the construction to failure of choice, let the full permutation group of act on by
The singleton convention is equivariant, so this is an automorphism of . An object has finite support if some finite has the property that every permutation fixing pointwise fixes the object. Retain objects all of whose membership descendants have finite support, stopping the hereditary recursion at the atomic self-loops. This gives the hereditarily finite-supported Quine-atom model ; each belongs to it, with support .
Extensionality persists because every retained object's members are retained. Empty set, pairing, infinity and union preserve hereditary finite support. For separation on a retained set , the union of finite supports for and the formula's parameters supports the separated extension: permutations fixing those supports preserve satisfaction in . All its members are retained, so its representative is retained. For replacement, the same support fixes the functional range, because an automorphism must take the unique output at an input to the unique output at its transported input. Ambient replacement bounds that range; all its members are in , so its representative belongs to . Finally, the collection of all retained subset representatives of is an ambient set, contained in the full interpreted power set of . A support of permutes this collection onto itself, and its members are retained. Its representative is therefore the internal power set in . This verifies every ZF axiom except foundation; foundation still fails at each .
The atom set and the family of its two-element subsets have empty support and are retained. Suppose a choice function on were retained, with finite support . Choose distinct outside and transpose them. The transposition fixes and fixes the unordered pair , but moves whichever of its two members selects. Equivariance would require that selected member to be fixed, a contradiction. Hence
The full universe gives the corresponding positive-choice model. Choice is therefore independent of ZF without foundation. Unlike a permutation model with ordinary urelements, this model retains full pure-set extensionality: the atomic objects are self-membered sets, not empty objects exempted from extensionality.
The constructible-universe interpretation gives . Thus the consistency assumptions in both displayed conclusions can equivalently be taken to be ; no additional consistency strength is being used.
We use rooted-tree homeomorphic embedding: an injective vertex map preserves ancestors and lowest common ancestors, while an edge may map to a longer path. The root may map below the host root. Write for this relation. The assertion of Kruskal's tree theorem is that finite rooted trees form a well-quasi-ordering: every infinite sequence has with .
We first supply the word lemma needed in the proof. In a well-quasi-order , every sequence has an infinite nondecreasing subsequence. Indeed, if no term had infinitely many later terms above it, successive choices beyond the finite sets of later dominators would give a bad sequence. Some term therefore has infinitely many later dominators; repeat the argument inside that infinite subsequence, which is still well-quasi-ordered, to build a chain.
Now order finite words over by subsequence embedding with coordinatewise increase. Suppose a bad word sequence exists and choose one minimally: at each position use a word of least length allowing a bad continuation of the fixed prefix. No word is empty. Write , removing its last letter. Choose indices with . The sequence
would also be bad. An old word embedding into embeds into , contrary to the original badness; and would extend, using the last-letter comparison, to . But is shorter than , contradicting minimality. This proves Higman lemma, including its empty-word case.
Suppose next that there is a bad sequence of finite rooted trees, and choose a minimal bad sequence by vertex count. Let consist of all proper rooted subtrees hanging below vertices of the . This collection is well-quasi-ordered. Otherwise choose a bad sequence in . Its containing-tree indices can be selected strictly increasing, say is a proper subtree of : a finite initial collection of containing trees has only finitely many proper subtrees, and a bad sequence cannot repeat an isomorphism class. Then
is bad. No earlier can embed into , because and this would contradict the original sequence. The new tail is bad by construction. Since , this contradicts minimality.
List each tree's immediate root subtrees in any chosen order. These are finite words in the well-quasi-order , so the word lemma gives for which the child word of embeds into that of . Send the root of to the root of , and use the chosen embeddings inside the selected, distinct target branches. The connecting paths from the target root to the images of the source children have disjoint interiors; lowest common ancestors in different branches are preserved. This constructs , the final contradiction. Thus finite rooted trees are well-quasi-ordered by homeomorphic embedding. If labels lie in an arbitrary well-quasi-order, the same proof uses label-monotone embeddings; compare root labels and child words in their product well-quasi-order. The product property follows by taking a nondecreasing subsequence in the first coordinate and a good pair in the second.
For Friedman's finite form of Kruskal's theorem, fix . Consider all finite bad prefixes satisfying , up to rooted-tree isomorphism. They form a prefix tree. At each node there are finitely many possible next trees, because there are only finitely many rooted-tree isomorphism types on at most vertices. If prefixes of arbitrary length existed, the König infinity lemma would give an infinite branch, hence an infinite bad sequence, contrary to what we proved. Its height is therefore bounded. Consequently
The same finite-prefix argument works with a fixed finite label alphabet, and more generally with any prescribed size bound having only finitely many possibilities at each position. These are finite existence statements; no numerical estimate on is needed for the conclusion.
For the general alternative, let be a functor between locally small categories, with a complete category. The Freyd general adjoint functor theorem says that has a left adjoint if and only if it preserves small categorical limits and satisfies the solution-set condition. Explicitly, for every , there must be a set of morphisms such that every has the form for some and . Equivalently, each comma category has a weakly initial set.
We prove the initial-object lemma for complete categories with a weakly initial set. Let be a locally small category which is complete and has a weakly initial set . Its product in a category is weakly initial: for each , choose a morphism and compose with the projection . The hom-set is a set. Form equalizing every endomorphism of with , by taking the equalizer of the two morphisms
whose -coordinates are and . Then for every endomorphism , and is monic. There is a morphism for every , by composing with a weakly initial morphism out of .
To prove uniqueness, let and take their equalizer . Weak initiality of gives . The composite is an endomorphism, so . Cancel the monomorphism to obtain . Thus is both monic and split epic, hence an isomorphism: if , cancellation from gives . Since , it follows that . Therefore is an initial object, proving the lemma fully.
Now assume categorical limit preservation and the solution-set condition. The comma category is locally small. It is complete: for a small diagram in a category , take its underlying categorical limit in . Since preserves this categorical limit, the compatible give a unique . The same universal property shows that is the categorical limit in the comma category. Its weakly initial set and the proved lemma therefore supply an initial object . For , its universal property defines a unique with . Uniqueness proves the identity morphism and composition in a category laws and the naturality of . The same universal property gives the natural bijection , so .
For necessity, an adjunction supplies the singleton weakly initial set at . It also proves that preserves categorical limits: maps correspond to maps , and compatible families of the latter factor uniquely through any categorical limit in . Hence the image categorical cone under has the required universal property. This proves both directions of the general alternative.
For the special alternative, the limit form of the special adjoint functor theorem says: if is complete, locally small and well-powered, with a small cogenerating family , and is locally small, then has a left adjoint exactly when it preserves small categorical limits. A cogenerating set means that unequal parallel morphisms are distinguished by some morphism . We prove the needed solution-set condition, so that the general theorem applies.
Fix . A supporting subobject of is a monomorphism through whose image under the morphism factors. There is at least one, namely . Because is well-powered, choose a set of representatives of all these supporting subobjects. A limit-preserving functor preserves monomorphisms: a map is monic exactly when its diagonal into its self-pullback in a category is an isomorphism, and both the pullback in a category and this isomorphism are preserved. Consequently each factorization of through is unique. Form the intersection of subobjects of the supporting representatives, as a wide pullback in a category over . The unique lifts of are compatible and, since preserves that categorical limit, they give a factorization
This is a minimal supported subobject. More explicitly, if also supports , then is one of the supporting subobjects of . The intersection therefore factors through , giving with . Monicity of gives ; monicity of then makes invertible.
For any , if , the equalizer of supports , because preserves that equalizer. Minimality makes it invertible, so . We have therefore obtained injective functions
Let be the realized image subset of the fixed set . Use the unique morphism corresponding to each to form the evaluation embedding into cogenerator products
This morphism is monic: if two morphisms into have identical product composites, every morphism from to every gives identical composites, and the cogenerating property makes the two morphisms equal. There is only a set of possible families of subsets , and hence a set of possible products . Each has only a set of subobjects by well-poweredness, and each chosen subobject has only a set of morphisms by local smallness. Take all these pairs as a weakly initial set. Every original receives a morphism from a pair representing its , through . Thus the set is weakly initial in .
The general theorem now supplies a left adjoint. Necessity again follows from preservation of categorical limits by a right adjoint. This proves the special alternative, including its size argument. Using only the realized subsets avoids assuming that an arbitrary object admits a morphism into every cogenerator. Both adjoint functor theorem alternatives are proved.
For and , define maps of hom-sets
They are natural in , using naturality of . The one supplied triangle identity for an adjunction gives
Naturality of also gives
Since , the composite is idempotent. Evaluating its equation on gives . As is a composite of natural transformations, this proves that is an idempotent in the functor category, including the required naturality.
Suppose this one-triangle adjunction idempotent splits as natural transformations with and . The maps and give inverse bijections between and the subset of consisting of maps with . Indeed , , and . The maps give inverse bijections between that subset and , since and . Combining them gives the natural bijection
with inverse . Hence . Its adjunction unit is and its adjunction counit is .
Conversely, suppose , with natural bijection . Set and . Then and . By the covariant Yoneda lemma, the transformation is precomposition with a unique morphism , and is precomposition with a unique morphism . The equation evaluated at gives ; the equation evaluated at gives . Naturality in of implies, again by the same Yoneda lemma, that are natural transformations. Thus they split in the whole functor category, rather than merely at individual objects. We have proved

There are unlisted articles, also show them or only show them.