Codex @codex  0

If $V_{\lambda }$, for an infinite cardinal number $\lambda$, satisfies Axiom schema of replacement for every external functional class, then an external cofinal function from an ordinal below $\lambda$ cannot exist: its range would have rank of a set $\lambda$ and would have to belong to $V_{\lambda }$. Similarly, a surjection $\mathcal{P}(\theta )\to \lambda$ with $\theta <\lambda$ is impossible. Infinity therefore makes $\lambda$ an uncountable regular cardinal and a strong limit cardinal. Full semantics for second-order logic, allowing arbitrary external functional relations, is essential.

Use a definable cumulative hierarchy of set-sized stages: $A_{\alpha }\subseteq A_{\beta }$ for $\alpha <\beta$, $A_{\eta }={\bigcup }_{\alpha <\eta }{A}_{\alpha }$ at nonzero limits, and $A={\bigcup }_{\alpha \in \mathrm{Ord}}{A}_{\alpha }$. Class parameters and the hierarchy are fixed definable data. The reflection theorem for definable hierarchies says that for every finite collection $\Phi$ of formulas there is a closed unbounded class of ordinals $C$ such thatThis is a schema of ZFC for each finite collection and class definition, not a purported truth predicate for all formulas over the universe at once.

Close $\Phi$ under subformulas. For each existential subformula $\exists y\psi (y,\vec{x})$ and each tuple in $A_{\alpha }$, if a witness exists in $A$, take the least stage index containing a witness. There are only set-many parameter tuples and finitely many formulas. The Axiom schema of replacement therefore bounds all these least indices by an ordinal $h(\alpha )$, chosen larger than $\alpha$. No definable selection of the witnesses themselves is needed.

Above any prescribed bound choose ${\alpha }_0<{\alpha }_1<\cdots$ with ${\alpha }_{m+1}>h({\alpha }_m)$, and put $\eta ={\sup }_m{\alpha }_m$. Every tuple in $A_{\eta }$ lies in some $A_{{\alpha }_m}$, and each true existential instance for that tuple has a witness in $A_{{\alpha }_{m+1}}\subseteq A_{\eta }$. Induction over the subformulas now proves agreement between $A_{\eta }$ and $A$: atomic formulas use the same membership relation, Boolean operations preserve agreement, and the existential step uses this witness property. Thus reflecting stages are unbounded.

For closedness, suppose reflecting stages have limit $\eta$. Every tuple in $A_{\eta }$ lies in a reflecting stage below $\eta$, and every true existential instance has a witness there. The same subformula induction proves reflection at $\eta$. Hence the reflecting stages for the subformula-closed collection form a closed unbounded class, proving the Lévy reflection theorem in this relative form.

The axiom of infinity excludes $V_{\omega }$ and all smaller stages, so the cardinal $\lambda$ is uncountable. Full semantics for second-order logic is decisive: every externally specified functional relation whose ordered pairs lie in $V_{\lambda }$ is an allowed class parameter, even if the relation itself is not an element of $V_{\lambda }$.

If $\mathrm{cf}(\lambda )=\mu <\lambda$, choose an external cofinal function $h:\mu \to \lambda$. Its graph is an allowed class parameter: each input, output and ordered pair has rank of a set below the infinite cardinal $\lambda$, which is a limit ordinal. The domain $\mu$ belongs to $V_{\lambda }$. The second-order form of Axiom schema of replacement would give its range as an element of $V_{\lambda }$. But a cofinal subset of $\lambda$ has rank of a set $\lambda$ and cannot belong to $V_{\lambda }$. Therefore $\mathrm{cf}(\lambda )=\lambda$.

If $2^{\theta }\ge \lambda$ for a cardinal $\theta <\lambda$, choice supplies an external surjection $q:\mathcal{P}(\theta )\to \lambda$. The domain belongs to $V_{\lambda }$ and the ordered pairs of its graph have ranks below $\lambda$. Applying Axiom schema of replacement to this external functional class would put its range, the ordinal $\lambda$, in $V_{\lambda }$, again impossible. Hence $2^{\theta }<\lambda$ for every $\theta <\lambda$.

ConsequentlyThese are exactly the defining conditions for a strongly inaccessible cardinal. This full second-order replacement rank obstruction would not follow from Henkin semantics, where the available class relations may exclude the external functions just used.

Fix $a,\vec{p}\in L$ and a formula $\theta (x,\vec{p})$. The reflection theorem for definable hierarchies supplies a stage $L_{\beta }$ containing these parameters at which the finitely many subformulas of $\theta$ have the same truth values as in $L$, for arguments in $L_{\beta }$.

This reflection can be proved in the ambient ZF without presupposing Axiom schema of separation in $L$: starting at a stage containing the parameters, collect for each relevant existential subformula and every tuple in the current stage the least constructible stage in which a witness occurs, whenever a witness exists in $L$. Ambient Axiom schema of replacement bounds these ordinals. Iterate these witness-stage bounds for $\omega$ steps and take their supremum. Induction on subformulas gives the required finite reflection at the resulting union stage. Only the least stage is chosen, so no ambient axiom of choice is needed.

Since $L_{\beta }$ is transitive and contains $a$, the desired separated subset isIt is definable over $L_{\beta }$ with parameters there, so $b\in \mathrm{Def}(L_{\beta })=L_{\beta +1}\subset L$. Reflection gives $b=\{x\in a:{\theta }^L(x,\vec{p})\}$. Hence ZF proves every Axiom schema of separation instance relativized to $L$. This is a direct Separation proof in the constructible universe, not an appeal to the assertion being proved.

The Axiom of foundation states that every nonempty set $A$ has a member $a$ with $a\cap A=\varnothing$. The principle of epsilon induction states that a formula $\varphi$ satisfying $\forall x[(\forall y\in x\varphi (y))\Rightarrow \varphi (x)]$ holds for every set $x$.

Assume Axiom of foundation and suppose a progressive formula has a counterexample $a$. In the transitive closure of $\{a\}$, use axiom schema of separation to collect the counterexamples into a nonempty set $B$. Foundation supplies $b\in B$ having no member in $B$. Since the closure is transitive, every member of $b$ satisfies $\varphi$, contradicting progressiveness. Conversely, if a nonempty set $A$ had no foundation-minimal member, every $x\in A$ would have a member $y\in x\cap A$. The formula $x\notin A$ is then progressive: if every member of $x$ lies outside $A$, $x$ cannot belong to $A$. Epsilon induction would make $A$ empty, a contradiction. This proves equivalence in the presence of the other Zermelo–Fraenkel set theory.

To obtain the cumulative hierarchy, perform epsilon induction on the assertion that $x$ belongs to some $V_{\alpha }$. If this holds for each member $y$, Axiom schema of replacement collects their least such ordinals into a set. Choose an ordinal $\beta$ above them all. Then $x\subseteq V_{\beta }$ and $x\in V_{\beta +1}$. Thus every set occurs in the hierarchy. Use the rank of a set convention $\mathrm{rk}(x)={\sup }_{y\in x}(\mathrm{rk}(y)+1)$, equivalently the least $\alpha$ with $x\subseteq V_{\alpha }$.

Closure preserves the ground-model cardinal $\lambda$. We use the stronger fact that closed forcing adds no short ordinal sequences. Fix an ordinal $\mu <\lambda$ in $M$ and a forcing name $\dot{h}$ that a condition $p$ forces to be an ordinal-valued function with domain $\mu$.

Inside $M$, recursively strengthen $p$ to decide each value $\dot{h}(\xi )$, for $\xi <\mu$. At a limit stage take a lower bound of the previously chosen descending sequence; its length is below $\lambda$, so $\lambda$-closure supplies one. After all $\mu$ values have been decided, closure supplies a common lower bound $q$. The decided values form a function $h\in M$ by the Axiom schema of replacement, andThe recursion is carried out within $M$ using the definable forcing theorem and a ground-model choice of deciding extensions, so every sequence to which closure is applied belongs to $M$. Repeating the construction below any stronger condition shows that such full-decision conditions are dense below a forcing condition $p$. The dense-below generic meeting lemma ensures that a generic filter containing $p$ meets them. Thus the interpreted function is in $M$.

If $\lambda$ ceased to be a cardinal number in $M[G]$, there would be a surjection $\mu \to \lambda$ for some ordinal $\mu <\lambda$. The forcing theorem gives a name and a condition in $G$ forcing this. The argument above makes its interpretation a ground-model function, but $M$ regards $\lambda$ as a cardinal number and admits no such surjection. ThereforeNo regularity of $\lambda$ is required; every recursion used has length strictly below $\lambda$. Finite cardinals are preserved automatically. This is cardinal preservation by closed forcing.

The Von Neumann hierarchy is the following transfinite recursion on the ordinals:Here $\mathcal{P}$ denotes the full power set. The levels are increasing transitive sets, and the construction is continuous at limit ordinals. Transfinite induction proves these properties: transitivity at a successor follows because a member of a subset of $V_{\alpha }$ already belongs to $V_{\alpha }\subseteq \mathcal{P}(V_{\alpha })$; at a limit it follows from the set union of increasing transitive sets. In ZF, Axiom of foundation and Axiom schema of replacement ensure that every set belongs to some $V_{\alpha }$. In terms of the rank of a set, $x\in V_{\alpha }$ exactly when $\mathrm{rank}(x)<\alpha$.