[FOM] Fwd: 303: PA Completeness (restatement) (Andrej Bauer)
dana.scott at cs.cmu.edu
Wed Nov 1 23:57:28 EST 2006
In FOM Digest, Vol 46, Issue 40 (October 31),
Andrej Bauer asked about the provability in PA of two
quite short statements:
(1) exists x, exists y, x^4 = 1 + x + y^2
(2) exists x, exists y, x^2 (1 + y) = 1 + x + y^2
I concluded that both can be REFUTED. I outline two
arguments which can surely be done formally in PA.
(Ad 1) Look, for x = 0, 1, or 2 the euqation is impossible
for any natural number. Right?
Consider x^4 - 1 - x for x >= 3. That is a little
bit less than the square of x^2.
Now, if we think of any n^2, the square right BELOW it
is n^2 - 2 n +1 = (n - 1)^2.
Therefore, the square just below x^4 has to be
x^4 - 2 x^2 + 1.
However, (x^4 - 1 - x) - (x^4 - 2 x^2 + 1) =
2 x^2 - x - 2. That quantity is POSITIVE for x >= 2.
In other words, x^4 - 1 - x is never a square. Q.E.D.
(2) I checked that the equation has no integer solutions
up to x = 2,000,000. But that is not a proof.
So, solve the equation for y. The positive root is:
y = (x^2 + Sqrt(- 4 - 4 x + 4 x^2 + x^4))/2.
Note that this is in general a fraction.
For y to be an integer we should find out
something about what is under the square root sign.
If x is even, then the stuff under the root is even,
so the square root is even, so the numerator is even,
so y is an integer (if the root is an integer).
If x is odd, then x^4 is odd, so the stuff under the
root is odd, so the square root is odd, so the numerator
is even, so y is again an integer.
HENCE, the problem comes down to whether the stuff
under the root can ever be a SQUARE. Write it as
x^4 + 4(x^2 - x - 1).
Remark that for large x, the term x^4 is much larger
than 4(x^2 - x - 1).
Now 4(x^2 - x - 1) is larger than 2 x^2 + 1, so
x^4 + 4(x^2 - x - 1) might exceed the NEXT square after x^4.
But the SECOND square after x^4 is x^4 + 4 x^2 + 4, which is
LARGER than x^4 + 4(x^2 - x - 1). Q.E.D.
The point of these simple arguments is that there are bigger
and bigger gaps between squares.
More information about the FOM