Iterated consistency progression

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.