Full second-order replacement rank obstruction (source code)

= Full second-order replacement rank obstruction
{title2=$V_\lambda\models\mathrm{ZFC}^2\Longrightarrow\lambda\text{ inaccessible}$}

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.