The Constructible Hierarchy and Inner Models

Fix an actual formula code and take $m\in \omega$ greater than every variable index occurring anywhere in it, including bound indices. Transitivity and internal Pairing and Union put every finite tuple from $A$ in $N$. Conversely every internal $m$-tuple from $A$ is an actual one: the domain, entries and ordered pairs agree by transitivity. Finite code parsing uses the same finite words in both universes.

On each subformula define truth for assignments $t\in A^m$ recursively. For atoms use equality or membership of the indicated coordinates; use complement and intersection for negation and conjunction; for $\mathrm{\exists }{v}_i\psi$ use $\mathrm{\exists }b\in A$ applied to the truth of $\psi$ at $t[i:=b]$. Recursion into $\mathcal{P}(A^m)$ is a set construction, both internally and externally.

Constructor induction identifies these truth values. Atoms compare the same sets by the same membership relation. Equal child truth values give equal negations and conjunctions. At an existential node each witness on either side lies in the identical set $A$, and its updated tuple is in $N$ by step 1.1; the induction hypothesis therefore transfers each witness in both directions. This comparison does not require equality of the internal and external power sets of $A^m$.

Fix one $a_0\in A$. An $m$-tuple extends to an infinite assignment by setting every later coordinate equal to $a_0$; Replacement constructs this extension inside $N$ as well as outside. The satisfaction clauses show by constructor induction that this extension has exactly the recursively computed finite truth values. Coincidence makes all choices of extension equivalent on the free variables. Step 3.1 thus proves the asserted equality of internal and external satisfaction for every finite tuple. The single choice of $a_0$ is existential instantiation, not AC.

If $A=\mathrm{\varnothing }$, internal Pairing constructs the actual singleton $\{\mathrm{\varnothing }\}$ by transitivity, so both Def operations give that set. Suppose henceforth that $A\mathrm{\ne }\mathrm{\varnothing }$.

For each external formula and finite parameter tuple from $A$, the code and tuple belong to $N$. Internal Separation gives $b\in N$ consisting of the internally satisfying elements of $A$. For each actual $x\in A$, finite-tuple absoluteness gives $x\in b$ exactly when the external formula holds. Transitivity ensures that $b$ has no additional elements. Hence every external Def subset is an internal Def subset.

Conversely an internal member of Def has an internal code and tuple witnessing its definition. These are actual code and tuple, and the same satisfaction comparison identifies its subset with the externally defined one. Internal Replacement collects exactly these subsets; both inclusions show equality of the two Def sets.

If $A$ is transitive, every $a\in A$ is the subset of $A$ defined by $x\in a$, so $A\subseteq \mathrm{Def}(A)$. Each $b\in \mathrm{Def}(A)$ is a subset of $A$; hence $z\in b$ implies $z\in A\subseteq \mathrm{Def}(A)$. This proves transitivity of Def(A), including $A=\mathrm{\varnothing }$ by its special clause. Set transfinite induction along each ordinal interval now proves transitivity of the levels and nesting: successors use this observation; limits are increasing unions.

Induct simultaneously against the cumulative hierarchy. At zero the inclusion is equality. If $L_{\beta }\subseteq V_{\beta }$, every member of $L_{\beta +1}$ is a subset of $L_{\beta }$, hence is in $V_{\beta +1}$. At limits take unions. Thus $L_{\alpha }\subseteq V_{\alpha }$; in particular any ordinal in $L_{\alpha }$ is less than $\alpha$.

Induction proves that every ordinal below $\alpha$ belongs to $L_{\alpha }$. Zero is immediate. Given $L_{\beta }\cap \mathrm{Ord}=\beta$, for $\beta >0$ the bounded ordinalhood formula over the transitive nonempty $L_{\beta }$ defines precisely the subset $\beta$, so $\beta \in L_{\beta +1}$. For $\beta =0$, $0\in L_1=\{0\}$. Old ordinals remain by nesting, and limit stages take unions. This proves the ordinal intersection identity and $\alpha \in L_{\alpha +1}$.

The formula $x=x$ defines the whole set $L_{\alpha }$ over itself when nonempty, and Def(empty) contains empty. Hence $L_{\alpha }\in L_{\alpha +1}$. For $x\in L$, its first membership stage is ${\rho }_L(x)+1$. If $x\in L_{\alpha }$, leastness gives ${\rho }_L(x)+1\le \alpha$ and so ${\rho }_L(x)<\alpha$. Conversely that inequality and nesting place $x$ in $L_{\alpha }$. Transitivity of the class union follows from transitivity of each level; step 3.1 puts every ordinal in that union.

Use $W_{\gamma }=L_{\gamma }$ and $W=L$. The recursive definition supplies uniform definability, the limit definition supplies continuity, and F1 supplies monotonicity and nonemptiness. Every element of $W$ belongs to a level by definition. These are precisely the general-class hypotheses of F2.

Apply the construction in F2 to the finite subformula closure of $\mathrm{\Phi }$, starting above $\alpha$ and above zero. It bounds the least witness stages for tuples in each set level using ambient Replacement, iterates that definable bound through omega, and takes the supremum $\beta$. Strict increase makes $\beta$ a nonzero limit. Each finite tuple lies in a stage of this sequence, so every true existential in the closed family has a witness before $\beta$; the witness criterion in F2 gives agreement in both directions. All these are ambient ZF operations, and no internal Replacement or satisfaction predicate for the whole class L is presumed.

If $a,b\in L$ have the same members in L, transitivity puts all their actual members in L, so ambient Extensionality gives $a=b$. If $a\in L$ is nonempty, ambient Foundation gives $u\in a$ with $u\cap a=\mathrm{\varnothing }$; transitivity puts $u$ in L, so it is also an internal Foundation witness. Empty Set holds because $\mathrm{\varnothing }\in L_1$.

For $a,b\in L$, put both parameters in one nonempty level $L_{\gamma }$. The formula $x=a\vee x=b$ defines $\{a,b\}$ as a subset of this level, hence puts it in $L_{\gamma +1}$. For $a\in L_{\gamma }$, transitivity twice ensures that every member of $\bigcup a$ is in $L_{\gamma }$; the formula $\mathrm{\exists }y\in a(x\in y)$ over that level therefore defines exactly $\bigcup a$. Its successor contains this union, including the empty union. These actual sets satisfy the relativized Pairing and Union axioms.

The actual ordinal $\omega$ belongs to L. It contains empty and, with each $n\in \omega$, the actual successor $n\cup \{n\}$. These finite ordinals belong to L; the pairs and unions used in the successor description are the actual operations by step 2.1. Thus $\omega$ is an internal inductive set, proving Infinity and completing the six asserted axioms.

Choose an ordinal bound large enough that one level contains $a$ and every $p_i$. Reflect $\varphi$ above this bound, obtaining a nonempty transitive $L_{\beta }$ containing those parameters. For every $x\in a$, transitivity puts $x$ in $L_{\beta }$, so ${\varphi }^L(x,p)$ agrees with satisfaction of $\varphi (x,p)$ in $L_{\beta }$.

Over $L_{\beta }$ the formula $x\in a\wedge \varphi (x,p)$ defines exactly the desired subset: the first conjunct uses actual membership and the second agrees by step 1.1. F2 puts this subset in $\mathrm{Def}(L_{\beta })=L_{\beta +1}\subseteq L$. An empty a or a formula with no satisfying elements gives the empty subset by the same definition. The argument uses only this fixed formula and ambient ZF.

In the ambient universe use Separation on $\mathcal{P}(a)$ to form $Y=\{b\subseteq a:b\in L\}$. The predicate of belonging to L is uniformly definable. Ambient Replacement collects $R=\{{\rho }_L(b):b\in Y\}$; put $\beta =\sup (R\cup \{{\rho }_L(a)\})+1$. Then $a\in L_{\beta }$ and $Y\subseteq L_{\beta }$. This bounds all constructible subsets simultaneously without using Power Set or Replacement in L.

The set $L_{\beta }$ is itself an element of L. Apply F1 inside L to this set with the predicate $b\subseteq a$. For $a,b\in L$, this predicate is absolute directly: every member of $b$ lies in L by transitivity, and membership in $a$ is actual membership. The separated set is therefore $\{b\in L_{\beta }:b\subseteq a\}=Y$ by step 1.1. It belongs to L and contains exactly the internal subsets of a, proving internal Power Set.

The fixed ambient formula $y\in L\wedge {\varphi }^L(x,y,p)$ is functional on the actual set $a$, since transitivity puts each $x\in a$ in L. Ambient Replacement therefore forms its image Y as a set of constructible elements. Ambient Replacement again forms the set of their constructible ranks. A successor above their supremum and the finitely many parameter ranks gives $\beta$ with $Y\subseteq L_{\beta }$ and $a,p_i\in L_{\beta }$. Empty images require no exception to this bound.

Apply Separation inside L to the set $L_{\beta }\in L$ with formula $\mathrm{\exists }x\in a\varphi (x,y,p)$. Its relativization singles out exactly Y, because step 1.1 bounded the entire image. Hence $Y\in L$, using neither internal Replacement nor a choice of witnesses.

Equivalently, reflect that fixed image-defining formula at a level $L_{\gamma }$ above $\beta$. All image elements and parameters are in this level. Agreement makes its Def subset precisely Y, so $Y\in L_{\gamma +1}$. This also confirms that the assertion is a scheme for fixed formulas and has no uniform class-truth premise.

Internal ZF gives N its hierarchy history on each ordinal interval in N. External induction identifies its values: at zero both are empty; if the value at $\gamma$ is the actual $L_{\gamma }\in N$, F1 identifies its internal Def with $L_{\gamma +1}$. At a limit $\lambda \in N$, transitivity makes the internal history have every actual index $\gamma <\lambda$, and its internal union has exactly the union of their actual values. Thus $(L_{\alpha }{)}^N=L_{\alpha }\in N$ for every ordinal $\alpha$ of N.

If N contains all ordinals, every actual L level is therefore in N. Transitivity gives $L\subseteq N$, and the internal existential definition of constructibility ranges over precisely all actual ordinals, so its union is exactly L. For a set model the same argument stops at its ordinal height; no higher level is asserted to belong to N.

The six axioms in F2, Separation in F3, internal Power Set in F4, and Replacement in F5 establish all of ZF in L. Earlier level properties give transitivity and all ordinals. Thus L itself meets the hypotheses of step 2.1, which now yields $L^L=L$. Every element of L is internally constructible, exactly the relativization of $V=L$. This application occurs only after ZF in L has been established.

For arity zero the tuple set is the singleton containing the empty tuple. Induct on n: for a nonempty subset of $A^{n+1}$, take the least first coordinate occurring in it; its nonempty fibre of n-tuples has a least tuple by induction. Prepending the selected first coordinate gives the lexicographic least member. If A is empty, positive-arity tuple sets are empty and are well-ordered vacuously. Totality and transitivity follow by comparing the first coordinate at which two tuples differ.

In any nonempty set of valid codes, first minimize its natural-number e coordinates. The remaining tuples all have the single arity specified by e, and step 1.1 gives a least tuple. This proves the code order is a well-order. For each $b\in \mathrm{Def}(A)$ with A nonempty, its decoding fibre is a nonempty set by F1; its least element therefore exists uniquely. For empty A the designated singleton code has the same property. Minimization gives unique representatives, without any appeal to AC.

Recurse on ordinal intervals, keeping an order ${<}_{\alpha }$ on $L_{\alpha }$. At zero use the empty order. At $\alpha +1$ retain ${<}_{\alpha }$ on the old elements, put every old element before every member of $L_{\alpha +1}\setminus L_{\alpha }$, and order the new elements by their least Def codes over $(L_{\alpha },{<}_{\alpha })$ from F1. At nonzero limits take the union of earlier orders. On malformed histories one may return the empty relation, so the recursion rule is total and definable.

Induction proves these are coherent well-orders and each earlier level is an initial segment. The successor order is the sum of the old well-order and a subset of the code well-order. At a limit, comparisons of finitely many elements take place in a common earlier level, giving a total transitive strict order. For a nonempty subset S of the limit level, take any $x\in S$ in an earlier level; the least member of the nonempty intersection of S with that level is least in all of S, since the level is an initial segment. This single existential choice proves well-ordering without a choice function.

Interval uniqueness gives a uniform formula for all these orders. Their class union defines ${<}_L$ without set parameters. The same initial-segment argument as step 2.1 gives a least element to every nonempty set subset of L (and to any specified nonempty definable subclass, by Separation in a level). For $x\in L_{\alpha }$, every predecessor of x lies in $L_{\alpha }$, so Separation makes its predecessor collection a set.

Inside L the construction is licensed by the ZF axioms in F4–F7 and has exactly the same levels by F8. Induct on alpha to compare orders. At successors, F9 identifies internal and external Def on the old level. The previous order is identical, hence code comparison, decoding fibres and their least codes are identical. At limits the unions agree. Thus the two constructions produce the same restrictions and the same class relation.

Let $a\in L$ be internally a family of nonempty sets. Transitivity makes every $b\in a$ an actual nonempty subset of L. Inside L, separate the restriction of its canonical order to b; this is a well-order by F1, so b has a unique least element $m(b)\in b$. The rule specifying m is one fixed internal formula, with no chosen ordering parameter.

Internal Replacement applied to $b\mapsto ⟨b,m(b)⟩$ produces a graph $g\in L$ with domain a, since internal Pairing in F4 constructs the ordered pairs. The uniqueness in step 1.1 makes g a function and $g(b)\in b$ for each $b\in a$. If a is empty this graph is empty. Thus g is the choice function required by F5. AC was proved internally; it was not invoked to choose the least elements.

OD is closed under every fixed uniquely defined set operation with finitely many OD parameters: replace each parameter by its unique definition from finitely many ordinals and existentially quantify those uniquely specified parameters. The resulting fixed formula uniquely defines the output from the union of the finite lists of ordinal parameters, so F1 makes the output OD. This argument is a formula-by-formula composition, not a class truth predicate. Every ordinal is OD using itself as a parameter, so every ordinal and all its descendants are OD. Thus all ordinals belong to HOD. If $y\in x\in \mathrm{H}\mathrm{O}\mathrm{D}$, every member of $\mathrm{TC}(\{y\})$ belongs to $\mathrm{TC}(\{x\})$, proving transitivity.

Whenever a set z is OD and every member of z is in HOD, z is in HOD: its TC consists of z and descendants of its members, all OD. Pairing and union of HOD sets are OD by step 1.1; their members are HOD by transitivity, so they are HOD. Empty and omega are already HOD as ordinals. Transitivity transfers Extensionality and ambient Foundation exactly by putting every actual member, including a Foundation witness, in HOD. Actual omega, pairs and unions verify internal Infinity.

For a fixed formula phi, a and finitely many parameters in HOD, ambient Separation forms $b=\{x\in a:{\varphi }^{\mathrm{H}\mathrm{O}\mathrm{D}}(x,p)\}$. Because HOD is a fixed definable class, b is uniquely definable from those OD parameters; step 1.1 makes it OD. Every member of b is HOD by transitivity from a, so step 2.1 makes b HOD. This proves each internal Separation instance.

Ambient Separation on $\mathcal{P}(a)$ forms $c=\mathcal{P}(a)\cap \mathrm{H}\mathrm{O}\mathrm{D}$ for $a\in \mathrm{H}\mathrm{O}\mathrm{D}$. It is uniquely definable from the OD parameter a, hence OD by step 1.1. All its members are HOD by its definition, so c is HOD by step 2.1. Transitivity makes internal subsethood agree with actual subsethood, proving that c is the internal power set.

If a fixed HOD-relativized formula is functional on $a\in \mathrm{H}\mathrm{O}\mathrm{D}$ with HOD parameters, ambient Replacement produces its set image Y of HOD elements. This image is uniquely definable from those OD parameters, so it is OD; step 2.1 then puts Y in HOD. This proves Replacement without assuming it internally. Together with steps 2.1–4.1 all ZF axioms now hold in HOD.

Order OD witness codes $(\theta ,e,t)$ first by the ordinal theta, then by the natural number e encoding formula and arity, then lexicographically by the ordinal tuple $t\in {\theta }^n$. Require theta positive and the code to have a unique decoded output in $V_{\theta }$. F2 gives a well-order within each theta. For any nonempty definable class of codes, minimize theta by first restricting to an ordinal bound supplied by one witness; then minimize e and t in sets. Predecessors of a fixed code form a set, since they lie among codes with theta at most its theta, hence in a set of finite ordinal tuples. Each OD set has a least witness code; order OD by these least codes. This is a uniformly definable setlike class well-order: distinct outputs have distinct least codes, and the same witness-bound minimization supplies minima for nonempty set subsets of OD.

For a family $a\in \mathrm{H}\mathrm{O}\mathrm{D}$ of nonempty sets, let m(b) be the least element of b in the OD order from step 6.1. Each b is a subset of HOD and hence of OD. Ambient Replacement forms $g=\{⟨b,m(b)⟩:b\in a\}$. This graph is uniquely definable from a using the fixed code order, so it is OD by step 1.1. Each b and m(b) is HOD, and Kuratowski pairs formed from them are HOD by step 2.1. Thus every member of g is HOD and step 2.1 implies g is HOD. It is a choice function internally as well as externally, proving F3 in HOD. This does not require the ambient OD order to be the order computed as OD inside HOD.

HOD is now a transitive definable ZFC inner model with all ordinals. Apply F4 to obtain $L\subseteq \mathrm{H}\mathrm{O}\mathrm{D}$. Every construction above used unique definitions, ambient ZF and minimization in specified well-orders, never ambient AC.

Fix one axiom sigma. F1 supplies the six basic ZF axioms, while F2, F3, and F4 supply Separation, Power Set, and Replacement; each schema instance uses only its fixed formula and finitely many ZF instances. F6 supplies AC and F5 supplies V=L. Thus for this sigma there is a ZF derivation of ${\sigma }^L$. This assertion is indexed externally by standard axioms and is not an internal truth assertion about all formulas.

Suppose now that M is a transitive set model of ZF. External Separation on M, using satisfaction of the fixed predicate defining constructibility, forms $C=L^M$ as a set. By F5 it is the union of the actual $L_{\alpha }$ for ordinals alpha in M. Hence it is nonempty and transitive, all its ordinals belong to M, and every ordinal of M belongs to C (its successor stage is still indexed in M).

Evaluate each fixed derivation from step 1.1 in M. Its axioms hold there, and first-order inference preserves satisfaction; thus M satisfies the internally relativized sigma. Constructor comparison of that fixed formula, as in F7, identifies this with satisfaction in C: atoms are actual membership and each guarded quantifier ranges over exactly C. Therefore C satisfies each standard axiom of ZFC+V=L. Step 2.1 gives the same-ordinals conclusion. The result remains conditional on the supplied M, with no assertion that a model can be obtained from a consistency statement.