Formal consistency statement ($\mathrm{Con}(T)$)

After fixing a Gödel numbering, the formal consistency statement $\mathrm{Con}(T)$ asserts that no natural number codes a $T$-proof of a contradiction. For a recursively axiomatized theory, this is an arithmetical sentence expressible inside any sufficiently strong base theory.

If $T$ is a consistent, recursively axiomatized theory containing enough arithmetic, then $T$ does not prove $\mathrm{Con}(T)$. The consistency assumption is external: an inconsistent theory proves every sentence, including its formal consistency statement.

For theories $T,S$ extending a fixed base theory, one consistency-strength comparison iswhere $C_T$ is the set of consequences of $T$ and $\mathrm{Cons}$ is the chosen class of formal consistency statements. Its strict part $T{<}_{\mathrm{Cons}}S$ means $T{\le }_{\mathrm{Cons}}S$ but not $S{\le }_{\mathrm{Cons}}T$.

Let $T=\mathrm{ZFC}+\text{“there is a worldly cardinal”}$ and $T^{\ast }=\mathrm{ZFC}+\mathrm{Con}(\mathrm{ZFC})$. A worldly $\kappa$ makes $V_{\kappa }$ a model of ZFC, and arithmetic absoluteness for a rank-initial model makes it a model of $T^{\ast }$, so $T$ proves $\mathrm{Con}(T^{\ast })$. If $T^{\ast }$ proved $\mathrm{Con}(T)$, then the stronger theory $T$ would prove its own consistency, contradicting the Gödel second incompleteness theorem. Thus, assuming consistency, $T^{\ast }{<}_{\mathrm{Cons}}T$.

Starting from a recursively axiomatized theory $T_0$, defineAssuming consistency, Gödel second incompleteness theorem makes every step strict in the consistency-strength preorder, while the effective union $T_{\omega }={\bigcup }_{n<\omega }{T}_n$ lies strictly above every finite stage.