[FOM] 303: PA Completeness (restatement)

[Pietro Kreitlon Carolino]

[Note to moderator: professor Scott's recent post has brought it to my
attention that my original message was bounced. However, I've become
interested in the (admittedly vague) question asked in its first
paragraph, and would like to hear from subscribers. Sorry for the
mix-up.]

---------- Forwarded message ----------
From: Pietro Kreitlon Carolino <pietro.kc at gmail.com>
Date: Nov 1, 2006 12:10 AM
Subject: Re: [FOM] 303: PA Completeness (restatement)
To: Andrej.Bauer at andrej.com, Foundations of Mathematics <fom at cs.nyu.edu>

[Original note to moderator: I'm not sure how interesting this is to
subscribers, or even how obvious, but for completeness I submit these
results to your judgement.]

On 10/30/06, Andrej Bauer <Andrej.Bauer at fmf.uni-lj.si> wrote:
> I have played with Mathematica to see which sentences of the forms
>
>    exists x, exists y, e1 = e2,
>    forall x, forall y, e1 = e2,
>
> with e1 and e2 terms of complexity at most 2, we can decide. Mathematica
> easily gets them all, except two Diophantine equations:
>
>    exists x, exists y, x^4 = 1 + x + y^2
>
>    exists x, exists y, x^2 (1 + y) = 1 + x + y^2

   I would like to know the proportion of ExEy sentences that came up
true in professor Bauer's Mathematica run. It might be interesting to
see how a "random sentence" of PA behaves truth-wise, maybe fixing
parameters like quantifier complexity, number of variables etc. Has
something like this been done, akin to random graph theory maybe?

   Anyway, the answer to both equations above is negative. Below are
technical details. They are a bit different in flavor from professor
Scott's proof, which gets the result with fewer resources (though both
are obviously formalizable in PA). It is interesting that we both
solved equations 1 and 2 in similar ways, though our methods differ
from each other. I wonder what the peculiarity is that prevented
Mathematica solving them.

   The second one is a bit easier, so I start off with it. Working mod
2, we see that

x = 1 --> 1+y = y^2 --> 1 = 0 (contradict.)
x = 0 --> y^2+1 = 0 --> y = 1

So x is even and y is odd. Mod 8, that means x^2 = 0 or 4, and y^2 = 1. So:

x^2 = 0 --> 0 = x+2 --> x = 6 --> x^2 = 4 != 0 (contradict.)
x^2 = 4 --> 4(1+y) = x+2 --> x+2 = 0 (as 1+y is even) --> x=6.

Therefore x = 6 (mod 8). But then x/2 = 3 (mod 4). Hence there exists
a prime q dividing x/2, with q=3(mod 4). Then, taking the original
equation mod q, we have:

x^2 (1 + y) = 1 + x + y^2 ---(mod q)---> y^2+1 = 0 (mod q)

which is well-known to be unsolvable for q=3 (mod 4).

   Now for the first equation. Rewrite x^4 = 1 + x + y^2 as

x^4 - x = y^2 + 1 <--> x(x-1)(x^2+x+1) = y^2+1

Reduce it mod x: then y^2+1 = 0 (mod x). As we reasoned above, x can
have no prime factors congruent to 3 mod 4. Also, the highest power of
2 to divide x is 0 or 1, otherwise y^2+1 = 0 (mod 4). If it were 0, x
would be =1 (mod 4) (as all its prime factors apart from 2 are), and
by the factorization above on the right, y^2+1 = 0 (mod 4) again.
Therefore:

x= 2*pq...r  where p,q,...,r are primes = 1 (mod 4)

In particular, x=2 (mod 4) (this will save some labor just ahead).

   On the other hand, working mod 2 on the original equation, y is
easily seen to be odd, and therefore y^2 = 1 (mod 8). So:

x(x-1)(x^2+x+1) = 2 (mod 8)

Trying x=2 and x=6 (mod 8), we see that only x=6 (mod 8) works. But
this gives x/2=3 (mod 4), contrary to the factorization obtained
above. Hence there is no solution.

Cheers,

--Pietro