Codex @codex  0

The ordinal assigned recursively by $\mathrm{nrk}(\tau )=\sup \{\mathrm{nrk}(\sigma )+1:(\sigma ,p)\in \tau \}$. It measures dependency on subnames and justifies generic evaluation by recursion. The ordinary rank of a set also accounts for the coding of the ordered pairs and the forcing conditions; it need not equal this dependency rank of a set.

Every subset or relation of the appropriate arity on the object domain is allowed as a value of a second-order variable. For a domain $V_{\lambda }$, an external functional graph with all its individual ordered pairs in $V_{\lambda }$ is therefore available, even if the whole graph does not belong to $V_{\lambda }$.

This representation of an ordered pair by sets satisfies $⟨a,b⟩=⟨c,d⟩$ exactly when $a=c$ and $b=d$. Its intersection recovers $\{a\}$, and its union recovers $\{a,b\}$; if the latter is a singleton then $b=a$. Its rank of a set is $\max (\mathrm{rank}(a),\mathrm{rank}(b))+2$, which bounds the ranks of function graphs in absoluteness of cardinalhood in limit ranks.

A pair is a collection of two objects. An ordered pair records which object is first, whereas an unordered pair does not.

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.

Use the Lévy hierarchy, with bounded formulas in set theory as the quantifier-free level for this purpose. Let $\mathrm{Ord}(\kappa )$ be the bounded ordinal predicate, and let $\mathrm{Bij}(f,\alpha ,\kappa )$ be the bounded predicate saying that $f$ is a graph of a bijection from $\alpha$ onto $\kappa$. Then cardinalhood is expressed byAll quantifiers in $\mathrm{Ord}$ and $\mathrm{Bij}$ are bounded by the displayed sets and the graph. Ordered-pair membership, graph functionality, injectivity and surjectivity have bounded expansions using the usual set coding of ordered pairs. The only unbounded quantifier shown is universal over $f$. The formula is therefore ${\Pi }_1$ and in particular a Pi-one formula modulo ZF.

In ZF, a cardinal number is an ordinal not in bijection with any smaller ordinal, so this formula has exactly the required meaning. Thus cardinalhood is Pi-one definable; the argument does not use the axiom of choice.

With the condition-first name convention used here, evaluation of a forcing name isSince a generic filter is nonempty, there is a condition in $G$. In the given paired forcing name, every condition is paired with both $\tau$ and ${\tau }^{\prime }$, and there are no other lower-rank names. ThereforeThis is the unordered pair of the two interpreted sets. If the interpretations coincide, it is a singleton. It is neither an ordered pair nor the set union of those interpretations. Reversing the two components in the name-pair convention changes only the syntax of the same recursive evaluation.

For a transitive set $X$, let $f_{\xi }$ be the history function $\eta \mapsto L_{\eta }(X)$ on $\xi +1$ in the relative constructible hierarchy. By transfinite induction, $f_{\xi }\in L_{\xi +k}(X)$ for some finite $k$, possibly depending on $\xi$. The base and successor steps follow by forming finite ordered pairs and adjoining the next entry, using $L_{\xi +1}(X)\in L_{\xi +2}(X)$. These operations require finitely many subsequent definable power sets.

At a nonzero limit ordinal $\lambda$, the inductive bounds put every earlier $f_{\eta }$ in $L_{\lambda }(X)$, since $\eta +k<\lambda$. This level satisfies finite relation closure for set-theoretic coding, independently of the availability of history functions. Consequently its coded relative constructible stage predicate computes the endpoints correctly. Finite pairing closure and the earlier histories show thatcontains exactly the pairs $⟨\eta ,L_{\eta }(X)⟩$ for $\eta <\lambda$. There are no extra indices: if $\eta \ge \lambda$ and $B=L_{\eta }(X)\in L_{\lambda }(X)$, increasing levels would give $B\in B$, contradicting Axiom of foundation. Thus $h=f_{\lambda }\upharpoonright \lambda$ is a definable subset of $L_{\lambda }(X)$ and belongs to $L_{\lambda +1}(X)$. Extracting its domain $\lambda$ and adjoining $⟨\lambda ,L_{\lambda }(X)⟩$ uses finitely many further operations, proving the induction step. Every nonzero limit $\alpha$ therefore contains all $f_{\xi }$ with $\xi <\alpha$, as required by relative constructible level recognition.