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?

• 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

2 Answers

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.

This proof generalizes to an arbitrary level of the arithmetical hierarchy. In particular, given any $Σ_n$-sound $S$ we can compute a $Σ_n$-sound extension $S'$ that is $Σ_{n+1}$-unsound, by relativizing to the truth oracle $H_n$ for $Σ_n$-sentences (the halting oracle was for $Σ_1$-sentences). The hard part lies in showing that the halting and output of a program relative to $H_n$ can be uniformly expressed as a $Σ_{n+1}$-sentence. This can be done by using each existentially quantified variable as a sequence. In particular, for any such program $P$ we can construct the query function $Q$ and the state transition predicate $R$, where $Q(s)$ represents the $n$-parameter sentence $φ$ that $H_n$ will tell the truth-value of $\exists x \forall y \cdots z ( φ(x,y,...,z) )$ and $R(s,t,u)$ represents that $s \to t$ is a valid state transition if $H_n(Q(s))$ is $u$, and can express "$P$ halts on $i$ and outputs $v$" as "$\exists x \exists y_0 \forall y_1 \exists y_2 \cdots y_n \Big($ $x$ starts with an input-$i$ state and ends with an output-$v$ state, and $x,y_0,...,y_n$ all have equal length, and for each $i$ from $0$ to $|x|-1$ we have $\big($ $R(x[i],x[i+1],0)$ and not $E(Q(x[i]),y_1[i],...,y_n[i])$ $\big)$ or $\big($ $R(x[i],x[i+1],1)$ and $E(Q(x[i]),y_0[i],...,y_{n-1}[i])$ $\big) \Big)$" using sequence coding, where $E(φ,u_1,...,u_n)$ represents the truth-value of $φ$ when evaluated on $(u_1...,u_n)$. One can check that any valid program execution can be translated to a state sequence and existential witnesses for each of the oracle's answers, which can be combined to witness the above sentence. The converse is clear.

• 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