[FOM] 303: PA Completeness (restatement)
Andrej.Bauer at fmf.uni-lj.si
Mon Oct 30 17:54:56 EST 2006
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.
More information about the FOM