= Iterated consistency progression
Starting from a recursively axiomatized <arithmetic> <first-order theory> $T_0$ with the usual <arithmetical provability predicates>, define
$$
T_{n+1}=T_n+\operatorname{Con}(T_n).
$$
If 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=\operatorname{PA}+\neg\operatorname{Con}(\operatorname{PA})$ is <first-order consistent> by the <Gödel second incompleteness theorem>. Proof inclusion makes it prove $\neg\operatorname{Con}(T_0)$, so adding $\operatorname{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.
Back to article page
