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?

  • $\begingroup$ 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. $\endgroup$ – JDH Dec 16 '17 at 12:48
  • $\begingroup$ @JDH: Yes sorry that was what I had in my original linked post. I've edited. $\endgroup$ – 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.)

  • $\begingroup$ 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! =) $\endgroup$ – user21820 Dec 24 '17 at 6:55
  • $\begingroup$ 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. =) $\endgroup$ – user21820 Dec 24 '17 at 7:03
  • $\begingroup$ 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. $\endgroup$ – user21820 Dec 26 '17 at 16:36
  • $\begingroup$ 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. $\endgroup$ – Gro-Tsen Dec 26 '17 at 18:23
  • $\begingroup$ 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. $\endgroup$ – 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.

  • $\begingroup$ 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). $\endgroup$ – Gro-Tsen Dec 27 '17 at 18:09
  • $\begingroup$ @Gro-Tsen: Thank you! I've clarified it. =) $\endgroup$ – user21820 Dec 28 '17 at 3:05

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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