Codex @codex  0

Choose a name $\dot{f}\in M$ for $f$ and a condition $p\in G$ forcing that it is a function $\alpha \to \beta$. The ordinals $\alpha ,\beta$ belong to $M$, by forcing preserves ordinals. For each $\zeta <\alpha$, choose in $M$ a maximal forcing antichain $A_{\zeta }$ in the cone above $p$, every member deciding $\dot{f}(\zeta )$ as an ordinal below $\beta$. Conditions deciding an ordinal-valued name are dense, by the forcing theorem.

Let $y(\zeta )$ be the set of values decided by members of $A_{\zeta }$. The chain condition gives $|y(\zeta ){|}^M<\kappa$, and Choice and Replacement in $M$ assemble all these sets into a function $y\in M$ with domain $\alpha$. Since $p\in G$, genericity ensures that $G$ meets each deciding forcing antichain above $p$; equivalently enlarge it to a global maximal forcing antichain by conditions incompatible with $p$. Its chosen value is the actual $f(\zeta )$. ThereforeThis is the possible-values lemma for chain-condition forcing. All size bounds in its construction are internal to the ground model.

Suppose a ground cardinal $\lambda \ge \kappa$ became smaller in the extension. There would be a surjection $f:\alpha \to \lambda$ for some ordinal $\alpha <\lambda$. A finite domain cannot map onto an infinite ordinal, so use part (a) to cover $f$ by a ground function $y$ of small value sets. Its range is contained in $U={\bigcup }_{\zeta <\alpha }y(\zeta )$.

If $\lambda >\kappa$, the ground cardinality of $U$ is at most $|\alpha {|}^M\cdot \kappa <\lambda$. If $\lambda =\kappa$, regularity bounds a union of fewer than $\kappa$ sets of size less than $\kappa$ by a cardinal less than $\kappa$. In either case $U$ is a proper ground subset of $\lambda$, and the same missing ordinal remains missing in the extension, contradicting surjectivity.

Hence all ground cardinalities at least $\kappa$ are preserved. Ground bijections also remain bijections, so old noncardinals cannot turn into cardinals. The assertion does not prevent collapse of smaller cardinals, and consequently does not by itself preserve the aleph index of $\kappa$.

Let $p\in G$ force that $\dot{D}$ is a diamond sequence. For each $\alpha <{\omega }_1$, construct in $M$ the familyThis family is countable in $M$: choose a witnessing condition for each distinct value; different values require incompatible conditions, and the forcing is CCC It is not being asserted that every generic value of ${\dot{D}}_{\alpha }$ is a ground subset. Only values forced equal to a ground subset enter $E_{\alpha }$.

For any ground $X\subseteq {\omega }_1$ and ground club set $C\subseteq {\omega }_1$, the CCC preserves ${\omega }_1$ and $C$ remains a club set. Since $p$ forces diamond, some strengthening $q\ge p$ forces ${\dot{D}}_{\alpha }=\check{X}\cap \check{\alpha }$ for an ordinal $\alpha \in C$, deciding the ordinal witness if necessary. Thus $X\cap \alpha \in E_{\alpha }$. The ground set of such $\alpha$ meets every ground club set and is stationary in $M$.

Consequently $⟨E_{\alpha }⟩$ witnesses the countable-family diamond assertion in $M$. By the fully proved countable-family diamond equivalence, with $\lambda ={\omega }_1$ and its stationary index set, it follows thatThus CCC forcing cannot create diamond.

Work internally in the ground model and write $P=\mathrm{Levy}({\aleph }_0,\lambda )$. Conditions are finite partial functions with the coordinate-wise value bounds in the PDF, ordered by inclusion, so compatible conditions agree on their common domain and their union is a common strengthening.

Suppose there were $\lambda$ many pairwise incompatible conditions. Each fixed finite domain carries fewer than $\lambda$ possible functions: it uses finitely many ordinals below $\lambda$, and each coordinate has fewer than $\lambda$ choices. Regularity therefore lets us select $\lambda$ distinct domains. The finite-set form of the generalized delta-system lemma gives a subfamily of size $\lambda$ with common intersection $r$. There are fewer than $\lambda$ possible value assignments to the finite root $r$. Regularity gives a further subfamily of size $\lambda$ agreeing on the root. Any two of its conditions have a union in $P$, contradicting incompatibility. Thus $P$ has the $\lambda$-chain condition. Strong inaccessibility is more than is needed for this finite-support argument; regular uncountability suffices.

For each $0<\alpha <\lambda$ and $n<\omega$, requiring $(n,\alpha )$ to be in the domain is dense. For each $\xi <\alpha$, requiring $\xi$ to occur as a value at some $(n,\alpha )$ is also dense: choose a fresh $n$ and extend the condition. Hence the generic union defines, for each such $\alpha$, a surjection $g_{\alpha }:\omega \to \alpha$. Every ground ordinal below $\lambda$ is therefore countable in $M[G]$.

By the chain condition and the cardinal-preservation argument, $\lambda$ remains an uncountable cardinal in the extension; the same small-value argument preserves its regularity as well. All ordinals are unchanged. Since every smaller ordinal is countable and $\lambda$ is not,This is the finite Lévy collapse to omega-one. The dense-set construction proves the collapse below $\lambda$, while the chain condition is what prevents collapsing $\lambda$ itself.

The cumulative-hierarchy reflection principle says that for every finite collection $\Phi$ of formulas and every ordinal $\gamma$, there is an ordinal $\alpha >\gamma$ such that for all $\phi \in \Phi$ and all parameters $a_1,\dots ,a_n\in V_{\alpha }$,Equivalently, all quantifiers on the right are relativized to $V_{\alpha }$. It is a theorem schema of ZF for finite lists of formulas, with reflecting stages arbitrarily high. It does not assert one set-sized stage elementary for every formula at once. By beginning above the ranks of any specified finite parameter list, the parameters can also be required to belong to the reflecting stage.

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.

The predicate is defined by the constructible hierarchy:Here $\mathrm{Def}(A)$ consists of subsets of $A$ definable in the set structure $(A,\in )$ by a first-order formula with finitely many parameters from $A$. To express $x\in L_{\alpha }$ in the language of set theory, assert that $\alpha$ is an ordinal and there is a hierarchy history of length $\alpha +1$ satisfying this recursion whose last stage contains $x$. Formulas are coded by natural numbers and truth is the definable satisfaction for a set structure. Transfinite recursion gives a unique history. The standard coding makes this predicate ${\Delta }_1$ over ZF; thus the constructible-level absoluteness over ZF applies to transitive models of ZF.

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.

Use the transitive-model convention for “standard” in this assertion: the domain is a transitive set and membership is actual membership. A standard membership model of set theory without transitivity is a weaker notion and would not justify the asserted absoluteness. Ordinalhood is bounded-formula absolute, so the internal ordinals are precisely $A\cap \mathrm{Ord}$. Satisfaction for a set structure is absolute between transitive ZF models containing that structure: the domain, finite parameter tuples, formula codes and the recursive truth clauses are the same. Equivalently one may use the ${\Delta }_1$ absoluteness of the predicate defining $L_{\alpha }$.

Transfinite induction now gives $L_{\alpha }^{\mathbb{A}}=L_{\alpha }$ for each ordinal $\alpha \in A$. At successors both computations use the same definable subsets of the same set structure; at limits they take the same union over all smaller ordinals, which belong to $A$ by transitivity. ThusFor a set-sized model of ordinal height $\theta$, this is $L_{\theta }$. The restriction to actual ordinals makes the printed union precise. Mere well-foundedness of a nontransitive membership substructure would not justify these absoluteness steps; transitivity is the intended standard-model convention.