A notion of iterated consistency axioms

172 Views Asked by At

Let $T$ be some theory (such as Peano Arithmetic or ZFC) capable of expressing arithmetic. We define $T_k$ for some $k$ as $T+\forall x<k.\text{Con}(T_x)$ (call that last axiom $\text{Con}_k(T)).$

Now if, $T$ is also capable of expressing ordinal arithmetic, we can expand this to all ordinal numbers. (Even if it can't, you can create an axiom for each $x$ under $k$, splitting $\text{Con}_k(T)$ into $|k|$ statements. (This won't be a nice theory though unless $k$ is a recursive ordinal.))

Here's an interesting lemma. If the provable arithmetical statements of $T$ are true in the standard model of natural numbers, then so is every $T_k$. To prove this, assume that all $T_x$ are true. Then $T_x$ are all consistient, since if otherwise, they would prove $0=1$, which is false. This means that $\text{Con}_k(T)$ is true, and so $T_k$ is as well. By transfinite induction, this means $T_k$ is true for all $k$.

This means for example, if we trust $ZFC$, we should trust $ZFC_k$ for all $k$ as well.

Is there a name for this notion of iterated consistency? Any references?