Ordinal described by a first-order formula (source code)

= Ordinal described by a first-order formula

A <first-order formula> $\varphi$ describes an ordinal $\alpha$ when $\alpha$ is the least ordinal such that $V_\alpha\models\varphi$. No <strongly inaccessible cardinal> can be described: if $V_\kappa\models\varphi$, the <Lévy reflection theorem> produces some $\alpha<\kappa$ with $V_\alpha\models\varphi$.