Infinite descending consistency chains

Question

What are some examples of consistent theories $T_i$ (extending elementary arithmetic EA) such that for $∀i∈ℕ \,\, T_i ⊢ \mathrm{Con}(T_{i+1})$?

Such theories exist; see for example An infinitely descending sequence of sound theories each proving the next consistent. However, in the link, the theories are given using (non-well-founded) self-reference, which in an intuitive informal sense, leaves one wondering what exactly is each theory asserting.

Thus, I am especially interested in natural or intuitive examples that do not use self-reference. Here is what I have.

If we only require $\mathrm{PA} ⊬ (\mathrm{Con}(T_{i+1}) ⇒ \mathrm{Con}(T_i))$, then for an example, fix a proof system that is constructively provably in $\mathrm{EA}$ polynomial time equivalent to sequent calculus. Let $n$ (provably in EA) be the number of bits in the shortest inconsistency in $\mathrm{PA}$ if there is any. If $T_i = \mathrm{EA} + \mathrm{Con}(\mathrm{PA}) ∨ 2^i ∤ ⌊\log \log \log n⌋$, then for all $i$, $T_i ⊢ T_{i+1}$ and $\mathrm{PA} ⊬ (\mathrm{Con}(T_{i+1}) ⇒ \mathrm{Con}(T_i))$. (To get the unpredictability of $n$, the proof relies on $\mathrm{PA}$ provability of $\mathrm{PA}$ bounded consistency in polynomial time, and the impossibility of a subpolynomial proof length of bounded consistency.)

To get $T_i ⊢ \mathrm{Con}(T_{i+1})$, I have two potential natural examples, but I do not have a proof that they work.
Update: Per Fedor Pakhomov's answer, the original constructions (given in brackets for reference) did not work; below are the modified versions. See the answers for constructions that have been shown to work; the answers complement each other.

Construction 1: Let $S_0 = \mathrm{PA}$ and $S_{i+1} = \mathrm{PA} + \mathrm{Con}(S_i)$, and let $h_{ε_0}$ be the $ε_0$ function in the Hardy hierarchy. Set $T_i = \mathrm{PA} + ∀n \,\, (h_{ε_0 2}(i+n) \text{ exists} ⇒ \mathrm{Con}(S_n))$ [the original used $h_{ε_0}$, but perhaps even $h_{ε_0 2} = λx.h_{ε_0}(h_{ε_0}(x))$ is too small]

Construction 2: Let $S_0 = \mathrm{PA}$ and $S_{i+1} = \mathrm{PA} + \mathrm{Con}(S_i)$. We can arrange that $⌈\mathrm{Con}(S_i)⌉$ is $i^{O(1)}$, but we only need $2^{2^{2^{O(i)}}}$. Let $\mathrm{Con}_m(A)$ mean that $A$ has no inconsistency shorter than $m$ bits.
Set $T_i = \mathrm{PA} + ∀n \, (\mathrm{Con}_{2^{n^i}}(S_{n+i}) ⇒ \mathrm{Con}(S_n))$ [the original used $S_n$ in place of $S_{n+i}$].
Note: If we can show in $\mathrm{PA}$ that each $T_i$ (for $i>0$) is consistent relative to $S=∪S_i$, then the construction works because if $S$ is inconsistent, then working in $T_i$, $T_{i+1}$ is equivalent to $S_{i'}$ for a low enough $i'$ so as to be consistent.

Also, the well-ordering of $Π^0_1$ ordinals imposes fundamental limits on descending consistency chains. I suspect that for sound $T$, $∃i \, T_i ⊬ ∀j \, (T_j ⊢ \mathrm{Con}(T_{j+1}))$.

Answer 1

Here is perhaps a more relatable example, which doesn't use self-reference. (I once heard a similar such example from W. Hugh Woodin.)$\newcommand\Con{\text{Con}}\newcommand\ZFC{\text{ZFC}}$

Let $\psi_i$ be the assertion that there are $n-i$ many inaccessible cardinals, where $n$ is the size of the least proof of a contradiction from ZFC plus a measurable cardinal, if this theory is indeed inconsistent.

Let me assume that ZFC plus a measurable cardinal is consistent. In this case, $\ZFC+\neg\Con(\ZFC+\exists\text{ measurable})$ is also consistent, and in any model of ZFC plus $\neg\Con(\ZFC+\exists\text{ measurable})$, the proof of a contradiction from that theory will be necessarily nonstandard. So $n$ will be nonstandard when it exists. Since $i$ is standard, however, the subtraction $n-i$ is sensible and we will never hit zero.

Furthermore, in any model of $\neg\Con(\ZFC+\exists\text{ measurable})$, each $\psi_i$ directly implies the truth and indeed the consistency of $\psi_{i+1}$, since with $n-i$ inaccessible cardinals we will have an extra one, and can therefore make a model with only $n-(i+1)$ inaccessible cardinals, as desired, simply by chopping off at the biggest one.

Thus, the theories $\ZFC+\neg\Con(\ZFC+\exists\text{ measurable})+\psi_i$ are descending in consistency strength.

Of course, you can use other large cardinals, if you like, and form additional similar examples.

Answer 2

I know two constructions of the chains of this sort that aren't based on explicit diagonalization.

In a recent work by James Walsh and me https://arxiv.org/abs/1805.02095 we gave an example (Theorem 3.8) of a chain of theories $T_0,T_1,\ldots$ that have even stronger property $T_i\vdash \mathsf{RFN}_{\Sigma_1}(T_{i+1})$. The theory $T_i$ is defined to be $$\mathsf{EA}+\mbox{``there is a proof $p$ of a false $\Sigma_1$ sentence in $\mathsf{I\Sigma}_2$ s.t. $\mathsf{RFN}^{p\mathop{\dot -}i}_{\Sigma_1}(\mathsf{EA})$ holds''}.$$

In the construction above one could replace $\mathsf{EA}$ with $\mathsf{I}\Sigma_1$ and sustain the same property. But in the case of $\mathsf{I}\Sigma_1$ the $T_i$'s could be defined in an alternative way that makes them very similar to your Construction 1. Let $R_{\mathsf{I\Sigma_2}}$ be the following fast-growing function $$\begin{aligned} R_{\mathsf{I\Sigma_2}}\colon x \longmapsto \sup \{ y\mid & y\mbox{ is the least witness for a $\Sigma_1$ sentence provable in } \\ & \mbox{$\mathsf{I\Sigma_2}$ by a proof with the Gödel number $\le x$}\}\end{aligned}.$$ Alternatively $T_i$'s could be defined as $$T_i\colon \mathsf{I}\Sigma_1+\forall x\; (R_{\mathsf{I}\Sigma_2}(x+i)\mbox{ is defined } \Rightarrow \mathsf{RFN}^x_{\Sigma_1}(\mathsf{I}\Sigma_1))+R_{\mathsf{I}\Sigma_2}\mbox{ isn't total}.$$

Although, the similarity, your Construction 1 seems not to work. Using some manipulations with models of arithmetic (injecting inconsistencies, and cuts in large non-standard intervals) if I am not missing anything, it is possible to construct a model $\mathfrak{M}$ of $T_0$ such that $\mathfrak{M}\not\models \mathsf{Con}(S_a)$, for some non-standard $a\in \mathfrak{M}$. But it is easy to observe that $\mathfrak{M}\not\models \mathsf{Con}(T_1)$. Assume for a contradiction that $\mathfrak{M}\models \mathsf{Con}(T_1)$. Since $\mathsf{PA}\vdash \forall x\;\mathsf{Prv}_{\mathsf{PA}}(h_{\varepsilon_0}(x)\mbox{ is defined})$, we would have $\mathfrak{M}\models \mathsf{Con}(T_1+h_{\varepsilon_0}(a+1)\mbox{ is defined})$. But the latter would imply that $\mathfrak{M}\models \mathsf{Con}(\mathsf{PA}+\mathsf{Con}(S_a))$ and hence $\mathfrak{M}\models \mathsf{Con}(S_a)$, contradiction.

I don't see how you thought to achieve the desired effect with your Construction 2. Let us consider a model $\mathfrak{M}$ of $T_1$ where we have $\mathfrak{M}\not\models \mathsf{Con}(S_a)$, for some non-standard $a$ (such a model could be constructed using injecting inconsistencies theorem). Without loss of generality we could assume that $a$ is the least non-standard number with this property. Assume for a contradiction that $\mathfrak{M}\models \mathsf{Con}(T_2)$. It is easy to see that for any $b<a$ we have $\mathfrak{M}\models \mathsf{Prv}_{\mathsf{PA}}(\mathsf{Con}_{2^{b^2}}(S_b))$. Hence we have $\mathfrak{M}\models \mathsf{Con}(T_2+\mathsf{Con}_{2^{(a-1)^2}}(S_{a-1}))$. Thus we have $\mathfrak{M}\models \mathsf{Con}(\mathsf{PA}+\mathsf{Con}(S_{a-1}))$ and therefore $\mathfrak{M}\models \mathsf{Con}(S_a)$, contradiction.

A more natural example of a descending chain that I know is based on the notion of slow consistency. For a computable function $f$ let $$\mathsf{PA}\upharpoonright f =\{\mathsf{I}\Sigma_x\mid f(x) \mbox{ is defined}\}.$$ In the case when $f$ is total but not provably total in some theory $T$ the theory $\mathsf{PA}\upharpoonright f$ from the external point of view just coincide with $\mathsf{PA}$, but $T$ might not be able to prove that $\mathsf{PA}$ and $\mathsf{PA}\upharpoonright f$ coincide. The sentences $\mathsf{Con}(\mathsf{PA}\upharpoonright f)$ are known as slow consistency sentences and were introduced by Friedman, Rathjen, and Weiermann. For rationals $q>0$ let me consider the functions $f_{q}(x)=\mathsf{h}_{\varepsilon_0}([qx])$. Let $T_q=\mathsf{I}\Sigma_1+\mathsf{Con}(\mathsf{PA}\upharpoonright f_q)$. The claim is that for $p>q>0$ we have $T_q\vdash \mathsf{Con}(T_p)$. Let me reason in $T_q$. Actually I will present a model-theoretic argument that isn't directly available in an extension of $\mathsf{I\Sigma}_1$, but with some additional care it could be formalized in $\mathsf{WKL}_0+\mathsf{Con}(\mathsf{PA}\upharpoonright f_q)$ and then transfered to $T_q$ by the arithmetical conservativity of $\mathsf{WKL}_0$ over $\mathsf{I}\Sigma_1$. First assume that $f_q$ is total, this actually is equivalent to $\Sigma_1$-soundness of $\mathsf{PA}$, and it is fairly easy to prove consistency of $T_p$ in this case. Now we assume that there is the number $a$ s.t. $f_q(a)$ is defined but $f_q(a+1)$ is not. Since we externally know that $f_q$ is total, for any given $N$ we could prove in $T_q$ that $a>N$. By taking $N$ to be large enough we prove in $T_q$ that there is a number $b$ s.t. $f_p(b)$ is undefined and $[bp]<[ap]$. Clearly we have $\mathsf{PA}\upharpoonright f_q=\mathsf{I}\Sigma_a$. We construct a model $\mathfrak{M}$ of $\mathsf{I}\Sigma_a$. If $f_p(a)$ is undefined in $\mathfrak{M}$, then we are done since $\mathfrak{M}\models \mathsf{PA}\upharpoonright f_p\subseteq \mathsf{I}\Sigma_{a-1}$, $\mathsf{I}\Sigma_a\vdash \mathsf{Con}(\mathsf{I}\Sigma_{a-1})$ and hence $\mathfrak{M}\models \mathsf{Con}( \mathsf{PA}\upharpoonright f_p)$. Otherwise, in $\mathfrak{M}$ we have a non-standard interval $[f_p(b),f_p(a)]$. Using the fact that $[pb]<[pa]$ it is easy to show that $\mathfrak{M}\models A(f_p(b))<f_p(a)$, where $A(x)$ is the diagonal of Ackermann's function. From Sommer's results it follow that there is a cut $\mathfrak{J}\models \mathsf{I}\Sigma_1$ of $\mathfrak{M}$ such that $f_p(b)<\mathfrak{J}<f_p(a)$. Clearly we have $$\mathfrak{J}\models \mathsf{Con}(\mathsf{I}\Sigma_{a-1})\;\;\;\mbox{ and }\;\;\;\mathfrak{J}\models f_p(a)\mbox{ is undefined}$$ and hence $\mathfrak{J}\models \mathsf{Con}(\mathsf{PA}\upharpoonright f_p)$.

As for your last conjecture. It is known that for any sound arithmetical theory $U$ and a recursive chain $T_i$ of r.e. extensions of $U$ it couldn't be the case that $U\vdash \forall x\;(\mathsf{Prv}_{T_x}(\mathsf{Con}(T_{x+1})))$ (this is due to Friedman, Smorynski, and Solovay; in my paper with Walsh that I mentioned earlier we give a simple proof of this (Theorem 3.6); you could find reference to the earlier works about it there just before Theorem 3.6).

Through this answer I mentioned several times construction of models of arithmetic as cuts of non-standard intervals and construction of non-standard models of arithmetic by injecting inconsistencies in other non-standard models of arithmetic. Here are the relevant references:

R. Sommer. Transfinite induction within Peano arithmetic. Annals of Pure and Applied Logic, 76(3):231 – 289, 1995.

J. Krajíček and P. Pudlák. On the structure of initial segments of models of arithmetic. Archive for Mathematical Logic, 28(2):91–98, 1989.

Answer 3

Informed by Fedor Pakhomov's excellent answer, and using "slow" iterated $Σ_1$-soundness, here is an infinite sequence of sound theories $T$ such that $T_i$ = PA + 1-Con($T_{i+1}$).

Set $T_i$ = PA + "$h'_{g(n)∸i}(n)$ is total"
using fast-growing or Hardy hierarchy $h$ (either one works), with $h'_α$ being $h_{ε_α}$, and $g(n) = {h'_{ω+1}}^{-1}(n)$, where $f^{-1}(n) = \max(m: ∀m'<m \,\, f(m')<n)$ (or any reasonable variation on this). Also, $a∸b = \max(a-b,0)$.

Alternatively, almost any reasonable monotonic total recursive $g$ that is sufficiently slow-growing but tending to infinity works, but note that $T$ depends on $g$. The construction also generalizes to other theories extending $Σ^0_1$-PA (the proof uses $Σ^0_1$ induction) by replacing $h'_m(n)$ with a function corresponding to $1+m$ iterations of $Σ_1$-soundness.

Provably in PA, if $g$ is unbounded (equivalently, $h'_{ω+1}$ is total), then $T_i$ (and even PA + "$h'_ω$ is total") is $Σ_1$-sound. Thus, it suffices to prove that for each $i$, PA + "$g$ is bounded" proves "$h'_{g(n)∸i}(n)$ is total" $⇔$ 1-Con($T_{i+1}$). (However, the quantification over $i$ will be unprovable even in $T_0$).

Working in PA + "$g$ is bounded", let $k$ be the the maximum value of $g$. Since $k$ is (externally) nonstandard, $k>i$. Because 1-Con is unaffected by true $Π^0_1$ statements, in 1-Con(...), we can freely assume/assert that $k$ is the maximum value of $g$. Thus, 1-Con($T_{i+1}$) $⇔$ 1-Con(PA + "$h'_{k-(i+1)}(n)$ is total") $⇔$ "$h'_{k-i}(n)$ is total" (the latter follows from standard results in ordinal analysis), as required.

Addendum ($Σ^1_1$-soundness): Per the linked paper in Fedor Pakhomov's answer, the $Σ^0_1$ soundness cannot be improved to $Σ^0_2$ (equivalently $Π^0_3$) for c.e. (in $i$) $T$. However, if $T$ is not required to be computable enumerable in $i$, there is an infinite sequence $T_i$ of sound c.e. extensions of Z$_2$ such that each $T_i$ proves $Σ^1_1$-soundness of $T_{i+1}$. $T_i$ will be satisfied by every transitive model of Z$_2$ (and analogously for theories other than Z$_2$ extending $Π^1_1$-CA$_0$).
   To see this, given a recursive ordering $X$, let $T_a$ state Z$_2$ plus existence of a real $M$ such that for all $b ≤_X a$, $M_b$ is a (countably coded) $ω$ model of Z$_2$, and for all $c <_X b$, $M_c$ is an element of (the model coded by) $M_b$. Such $M$ exists for all $a$ in the well-founded part of $X$, so if $X$ is a recursive pseudowellordering, then such $M$ must also exist for some $a'$ outside of the well-founded part of $X$. If $a_i$ with $a_0=a'$ is an infinite $X$-descending sequence, then $T_{a_i}$ proves $Σ^1_1$-soundness $T_{a_{i+1}}$. Also, I suspect that there are sound finitely axiomatizable $T_i = Π^1_1\text{-CA}_0 + \mathrm{RFN}_{Σ^1_1}(T_{i+1})$, and similarly with many $Σ^1_1$ strengthenings of $\mathrm{RFN}_{Σ^1_1}$.