Skip to main content
2 of 2
added a nonrecursive construction with $Σ^1_1$ reflection
Dmytro Taranovsky
  • 7.5k
  • 1
  • 22
  • 45

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

Dmytro Taranovsky
  • 7.5k
  • 1
  • 22
  • 45