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