How strong is the iterated consistency of ZFC?

Question

Let $T_0$ be $\mathsf{ZFC}$ and, for $n\in\omega$, set $T_{n +1}=T_{n}+\mathrm{Con}(T_{n})$.

Question 1: Is there a natural number $n$ such that $T_{n}$ is equiconsistent with $\mathsf{ZFC}+$ some large cardinal axiom?

Question 2: Is the consistency strength of the $T_{n}$ bounded by some large cardinal axiom? More precisely, is there a large cardinal axiom $A$ such that $$\mathrm{Con}(\mathsf{ZFC}+A)\Longrightarrow \forall n\,\mathrm{Con}(T_{n})?$$

Continue the iteration transfinitely, so for each ordinal $\alpha$, $T_{\alpha +1}=T_{\alpha}+\mathrm{Con}(T_{\alpha})$ and, if $\alpha$ is limit, then $T_{\alpha}=\bigcup_{\beta\in \alpha} T_{\beta}$. Finally, let $T_{\infty}=\bigcup_\alpha T_{\alpha}$.

Question 3: For which large cardinal axiom $A$ and ordinal $\alpha$ we have that $T_{\alpha}$ is equiconsistent with $\mathsf{ZFC}+ A$?

Question 4: Is the consistency strength of all $T_{\alpha}$s bounded by some large cardinal axiom? Precisely, is there a large cardinal axiom $A$ such that $$\mathrm{Con}(\mathsf{ZFC}+A)\Longrightarrow \forall \alpha\,\mathrm{Con}(T_{\alpha})?$$ In the other words what is the consistency strength of $T_{\infty}$ in the large cardinal hierarchy?

Answer 1

The procedure you suggest really cannot get too far. Here is an abstract result explaining what I mean (see Aspects of incompleteness by Per Lindström): Given an r.e. sequence of r.e. theories that interpret arithmetic and whose union is consistent, there is a $\Pi^0_1$ formula that is not provable by any of them. That a sequence is r.e. means here that we have a way of listing all pairs $(\phi,n)$ with $\phi$ an axiom of the $n$-th theory. (The connection comes by realizing that $\mathsf{Con}(T)$ is $\Pi^0_1$ for r.e. $T$.)

Arguing specifically within your setting: There is a natural way of iterating the consistency operator, to define a sequence $T_\alpha$, $\alpha<\omega_1^{CK}$.

Although each $T_\alpha$ is strictly stronger than its predecessors, their union is still pretty weak: The theory $U_1=\mathsf{ZFC}+$"$\mathsf{ZFC}$ has an $\omega$-model" is stronger than all of them. This theory can also be iterated $\omega_1^{CK}$ times ($U_2$ would be $U_1+$"$U_1$ has an $\omega$-model", etc).

All these theories are strictly weaker than $S_1=\mathsf{ZFC}+$"$\mathsf{ZFC}$ has a transitive set model", which, again, we can iterate $\omega_1^{CK}$ times.

All these theories are strictly weaker than asserting that some $V_\alpha$ is a model of $\mathsf{ZFC}$ ($\alpha$ is what Joel Hamkins calls a worldly cardinal). Worldliness can also be iterated, and the resulting theories are strictly weaker than asserting that there is a weakly inaccessible cardinal.

(Stopping at $\omega_1^{CK}$ is just an artifact of my wanting to keep all the theories recursive. I don't quite see how to make sense of iterating these theories beyond the recursive ordinals. What do we mean by $\mathsf{Con}(T)$ in such a case, since $T$ is no longer r.e.? Of course, we can make sense of this semantically, and just require the existence of models (after some pains formalizing this, as the relevant language in which the theories are formulated would evolve with the ordinal), but even then it seems to me we need to argue that the models are sufficiently correct to see the relevant ordinals, and this seems a distraction from the main goal.)

Above, I mentioned that we iterate the consistency operator "naturally". By contrast, Solomon Feferman and others have investigated ways of iterating "consistency" operators, so that the claims above fail, with the "$\omega$-th step" being considerably stronger than just $\mathsf{ZFC}+\mathrm{Con}(\mathsf{ZFC})+\mathrm{Con}(\mathrm{Con}(\mathsf{ZFC}))+\dots$

There are also other alternatives, where we "add" to $\mathsf{ZFC}$ all true $\Pi^0_1$ statements, then to this "add" all true $\Pi^0_2$-statements, etc. This is typically formalized via reflection sequences, see here.

Answer 2

As long as $T_\alpha$ is uniformly definable say in $V_{\alpha+\omega}$, $V_\kappa$ is a model of $T_\kappa$ for $\kappa$ inaccessible. So you can't get "there is an inaccessible" that way.