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

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.]

• It seems to me that your claims are missing a soundness assumption on $S$, because if your original system $S$ is $\Sigma_1$-unsound, then of course the extension also will be $\Sigma_1$-unsound. – JDH Dec 16 '17 at 12:48
• @JDH: Yes sorry that was what I had in my original linked post. I've edited. – user21820 Dec 16 '17 at 14:41

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

• This is interesting! On first glance, it is essentially doing the same as in my linked post in the non-constructive version, except plus the trick of constructing Con(PA+Π1-truths). I hence think it in fact should produce a full answer to my question. I will check and get back to you. Thanks! =) – user21820 Dec 24 '17 at 6:55
• By the way, the computability-based proof of the incompleteness theorem trivially relativize, and hence apply to any formal system with a proof verifier program using some finite Turing jump, justifying your aside about Godel's theorems for systems that are $Σ_n$-axiomatizable. You're welcome to the Logic chat-room as well. =) – user21820 Dec 24 '17 at 7:03
• There are two issues with your answer: (1) You claim that if PA plus true $Π_1$-sentences proves contradiction then PA proves a false $Σ_1$-sentence. This is true based on soundness of PA, but you further claimed that PA proves Con(PA$^{Π_1}$)⇒$Σ_1$-Sound(PA). I do not see why it follows, unless you first prove that the conjunction of any two $Π_1$-sentences is provably equivalent over PA to a single $Π_1$-sentence. This is true by using pair coding, but should be pointed out. (2) You appear to be using soundness of PA to conclude that PA$^{Π_1}$ is sound. But this will not generalize. – user21820 Dec 26 '17 at 16:36
• Concerning (1): If PA is not $\Sigma_1$-sound, it proves a false $\Sigma_1$ statement, i.e., the negation $\neg P$ of a true $\Pi_1$ statement, so $\mathrm{PA}+P$ is inconsistent, and in particular $\mathrm{PA}^{\Pi_1}$ is; and all this reasoning can be held in PA, so PA proves $\mathrm{Consis}(\mathrm{PA}^{\Pi_1}) \Rightarrow \Sigma_1\textrm{-sound}(\mathrm{PA})$. No? Anyway, I'm certainly willing to believe that I used some standard facts on $\Pi_1$ statements in various places, including that the conjunction of two such is demonstrably equivalent to one. – Gro-Tsen Dec 26 '17 at 18:23
• Concerning (2): If $\mathrm{PA}^{\Pi_1}$ is inconsistent, then there is a finite conjunction of true $\Pi_1$ statements, hence a single true $\Pi_1$ statement, $P$, such that $\mathrm{PA}+P$ proves $\bot$, i.e., $\mathrm{PA}$ proves $\neg P$, so PA is not $\Sigma_1$-sound. So just $\Sigma_1$-soundness of PA will ensure the consistency of $\mathrm{PA}^{\Pi_1}$. But as I mentioned from the start, I don't have the courage to isolate the exact minimum hypotheses being used at each point. – Gro-Tsen Dec 26 '17 at 18:30

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

• I think this is correct, but in the interest of completeness you should clarify what "TC" is (I was able to guess "Theory of Concatenation" but this is definitely not a standard acronym). – Gro-Tsen Dec 27 '17 at 18:09
• @Gro-Tsen: Thank you! I've clarified it. =) – user21820 Dec 28 '17 at 3:05