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.

For adequate arithmetic provability predicates, the arithmetized deduction theorem identifies inconsistency of $S+\neg {\mathrm{Con}}_S$ with $S$-provability of ${\mathrm{Con}}_S$. Formalized second incompleteness gives ${\square }_S{\mathrm{Con}}_S\to {\square }_S\perp$. Contraposition yields the displayed conditional. This is an internal theorem and does not license removal of its consistency premise.

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.

Let $T$ be a first-order consistent arithmetic first-order theory with the Hilbert-Bernays-Löb derivability conditions, and suppose $T⊢\neg A$. Provability of $A$ and provability of falsity are equivalent inside $T$, because either refutable first-order sentence implies the other. Thus $\neg {\mathrm{Pr}}_T(A)$ is equivalent inside $T$ to its formal consistency statement. The second incompleteness theorem gives $T⊬\neg {\mathrm{Pr}}_T(A)$.

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$.

A relative-consistency result constructs a model of a first-order theory $S$, or interprets its proofs, from the assumed consistency of a background theory $T$. It establishes $\mathrm{Con}(T)\Rightarrow \mathrm{Con}(S)$ in the stated metatheory, not an unconditional proof of consistency. For independence of an axiom $\phi$ from $S$, obtain consistent models of both $S+\phi$ and $S+\neg \phi$, relative to the background assumption.

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 arithmetic first-order theory $T_0$ with the usual arithmetical provability predicates, defineIf every stage is first-order consistent, the Gödel second incompleteness theorem makes every step strict in the consistency-strength preorder: the next stage proves the preceding stage's formal consistency statement, which that preceding stage cannot prove. Every formal proof from the effective union $T_{\omega }={\bigcup }_{n<\omega }{T}_n$ uses only finitely many axioms and lies in one stage. Thus the union is first-order consistent under this hypothesis and lies strictly above every finite stage. Arithmetic soundness of $T_0$ is a sufficient starting assumption, since each added formal consistency statement is then true in the standard natural numbers.

Consistency of $T_0$ alone does not ensure consistency of the next stage. Assuming Peano arithmetic is first-order consistent, $T_0=\mathrm{PA}+\neg \mathrm{Con}(\mathrm{PA})$ is first-order consistent by the Gödel second incompleteness theorem. Proof inclusion makes it prove $\neg \mathrm{Con}(T_0)$, so adding $\mathrm{Con}(T_0)$ produces an inconsistent next stage. The hypotheses for a progression must therefore distinguish a consistent starting theory from consistency of all its iterates.

Consider extending $S+{\mathrm{Con}}_S$ by a rule sending every ${\mathrm{Con}}_A$ to ${\mathrm{Con}}_{A+{\mathrm{Con}}_A}$. Put $A=S+\neg {\mathrm{Con}}_S$. The initial consistency axiom proves ${\mathrm{Con}}_A$ by the negated-consistency extension theorem, so the rule proves ${\mathrm{Con}}_{A+{\mathrm{Con}}_A}$. But ${\mathrm{Con}}_A\to {\mathrm{Con}}_S$ is provable by inclusion of proofs, making $A+{\mathrm{Con}}_A$ inconsistent. Arithmetic verifies its finite contradiction proof. Thus the unrestricted rule proves both that theory's consistency and inconsistency. This differs from an externally justified progression along specified sound theories.