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}))$.


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.

  • $\begingroup$ I believe that one can also use the ideas of the universal algorithm (see jdh.hamkins.org/…), using essentially the assertions that the algorithm has $i$ successful stages. The nature of the extension property is that every model in which the algorithm has exactly $i$ stages thinks it is consistent (over a nonstandard fragment of its $\text{PA}$) that it has exactly $i+1$ stages. So this is an infinite descent. $\endgroup$ – Joel David Hamkins Jan 13 at 16:09
  • $\begingroup$ This is a good example. Note that ZFC + $ψ_i$ also works (since provably in ZFC, if a measurable is consistent, then so are ZFC + $ψ_i$); an optional change is to have $ω$ inaccessibles if a measurable is consistent. Also, the unsound $T_i$ = ZFC + $ψ_i$ + ¬Con(ZFC+measurable) proves not only consistency but $Π^V_2$ soundness of $T_{i+1}$, which (per the link in Fedor Pakhomov's answer) would not be possible for even $Π^0_3$ soundness for $Π^0_3$ sound $T_i$. $\endgroup$ – Dmytro Taranovsky Jan 14 at 8:38
  • $\begingroup$ (correction to my comment) $Π^V_2$-soundness should have been $Σ^V_2$-soundness (though there are variations for $Π^V_n$-soundness). $\endgroup$ – Dmytro Taranovsky Jan 14 at 10:39

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.

  • $\begingroup$ Thank you for the detailed answer. With its help, I added a new answer; let me know if there are gaps in the proof. Also, in the first $T_i$ you give, does "equivalently given as ..." work as EA does not appear to have enough induction to get the least counterexample to the totality of $R_{\mathrm{IΣ}_2}$? Also, near the end of the answer (about the conjecture) "some $T_i$" should be "all $T_i$" (since we can make $T_0$ arbitrarily strong). $\endgroup$ – Dmytro Taranovsky Jan 14 at 9:11
  • $\begingroup$ @DmytroTaranovsky Indeed, you are right the alternative definition of $T_i$'s in the first example, shouldn't be equivalent to the initial one; one would need to use $\mathsf{I}\Sigma_1$ as the base theory to overcome this problem. $\endgroup$ – Fedor Pakhomov Jan 14 at 9:51
  • $\begingroup$ @DmytroTaranovsky And you are right about the verification of the fact that a chain of theories is $<_{\mathsf{Con}}$-descending. The theorem in the paper by Walsh and me was that this couldn't be verified in $\mathsf{EA}$ (I don't remember the precise formulations Smorynski and Solovay used). This could be generalize to the result that for any sound r.e. arithmetical $U\supseteq \mathsf{EA}$ and recursive chain $T_i$ of extensions of $U$ it couldn't be the case that $U\vdash \forall x\;\mathsf{Prv}_{T_x}(\mathsf{Con}(T_{x+1}))$. But I don't know how to prove your conjecture. $\endgroup$ – Fedor Pakhomov Jan 14 at 10:02

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}$.

  • $\begingroup$ It is a nice example. And I don't see any gaps in the construction. $\endgroup$ – Fedor Pakhomov Jan 14 at 10:18

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Not the answer you're looking for? Browse other questions tagged or ask your own question.