Computable extension to $Σ_1$-sound system that is $Σ_2$-unsound?

Question

Recently, I wrote this post showing (if I did not make a mistake) essentially that:

For any nice formal system $S$ that is $Σ_1$-sound there exists some extension $S'$ that is $Σ_1$-sound but $Σ_2$-unsound. (Here "nice" is the usual kind of technical requirement, but you could simply assume that $S$ extends PA.)

In that same post I also sketched an argument that would easily imply that:

There exists a program that when given as input any nice formal system $S$ that is $Σ_1$-sound will output a formal system $S'$ that is $Σ_1$-sound but $Σ_3$-unsound.

Can we do better? Specifically:

Is there some program that when given as input any nice formal system $S$ that is $Σ_1$-sound will output a formal system $S'$ that is $Σ_1$-sound but $Σ_2$-unsound?

I cannot see how to convert my proof for the former theorem into a program. I also considered $T = S + ¬\text{Σ1-sound}(S)$, but although $T$ is clearly $Σ_2$-unsound, I fail to see why $T$ is $Σ_1$-sound. Can anyone construct such a program?

[Edit: I figured out a complete generalization to any level of the arithmetic hierarchy, and the proof is sketched in my answer.]

Answer 1

As a partial answer to your question, here is an explanation of why the theory $\mathrm{PA} + \neg\Sigma_1\textrm{-sound}(\mathrm{PA})$ is $\Sigma_1$-sound, where $\mathrm{PA}$ stands for (first order) Peano arithmetic (the reasoning does not apply just to $\mathrm{PA}$, but I don't have the courage to isolate exactly what hypotheses were used). Essentially, we need to reproduce Gödel's theorem but for a system that is $\Sigma_2$-axiomatizable instead of recursively axiomatizable. Specifically:

Let $\mathrm{PA}^{\Pi_1}$ stand for the theory obtained by adding to $\mathrm{PA}$ every true $\Pi_1$ statement of arithmetic (or, if you prefer, an axiom that states that $T$ does not halt for every Turing machine $T$ that, in fact, does not halt). Evidently, this theory is not recursively axiomatizable; however, it is $\mathbf{0}'$-axiomatizable (meaning, its axioms can be enumerated from the halting oracle); the set of theorems of $\mathrm{PA}^{\Pi_1}$ is therefore a $\Sigma_2$ set (by Post's theorem on the arithmetic hierarchy). Also, $\mathrm{PA}^{\Pi_1}$ is sound (because only sound axioms were added to it).

Now proceed as in Gödel's theorem, but “one level higher” in the arithmetic hierarchy (i.e., one Turing jump higher): in other words, consider the statement $G$ obtained by a fixed point theorem to mean “$G$ is not provable in $\mathrm{PA}^{\Pi_1}$”. Whereas the usual $G$ constructed similarly over $\mathrm{PA}$ is $\Pi_1$, this one is $\Pi_2$ (I explained above that the set of theorems of $\mathrm{PA}^{\Pi_1}$ is $\Sigma_2$); by the usual reasoning, $\mathrm{PA}^{\Pi_1}$ does not prove $G$. Again by lifting “one level higher” the proof of Gödel's second incompleteness theorem (by convincing oneself that the Hilbert-Bernays provability conditions hold), $\mathrm{PA}^{\Pi_1}$ does not prove the statement $\mathrm{Consis}(\mathrm{PA}^{\Pi_1})$ asserting its own consistency: note that $\mathrm{Consis}(\mathrm{PA}^{\Pi_1})$ can indeed be formulated in arithmetic, since $\mathrm{PA}^{\Pi_1}$ is arithmetically axiomatizable; however, like $G$ itself, it is a $\Pi_2$ statement (rather than a $\Pi_1$ statement as $\mathrm{Consis}(\mathrm{PA})$ is), so there is nothing really surprising in the fact that $\mathrm{PA}^{\Pi_1}$ cannot prove $\mathrm{Consis}(\mathrm{PA}^{\Pi_1})$.

Now what does $\mathrm{Consis}(\mathrm{PA}^{\Pi_1})$ really mean? It means that $\mathrm{PA}$ together with all true $\Pi_1$ statements of arithmetic does not prove $\bot$. But this is equivalent to saying that $\mathrm{PA}$ does not prove a false $\Sigma_1$ statement of arithmetic, in other words, $\mathrm{Consis}(\mathrm{PA}^{\Pi_1})$ is equivalent (over $\mathrm{PA}$, say), to $\Sigma_1\textrm{-sound}(\mathrm{PA})$. So the above reasoning shows that $\mathrm{PA}^{\Pi_1}$ does not prove $\Sigma_1\textrm{-sound}(\mathrm{PA})$, which means that $\mathrm{PA}$ together with all true $\Pi_1$ statements of arithmetic does not prove $\Sigma_1\textrm{-sound}(\mathrm{PA})$. This is, in turn, equivalent to saying that $\mathrm{PA} + \neg\Sigma_1\textrm{-sound}(\mathrm{PA})$ does not prove a false $\Sigma_1$ statement of arithmetic, in other words, $\mathrm{PA} + \neg\Sigma_1\textrm{-sound}(\mathrm{PA})$ is $\Sigma_1$-sound.

(I imagine all of this is very standard, but I don't know where it can be found. I rediscovered it myself, but I have no doubt it is well known to logicians. I don't even know where one can find a discussion of Gödel's theorems for systems which are $\Sigma_n$-axiomatizable instead of recursively axiomatizable as is usually assumed.)

Answer 2

Based on Gro-Tsen's answer, I believe that my proposed extension in my question should work in general, but needs $S$ to uniformly interpret PA. In contrast, I believe I have a way that only needs $S$ to interpret PA$^-$! (Note that PA$^-$ interprets TC, and the same holds for even weaker systems that merely interpret TC, where bounded quantifiers over TC means quantifiers over subwords of some variable.)

Take any $Σ_1$-sound formal system $S$ that has a proof verifier program and interprets PA$^-$. Let $S'$ be $S$ plus all true $Π_1$-sentences. Then $S'$ has a proof verifier program relative to the halting oracle $H$, and also can reason about programs relative to $H$, because such a program's halting and output is expressible as some $Σ_2$-sentence, and $S'$ proves every true $Σ_2$-sentence because it proves the $Π_1$ instantiation on the actual witness. Thus the computability proof of the incompleteness theorem applies (relativized), and hence $S'$ does not prove some true $Π_2$-sentence ($\neg W$ in the linked proof). Now the rest of the original non-constructive argument applies. Namely, $( S + W )$ is not $Σ_2$-sound, but is $Σ_1$-sound, otherwise it proves some false $Σ_1$-sentence $F$ and hence $( S + \neg F )$ proves $\neg W$, which is impossible because $S'$ does not prove $\neg W$.

And of course $\neg W$ is computable from $S$, because the proof verifier for $S'$ is computable from $S$ and the intermediate program constructed ($D$ in the linked proof) is computable from that, and the sentence stating the zero output of $D$ on itself is also computable from that. $ \def\code#1{\overline{#1}} \def\len{\text{len}} $

---

This proof generalizes to an arbitrary level of the arithmetical hierarchy. In particular:

We can given any $Σ_n$-sound $S$ compute a $Σ_n$-sound extension $S'$ that is $Σ_{n+1}$-unsound.

We can achieve this by relativizing the above proof to the truth oracle $H_n$ for $Σ_n$-sentences (the halting oracle was the truth oracle $H_1$ for $Σ_1$-sentences). Here $H_n$ takes as input an $n$-parameter $Δ_0$-sentence $Q$ (i.e. $n$-parameter arithmetical sentence with bounded quantifiers), and outputs the truth-value of $∃x_1\ ∀x_2\ ∃x_3\ \cdots\ x_n\ ( Q(x_{1..n}) )$. And truth here is relative to the standard model $\mathbb{N}$. Subsequently we shall write "$\code X$" for the code of $X$.

First we show that $H_n$ is captured by a $1$-parameter $Σ_{n+1}$-sentence $φ_n$, meaning that for any $n$-parameter $Δ_0$-sentence $Q$ we have that $H_n(Q)$ outputs true iff $φ_n(\code Q)$ is true. Obviously this holds for $n=0$, so by induction we can assume that $n>0$ and $H_{n-1}$ is captured by a $1$-parameter $Σ_n$-sentence $φ_{n-1}$. Now observe that $H_n(Q)$ is true iff $¬H_{n-1}(¬R(Q,y))$ is true for some $y$, where $R(Q,y)$ is the $(n-1)$-parameter sentence obtained from $Q$ by replacing the first parameter by $\code y$. Since $¬R$ is computable, its execution is captured by a $4$-parameter $Δ_0$-sentence $ψ$, meaning that for any $Q,y,Q'$ we have that $¬R(Q,y) = Q'$ iff $∃t\ ( ψ(\code Q,\code y,\code{Q'},t) )$ is true. Thus $H_n(Q)$ is true iff $φ_n := ∃y,r,t\ ( ψ(\code Q,y,r,t) ∧ ¬φ_{n-1}(r) )$ is true, and this $φ_n$ is clearly a $Σ_{n+1}$-sentence.

All that remains is to show that the output behaviour of a program $P$ that uses $H_n$ as an oracle can also be captured by a $Σ_{n+1}$-sentence $θ$, meaning that for every $u,v$ we have that $P$ halts on input $u$ and outputs $v$ iff $θ(\code P,\code u,\code v)$ is true. To do so, we simply include in the program trace all the oracle calls and results in the execution; $P(u) = v$ iff there is a program trace $t$ such that for each pair of consecutive states $A,B$ in $t$ we have that $P$ in state $A$ would proceed to state $B$. If $A$ specifies that $P$ will next call $H_n$ on input $q$, then $A$ must also specify the result $h$ of that call, and we must have $φ_n(\code q) ⇔ h$.

This gives us the sentence $θ := ∃t\ ∀i<len(t)\ ( \text{ $P$ in state $t[i]$ proceeds to state $t[i+1]$ } )$, in which the inner formula is $Σ_{n+1}$. It is not hard to see that $θ$ is also $Σ_{n+1}$, because "$∀i<\len(t)$" is bounded and can be 'moved past' the inner unbounded $∃$. Specifically, ( for each $i<\len(t)$ there is some $k$ such that ... ) is equivalent to ( there is some finite sequence $f$ of pairs such that for each $i<\len(t)$ there is some pair $⟨i,k⟩$ in $f$ such that ... ).

Finally, we can prove the generalized claim.

Take any $Σ_n$-sound formal system $S$ that has a proof verifier program and interprets PA$^-$. Let $S'$ be $S$ plus all true $Π_n$-sentences. Then $S'$ has a proof verifier program relative to the oracle $H_n$, and also can reason about programs relative to $H_n$, because such a program's output behaviour is (as shown above) captured by some $Σ_{n+1}$-sentence, and $S'$ proves every true $Σ_{n+1}$-sentence since it proves the $Π_n$ instantiation on the actual witness. Thus by the relativized incompleteness theorem, $S'$ does not prove some true $Π_{n+1}$-sentence ($\neg W$ in the linked proof). As before, $( S + W )$ is not $Σ_{n+1}$-sound, but is $Σ_n$-sound, otherwise it proves some false $Σ_n$-sentence $F$ and hence $( S + \neg F )$ proves $\neg W$, which is impossible because $S'$ does not prove $\neg W$.