[FOM] 303: PA Completeness (restatement)

[Andrej Bauer]

Harvey Friedman wrote:
> Thus for the sentence part of my Conjecture (restated above), we need only
> consider sentences of the form (forall x,y)(A) in the language 0,S,+,dot,
> where A is quantifier free.

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

Have fun solving these.

There are 101 terms of complexity at most 2 with variables x and y, 
after we put them in canonical form (write them as polynomials in two 
variables). We can form 5151 equations with these and quickly cut down 
to 2632 non-trivial ones using simplification procedues of Mathematica. 
So, to prove the conjecture one "just" needs to consider systems of up 
to 2632 Diophantine equations and inequations. This feels like a doable 
problem. The question is, what will we learn from investing in it?

If anoyone is interested I can publish the Mathematica notebook.

Andrej Bauer