Reflection, Absoluteness, and Elementary Submodels

For $a,b\in M$, equality and membership in either structure mean the actual relations $a=b$ and $a\in b$. Thus the atomic cases agree. The formula constructors admit induction, so it remains to show that agreement is preserved by each constructor.

If $\varphi$ and $\psi$ agree on all tuples in $M$, their conjunctions agree because both conjuncts have the same truth values. Their negations agree because a truth value is false in one structure exactly when it is false in the other.

Let $a,\bar{b}\in M$. A witness $c$ for $\mathrm{\exists }x\in a\varphi (x,\bar{b})$ in either structure is an actual member of $a$. Transitivity puts every such $c$ in $M$, hence also in $N$. The induction hypothesis at $(c,\bar{b})$ transfers the matrix in either direction, retaining the same witness. If $a=\mathrm{\varnothing }$, both existential statements are false. Universal bounded quantifiers follow by negation.

Constructor induction now gives the asserted equivalence for every bounded formula. For fixed class definitions the same induction is a finite metatheoretic induction on the chosen formula, with each quantifier relativized; it requires no class satisfaction set.

Write $Z(z):=\mathrm{\forall }u\in z(u\mathrm{\ne }u)$, $S(x,y):=\mathrm{\forall }u\in x(u\in y)$, and $P(z,x,y):=x\in z\wedge y\in z\wedge \mathrm{\forall }u\in z(u=x\vee u=y)$. These say respectively $z=\mathrm{\varnothing }$, $x\subseteq y$, and $z=\{x,y\}$. The singleton graph is $P(z,x,x)$. Every quantifier displayed is bounded; extensional equality with the indicated sets follows from the two inclusions encoded in each formula.

The union graph is $\mathrm{\forall }v\in a\mathrm{\forall }u\in v(u\in z)\wedge \mathrm{\forall }u\in z\mathrm{\exists }v\in a(u\in v)$. The intersection graph is $(Z(a)\wedge Z(z))\vee [\mathrm{\exists }v\in a(v=v)\wedge \mathrm{\forall }u\in z\mathrm{\forall }v\in a(u\in v)\wedge \mathrm{\forall }v\in a\mathrm{\forall }u\in v((\mathrm{\forall }w\in au\in w)\to u\in z)]$. If $a$ is nonempty, any member of the actual intersection lies in any chosen member $v$ of $a$, so the last clause puts it in $z$; the other clause gives the reverse inclusion. For difference use $\mathrm{\forall }u\in z(u\in a\wedge u\mathrm{\notin }b)\wedge \mathrm{\forall }u\in a(u\mathrm{\notin }b\to u\in z)$.

Put $K(p,x,y):=\mathrm{\exists }s\in p\mathrm{\exists }t\in p(P(s,x,x)\wedge P(t,x,y)\wedge P(p,s,t))$. It says exactly $p=\{\{x\},\{x,y\}\}$. To bound coordinates without assuming a union object in the domain, abbreviate $\mathrm{\exists }x\in \bigcup p\chi$ by $\mathrm{\exists }t\in p\mathrm{\exists }x\in t\chi$, and its universal version by two bounded universals. Write $\mathrm{Pair}(p):=\mathrm{\exists }x\in \bigcup p\mathrm{\exists }y\in \bigcup pK(p,x,y)$. This includes the case $x=y$, where $p$ is a singleton.

The product graph $z=a\times b$ is $\mathrm{\forall }p\in z\mathrm{\exists }x\in a\mathrm{\exists }y\in bK(p,x,y)\wedge \mathrm{\forall }x\in a\mathrm{\forall }y\in b\mathrm{\exists }p\in zK(p,x,y)$. Let $R(r):=\mathrm{\forall }p\in r\mathrm{Pair}(p)$ and $E(r,x,y):=\mathrm{\exists }p\in rK(p,x,y)$. The graph $d=\mathrm{dom}(r)$ includes $R(r)$, $\mathrm{\forall }x\in d\mathrm{\exists }p\in r\mathrm{\exists }y\in \bigcup pK(p,x,y)$, and $\mathrm{\forall }p\in r\mathrm{\forall }x\in \bigcup p\mathrm{\forall }y\in \bigcup p(K(p,x,y)\to x\in d)$. Interchange $x,y$ for the range. Both clauses are necessary: one excludes surplus coordinates and the other prevents missing coordinates.

Functionhood is $R(r)$ together with: for all $p,q\in r$, all $x,y\in \bigcup p$ and all $u,v\in \bigcup q$, $(K(p,x,y)\wedge K(q,u,v)\wedge x=u)\to y=v$. Injection replaces the last implication by $y=v\to x=u$, while retaining functionhood. Evaluation at $x$ with value $y$ is functionhood and $E(r,x,y)$. For $r:a\to b$ also require domain $a$ by the preceding graph and $\mathrm{\forall }p\in r\mathrm{\forall }x,y\in \bigcup p(K(p,x,y)\to y\in b)$. These formulas quantify only through supplied sets.

Expanding each finite abbreviation gives bounded membership formulas. Their truth therefore agrees by bounded absoluteness, with every input and candidate output in the smaller transitive structure. Each formula characterizes its actual graph by the calculations above, so an output present there has the same value outside. No clause quantifies over all subsets of an input or produces an output set inside a domain.

Transitivity of $a$ is $\mathrm{\forall }x\in a\mathrm{\forall }y\in x(y\in a)$. Add the bounded clauses that membership on $a$ is irreflexive, transitive, and trichotomous. In ambient ZF, every nonempty subset $b\subseteq a$ has by Foundation an element $u$ with $u\cap b=\mathrm{\varnothing }$; linearity then makes $u$ the least element of $b$. Hence these bounded clauses are equivalent to ordinalhood as defined in F2. Their truth is absolute by F1.

In a transitive ZF model $M$, the internal empty set has no actual members and is $0$. If the internal numeral $n$ is the real $n$, its internally formed successor has exactly the actual members of $n\cup \{n\}$, because both parameters and every member of the candidate output lie in $M$. Thus external induction fixes every finite ordinal and puts it in ${\omega }^M$.

The internal $w={\omega }^M$ satisfies the bounded description: $w$ is a nonzero ordinal, is not a successor, and each $u\in w$ is zero or a successor ordinal. Successor is expressed by $\mathrm{\exists }v\in u[u=v\cup \{v\}]$, using the bounded graphs in F3. Thus the description holds externally. By step 2.1, $\omega \subseteq w$. If $w\mathrm{\ne }\omega$, ordinal comparison gives $\omega \in w$, contrary to the description since $\omega$ is neither zero nor a successor. Hence $w=\omega$.

If $\alpha$ is an ordinal of $M$ and $\beta <\alpha$, transitivity puts $\beta$ in $M$, and step 1.1 makes it an ordinal there. Thus the ordinals of $M$ are downward closed among actual ordinals, as claimed.

Each model has its rank function by its ZF axioms; F1 identifies its ordinal values with actual ordinals. Suppose by external membership induction that both ranks agree on every $y\in x$. Transitivity ensures these are exactly the predecessors considered inside either model.

By F2, each rank of $x$ is the supremum of the predecessor ranks plus one. Ordinal successor and union have their actual values by F3, so both suprema are the same actual ordinal. For $x=\mathrm{\varnothing }$ both are the empty supremum $0$. Foundation validates this external induction, proving rank agreement for every $x\in M$.

For $x\in M$, F4 applied inside the two ZF models gives $x\in (V_{\alpha }{)}^M\leftrightarrow {\mathrm{rank}}^M(x)<\alpha \leftrightarrow {\mathrm{rank}}^N(x)<\alpha \leftrightarrow x\in (V_{\alpha }{)}^N$. Also every element of $(V_{\alpha }{)}^M$ belongs to $M$ by transitivity. These two statements give precisely the displayed intersection equality.

A bounded formula already has the required form with an empty existential block. Rename bound variables fresh before combining normal forms. For conjunction of $\mathrm{\exists }\bar{u}\delta$ and $\mathrm{\exists }\bar{v}ϵ$, use $\mathrm{\exists }\bar{u}\bar{v}(\delta \wedge ϵ)$. For disjunction use $\mathrm{\exists }\bar{u}\bar{v}(\delta \vee ϵ)$: unused witness variables can be filled with the empty set in either true branch. An added unbounded existential joins the prefix.

A bounded existential $\mathrm{\exists }x\in a\mathrm{\exists }\bar{u}\delta$ is $\mathrm{\exists }x\bar{u}(x\in a\wedge \delta )$. To treat a bounded universal, encode a finite tuple of witnesses as a set using successive ordered pairs, whose coordinate assertions are bounded by F2. For $\mathrm{\forall }x\in a\mathrm{\exists }u\delta (x,u)$, Collection (F1) supplies a set $b$ meeting the witness class for every $x\in a$. Thus this formula implies $\mathrm{\exists }b\mathrm{\forall }x\in a\mathrm{\exists }u\in b\delta (x,u)$. Conversely any such $b$ supplies the original witnesses by dropping the bound. If $a=\mathrm{\varnothing }$, take $b=\mathrm{\varnothing }$.

The matrix in the last display is bounded, and decoding a fixed finite tuple adds only bounded quantifiers over its pair components. Induction over the closure clauses now gives the claimed normal form, in both directions at every clause. The only collection of an arbitrary family of witnesses was step 2.1, where Collection selected a bounding set rather than a choice function.

If $M\models \mathrm{\exists }\bar{u}\delta (\bar{u},\bar{a})$, take its finite tuple of witnesses $\bar{b}\in M$. The tuple remains in $N$, and bounded absoluteness F1 gives $N\models \delta (\bar{b},\bar{a})$. Thus $N$ satisfies the existential formula. The empty block is exactly F1.

If a universal dual were true in $N$ and false in $M$, its existential negation would be true in $M$ and hence in $N$ by step 1.1. This contradicts its truth in $N$, proving downward transfer.

When classification is modulo ZF, F2 supplies a ZF equivalence to the literal normal form. Each model satisfies that equivalence under the extra hypothesis. Translate to the normal form in the source model, apply steps 1.1 or 2.1, and translate back in the destination model.

Assume agreement. A true existential in $D$ transfers to $C$, where its satisfaction provides $b\in C$ with ${\psi }^C(b,\bar{a})$. Since $\psi \in \mathrm{\Phi }$, agreement for the matrix transfers this to ${\psi }^D(b,\bar{a})$. This proves necessity.

Conversely assume the witness condition. Atomic equality and membership agree by restriction. Constructor induction (F1) gives agreement for negation and conjunction from agreement of their subformulas, since the Boolean truth tables are the same.

For an existential with parameters in $C$, a witness in $C$ for its truth in $C$ satisfies the matrix in $D$ by induction, so also witnesses truth in $D$. If it is true in $D$, the stipulated witness condition gives $b\in C$ satisfying the matrix in $D$, and induction transfers the matrix to $C$. Thus the existential agrees in both directions. Subformula closure licenses each invocation of induction. This proves sufficiency and the equivalence; the finite class version uses the same fixed list of relativizations.

For each existential matrix ${\psi }_i(y,\bar{x})$ define $r_i(\bar{x})=0$ when no witness exists, and otherwise let it be the least rank of a witness. F1 supplies that least ordinal and a witness at that rank. Because the list of formulas is fixed externally, this is a separate definable function for each $i$, with no appeal to truth for arbitrary formulas.

The union of the finitely many sets of parameter tuples from $V_{\alpha }$ is a set, including a singleton empty tuple for a sentence. Replacement collects all $r_i(\bar{a})$ in a set $R_{\alpha }$. Put $b(\alpha )=\sup (R_{\alpha }\cup \{\alpha \})+1$. Then $b(\alpha )>\alpha$ and every required least-rank witness has rank below $b(\alpha )$; by F2 it lies in $V_{b(\alpha )}$. No particular witness has been selected as a function of the tuple.

For $W$, replace least witness rank by the least stage containing a witness in $W$ whose matrix holds relativized to $W$. Exhaustion gives such a stage; it has a least value by the well-order of ordinals. Replacement over tuples in $W_{\alpha }$ and the same successor-supremum formula give $b(\alpha )$. By monotonicity, for every true instance at least one witness lies in $W_{b(\alpha )}$; witnesses of larger rank need not lie there. With no existential formulas or no true instances, the same formula still gives a bound above $\alpha$.

Expand abbreviations and close $\mathrm{\Phi }$ under subformulas; the resulting family is still finite. Take the definable witness bound $b$ from F1 for this family. Start ${\beta }_0>\alpha$, increasing it if necessary so that $W_{{\beta }_0}$ is nonempty in the general nonempty-class case. For $V$, ${\beta }_0=\alpha +1$ suffices.

Define ${\beta }_{n+1}=b({\beta }_n)$ and $\beta ={\sup }_{n\in \omega }{\beta }_n$. This definable class recursion yields a set sequence in ZF as follows: induction on $n$ gives a unique finite attempt of length $n+1$; extending the attempt applies the definable function $b$ once. Uniqueness makes its endpoint a functional formula, so Replacement on $\omega$ collects all endpoints. Union gives their supremum. Thus no fixed set containing all possible ordinals and no choice function is required. Strict increase implies $\beta >\alpha$ and makes $\beta$ a nonzero limit ordinal.

Continuity and monotonicity give $W_{\beta }={\bigcup }_n{W}_{{\beta }_n}$: any earlier index is below some ${\beta }_n$. A finite tuple from this union is contained in one stage, by taking the maximum of finitely many indices; the empty tuple is in every stage. If an existential from the closed family is true in $W$ at that tuple, F1 gives a witness in $W_{{\beta }_{n+1}}\subseteq W_{\beta }$.

The finite witness criterion F2 therefore gives agreement for every member of the closed family, hence for $\mathrm{\Phi }$. For $V$, F3 supplies the increasing transitive hierarchy and its limit clause is F4; Foundation supplies exhaustion. Power Set constructs successor stages, Separation and Replacement construct the rank bounds, and Infinity, Replacement and Union supply step 2.1. For an empty $W$ every positive-arity tuple assertion is vacuous and closed-formula relativizations agree because both domains are empty. The entire construction is choice-free.

List the finitely many sentences ${\gamma }_1,\dots ,{\gamma }_k$ of $\mathrm{\Gamma }$ using the axiom serialization in F2. Each is an axiom of the ambient theory, so their finite conjunction is a theorem there. If the ambient theory is ZFC and one of these sentences is Choice, use F3 exactly for that sentence. No Choice premise is needed for the ZF branch.

Apply F1 to that fixed finite list and the desired bound. It gives a $\beta$ such that each ${\gamma }_i^{V_{\beta }}\leftrightarrow {\gamma }_i$. Step 1.1 gives the right-hand sides, hence every relativized axiom. The cumulative stage is transitive, so it is the required transitive model. For an infinite carrier begin with a bound at least $\omega$. For $k=0$ any nonempty stage above the bound works.

For any nonempty subset $A\subseteq X$, ambient Foundation supplies $a\in A$ with no member in $A$. Hence the restricted membership relation is externally well-founded. It is setlike since $X$ is a set. This uses actual membership, not an arbitrary relation a structure calls well-founded.

For distinct $a,b\in X$, Extensionality in $M$ implies that some $u\in M$ belongs to exactly one of $a,b$. Elementarity F1 applied with parameters $a,b$ gives such a $u\in X$. Thus the predecessor sets of $a,b$ within $X$ differ: restricted membership is extensional.

F2 now supplies a unique isomorphism onto a transitive set $\bar{X}$, satisfying $\pi (a)=\{\pi (u):u\in X\cap a\}$. Its inverse is an isomorphism onto $X$. For any formula and tuple in $\bar{X}$, F3 transfers satisfaction to $X$, and F1 then transfers it to $M$. This is precisely elementarity of the inverse collapse into $M$. Composing any injection $X\to \omega$ with ${\pi }^{-1}$ shows the same countability for $\bar{X}$.

For $a\in A$, transitivity gives $a\subseteq A\subseteq X$. Assuming the collapse fixes every member $u\in a$, its equation (F1) gives $\pi (a)=\{\pi (u):u\in a\}=a$. External membership induction proves this for all $a\in A$, starting with the empty predecessor set.

The restriction of $\pi$ to $X\cap \alpha$ is an order isomorphism onto the elements of $\pi (\alpha )$, by its equation and injectivity. This image is transitive: if $v\in \pi (u)$ and $u\in X\cap \alpha$, then $v=\pi (t)$ for $t\in X\cap u$; ordinal transitivity gives $t\in \alpha$, so $v\in \pi (\alpha )$. The induced membership order is a well-order since $X\cap \alpha$ inherits one from $\alpha$ (F2). Thus $\pi (\alpha )$ is an ordinal of the indicated order type.

If $X\cap \alpha$ is transitive it is itself an ordinal, and the unique ordinal isomorphic to its membership order is itself. Therefore its order type, hence $\pi (\alpha )$, equals $X\cap \alpha$. Without the hypothesis $\alpha \subseteq X$ this need not equal $\alpha$.

The language has one binary membership symbol, so $\max (\mathrm{\mid }L\mathrm{\mid },{\mathrm{\aleph }}_0)={\mathrm{\aleph }}_0$. As $M$ is infinite, ${\mathrm{\aleph }}_0\le \mathrm{\mid }M\mathrm{\mid }$ in ZFC; the parameter set has size at most ${\mathrm{\aleph }}_0$. F1 therefore applies with $\kappa ={\mathrm{\aleph }}_0$ and gives $A\subseteq X\prec M$ of size exactly ${\mathrm{\aleph }}_0$. The AC premise F3 is used in this supplier to select Skolem witnesses and the size enumerations.

F2 applies to the actual membership on $X$ and the Extensionality hypothesis on $M$, giving its transitive collapse. The collapse bijection transports the countable enumeration of $X$ to its image. For a named parameter $a$, containment of $\{a\}$ gives $a\in X$ and does not require every member of $a$ to lie in $X$.

Enlarge the fixed finite fragment by Extensionality, and use F1 to reflect it to $V_{\beta }$ for $\beta >\omega$. This is an infinite transitive membership structure satisfying Extensionality and every original axiom of $\mathrm{\Gamma }$. In the ZFC branch, ambient AC (F3) supplies a reflected Choice axiom if present.

Apply F2 with empty parameter set to obtain a countable elementary submodel of this stage and its transitive collapse $C$. Elementarity preserves each sentence of $\mathrm{\Gamma }$, and the collapse isomorphism preserves the same sentences. Thus $(C,\in )\models \mathrm{\Gamma }$. AC is used in F2 even when $\mathrm{\Gamma }\subseteq \mathrm{Z}\mathrm{F}$; the earlier reflection of ZF axioms alone does not use it.

Let $\lambda >0$ and $U={\bigcup }_{\alpha <\lambda }{M}_{\alpha }$. F1 gives a set structure with $M_{\alpha }\prec U$. It satisfies Extensionality because any one stage does and sentences transfer by elementarity. Apply F2 with $X=M=U$ to obtain its collapse $\pi :U\to \bar{U}$, and similarly obtain ${\pi }_{\alpha }:M_{\alpha }\to {\bar{M}}_{\alpha }$ for each stage. Their uniqueness permits Replacement to collect these maps.

Define $j_{\alpha \beta }={\pi }_{\beta }\circ {\iota }_{\alpha \beta }\circ {\pi }_{\alpha }^{-1}$ and $j_{\alpha }=\pi \circ {\iota }_{\alpha }\circ {\pi }_{\alpha }^{-1}$. The inverse and forward collapses are isomorphisms and the inclusions are elementary, so each composite is elementary by the satisfaction equivalences. Its codomain is the corresponding transitive collapse, not the original carrier.

For $\alpha \le \beta \le \gamma$, cancellation gives $j_{\beta \gamma }{j}_{\alpha \beta }={\pi }_{\gamma }{\iota }_{\beta \gamma }({\pi }_{\beta }^{-1}{\pi }_{\beta }){\iota }_{\alpha \beta }{\pi }_{\alpha }^{-1}=j_{\alpha \gamma }$. The same calculation gives $j_{\beta }{j}_{\alpha \beta }=j_{\alpha }$, and $j_{\alpha \alpha }$ is the identity. This proves coherence without identifying any composite with a literal inclusion.