4
$\begingroup$

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

$\endgroup$
  • $\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
4
$\begingroup$

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

$\endgroup$
  • $\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
3
$\begingroup$

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

$\endgroup$
  • $\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.