The disjunction property in Peano Arithmetic?

Let $\phi,\psi\in\Pi_1^0$ be independent of PA. Is the disjunction $\phi\vee\psi$ independent of PA?

-

The answer is no, and here is a counterexample. The proof relies on the double fixed point lemma, a generalization of the usual Goedel fixed point lemma producing two statements forming a fixed point with respect to a system, and I provide a proof below. Using it, we may produce two distinct sentences $\phi$ and $\psi$ such that

• $\phi$ asserts that for every proof of $\phi$, there is a smaller proof of $\psi$, and
• $\psi$ asserts that for every proof of $\psi$, there is a smaller proof of $\phi$.

In this case, each of these statements has complexity $\Pi^0_1$. Let me argue that they are independent.

First, observe that both $\phi$ and $\psi$ must be true in $\mathbb{N}$. If $\phi$ were false, then there would be a standard proof of $\phi$, having no smaller standard proof of $\psi$. In particular, $\phi$ would be a provable, false statement, contradicting $\mathbb{N}\models$PA. A symmetric argument applies to $\psi$.

Second, observe that neither is provable (meaning provable in PA throughout). If $\phi$ were provable, then there would be a standard proof of $\phi$, and thus there would have to be a smaller standard proof of $\psi$, and so $\psi$ would be true, and so there would be an even smaller standard proof of $\phi$. Thus, there could be no smallest proof of $\phi$, a contradiction. And the same for $\psi$.

Thus, both the sentences are true unprovable assertions, and hence independent.

Finally, observe that the disjunction $\phi\vee\psi$ is provable. If both $\phi$ and $\psi$ fail in a model of PA, then that model would have proofs of both $\phi$ and $\psi$, but neither statement could have the smallest proof, for if it did, then the other statement would be true, contrary to assumption. This contradicts PA, since the smallest proof of one of them must be smaller than any proof of the other.

Thus, we have independent $\Pi^0_1$ statements $\phi$ and $\psi$, such that $\phi\vee\psi$ is provable.

Here is the double fixed point lemma, which I believe is due to Smullyan, connected with his double recursion theorem. I use $[\phi]$ here to denote the Goedel code of $\phi$.

Double Fixed Point Lemma. Suppose that $A(x,y)$ and $B(x,y)$ are two formulas, then there are sentences $\phi$ and $\psi$ such that

• $\phi$ is provably equivalent to $A([\phi],[\psi])$, and
• $\psi$ is provably equivalent to $B([\phi],[\psi])$.

Proof. Let $\text{Sub}$ be the substitution operator, the primitive recursive function such that $\text{Sub}([\eta(x,y)],n,m)=[\eta(n,m)]$. Let $\theta_1(x,y)=A(\text{Sub}(x,x,y),\text{Sub}(y,x,y))$ and $\theta_2(x,y)=B(\text{Sub}(x,x,y),\text{Sub}(y,x,y))$. Let $n=[\theta_1(x,y)]$ and $m=[\theta_2(x,y)]$. Finally, let $\phi=\theta_1(n,m)$ and $\psi=\theta_2(n,m)$.

Observe that $\phi\iff \theta_1(n,m)\iff A(\text{Sub}(n,n,m),\text{Sub}(m,n,m))$ $\iff A([\theta_1(n,m)],[\theta_2(n,m)])\iff A([\phi],[\psi])$.

Also observe $\psi\iff \theta_2(n,m)\iff B(\text{Sub}(n,n,m),\text{Sub}(m,n,m))$ $\iff B([\theta_1(n,m)],[\theta_2(n,m)])\iff B([\phi],[\psi])$, as desired. QED

Note that we can arrange that $\phi$ and $\psi$ are distinct simply by ensuring that $\theta_1(n,m)$ and $\theta_2(n,m)$ are not syntactically the same sentence, such as by replacing $\theta_1(x,y)$ with its conjunction, but ensuring that $\theta_2(x,y)$ does not have such a form.

The lemma easily generalizes to any size system and indeed, to infinite systems of fixed points.

-
@Joel Can't we directly prove the fixed point statement you want? Let $Q_1$ be the operator which, given two statements F and G with free variables X and Y, returns F with the Godel codes of F and G substituted for X and Y; let $Q_2$ be the similar operator which substitutes into G. Let F be "For every proof of $Q_1(X, Y)$, there is a shorter proof of $Q_2(X, Y)$" and let G be vice versa. Then I think $(Q_1(F,G), Q_2(F,G))$ is your $(\phi, \psi)$. Unless I've done something dumb. –  David Speyer Apr 27 '11 at 16:26
If $\phi$ is false, then there is a proof of $\phi$ such that every proof of $\psi$ is longer. I don't understand the claim that the assumption that $\phi$ is false leads to the existence of a proof of $\psi$ (in particular a small proof of $\psi$). Am I missing something? –  Eric Hall Apr 27 '11 at 16:29
Eric, if $\phi$ is false in $\mathbb{N}$, then it would be a false but provable statement, which contradicts that PA is true in $\mathbb{N}$. So $\phi$ is true. (I had edited that paragraph to make this clearer, evidently just as you posted your comment.) –  Joel David Hamkins Apr 27 '11 at 16:41
David, I'm not quite clear on your proposal; your $F$ semms to have variables in it, but we need sentences. I believe that one can use those assertions along with the syntactic version of the double recursion theorem to find the desired fixed points, but I would be happier if I could find a clear reference for this. I think Smullyan did things very like this. –  Joel David Hamkins Apr 27 '11 at 16:46
$F$ has variables, but $Q_1(F,G)$, which does not, is $\phi$. The analogous way to build the Godel sentence is to let $Q$ be the operator which takes a statement $F$ about a variable $X$ and returns the sentence that $F$ holds when $X$ is replaced by the Godel number of $F$. Then Q("Not Q(X) is provable") is the Godel sentence. Unless I'm doing something dumb... –  David Speyer Apr 27 '11 at 17:07

One can in fact prove a bit more than Joel did. For example:

Let $X$ be any r.e. set such that for any $\phi\in X$, PA$+\phi$ is consistent. Let $\psi$ be any true $\Pi^0_1$ sentence. Then there are $\Pi^0_1$ sentences $\phi_0$ and $\phi_1$ such that:

1. PA $\vdash\phi_0\lor\phi_1$.
2. PA $\vdash\phi_0\land\phi_1\to\psi$.
3. None of $\phi_0,\phi_1,\lnot\phi_0,\lnot\phi_1$ is in $X$.

In particular, we can take $\psi$ to be provable and $X$ to be the set of theorems of PA, and we get a counterexample to the question.

This result is due to Per Lindström, and can be found in Chapter 7 of his beautiful and very recommended book, "Aspects of Incompleteness". The proof is an elaboration of the argument with Rosser sentences. It is a basic technical lemma used in the study of the interpretability degrees of consistent r.e. extensions of PA. (The degree of $T$ is the collection of all $T'$ that are bi-interpretable with $T$.)

For example, Lindström uses it to show that the degrees are dense, i.e., if $a\lt b$ then there is a $c$ with $a\lt c\lt b$.

By the way, the double fixed point lemma in Joel's answer is proved in Chapter 1 of Lindström's book. The reference given there is to "Theories Incomparable with Respect to Relative Interpretability", by Richard Montague, The Journal of Symbolic Logic, Vol. 27, No. 2 (Jun., 1962), pp. 195-211. As far as I can see, Smullyan does not prove this version in his "Theory of formal systems", Annals of Mathematics Studies, No. 47, Princeton University Press, Princeton, N.J. 1961. The modern presentation of Rosser sentences comes from Smullyan's book, though. The review by Kreisel in Math Reviews even called the book "the most elegant exposition of the theory of recursively enumerable (r.e.) sets in existence."

-
Thanks, Andres, for the references and remarks. In various books Smullyan does have his double recursion theorem, which amonnts to the analogous statement for computable functions, and uses it to build pairs and larger systems of self-referential sentences. But are we to credit the double fixed point theorem to Montague? –  Joel David Hamkins Apr 28 '11 at 10:41
Hi Joel. Yes, I think so. Montague states it in a somewhat peculiar language, but it is proved in his paper. As with the fixed point lemma, it may well be that Smullyan was responsible for its wide dissemination. –  Andres Caicedo Apr 28 '11 at 14:23

I think Carl's answer has the same error I originally made--it doesn't address that both formulas have to be $\Pi_1^0$. The negation of a $\Pi_1^0$ formula is $\Sigma_1^0$.

I think the actual answer is "yes" but several edit attempts haven't got the proof right, so I'll see if I can fix it offline instead of keeping on repeatedly editing.

-
Yes, I did miss that. I have deleted my answer, which didn't consider the syntactic classes of the formulas. –  Carl Mummert Apr 27 '11 at 14:30
Hmm, well, if you've got another answer please feel free to post it; I think this should be an easy problem but I keep getting stuck with my proof. Or I might try again later in the day. –  none Apr 27 '11 at 14:54
OK, I don't know Smullyan's double recursion theorem, but Joel's answer is certainly more likely than mine to be right. –  none Apr 27 '11 at 15:30
Joel, there is a gap. Applying the lemma, we may get $\phi$ provably equivalent to $\psi$. In this case $\phi\vee\psi$ is equivalent to $Con(PA)$. Then, the lenghts of nonstandard proofs are nonstandard numbers, which may be incompatible. So, we need another argument to show that $\phi\vee\psi$ can be proved. –  Alex Gavrilov Apr 28 '11 at 1:57

This is not actually an answer but rather a comment to Joel's answer. I am not very good in models, so here is an idea how to do without them. There is a theorem of Kreisel: if a $\Pi_1^0$ statement is provable in $T+\neg Con(T)$, then it is provable in $T$. In $PA+\neg Con(PA)$ we may prove that there exists the smallest code of a proof of $\phi$ and the smallest code of a proof of $\psi$. Denote them by $n_{\phi},n_{\psi}$. Then $\phi$ asserts that $n_{\psi}<n_{\phi}$ while $\psi$ asserts that $n_{\phi}<n_{\psi}$. Then $\phi\vee\psi$ means $n_{\phi}\neq n_{\psi}$ which is provalbe if $\phi$ and $\psi$ are syntactically different. By Kreisel, $\phi\vee\psi$ is provalbe in $PA$. (Note that the numbers $n_{\phi},n_{\psi}$ do not really exist).

-
It was very wrong of me to write that "nonstandard numbers may be incompatible". Perhaps, I did not wake actually up. If I only new how to edit comments.... What surprised me is how Joel managed to show that something is $provable$ by ruling out all the models where it is wrong. I did not expect this to be possible - but, as I said, I am not very good in models. –  Alex Gavrilov Apr 29 '11 at 3:19