Are small sentences of Peano arithmetic decidable?
Recently there has been a discussion (here, here, here, and here) on the Foundations of Mathematics mailing list about completeness of Peano arithmetic (PA) with respect to “small” sentences. Harvey Friedman made several conjectures of the following kind: “All true small sentences of PA are provable.” He proposed measures of smallness, such as counting the number of distinct variables or restricting the depth of terms. Here are some statistics concerning such statements.
Consider the first-order language of PA with zero $0$, successor $S$, addition $+$ and multiplication $\cdot$. The axioms are:
$\lnot (S x = 0)$
$S x = S y \Rightarrow x = y$
$x+0 = x$
$x+S y = S(x+y)$
$x \cdot 0 = 0$
$x \cdot Sy = (x \cdot y) + x$
$R(0) \Rightarrow (\forall x, R(x) \Rightarrow R(S x)) \Rightarrow R(x)$
By Gödel's Theorem we know there exist undecidable sentences in PA. But just how small are the smallest undecidable sentences? The sentences we get from proofs of Gödel's Theorem are huge, so there ought to be some smaller ones. We can ask the same question from a different perspective: does PA decide all small sentences? If there is an undecidable sentence comparable in size to the axioms of PA, then PA is missing something important.
A while ago Harvey Friedman, John Langford and I already investigates decidability of small existentially quantified sentences. It turned out that among those, Diophantine equations were the hardest to decide in general. By exhaustive search we found two which gave a professional number theorist something to munch on for a couple of weeks. They were:
$\exists a \; b \; c, a^2 - 2 = (a+b) b c$
$\exists a \; b \; c, a^2 + a - 1 = (a+b) b c$
Incidentially, the property “$a$ is a prime” can be expressed succinctly as $\forall b\; c, \lnot (a = (S (S b)) \cdot (S (S c)))$. If I am not mistaken, it is not known whether there exist infinitely many primes of the form $a^2 - 2$ (these are known as near-square primes). This gives us a fairly short sentence whose status is unknown:
$\forall a \exists b \forall c \; d, \lnot ((a+b)\cdot(a+b) = S (S ((S (S c)) \cdot (S (S d))))$.
Read the above as: “For every $a$ there is $b$ such that $(a+b)^2 - 2$ is a prime.” If you know an even “smaller” open problem, please let me know. In particular, can we reduce the number of nested quantifiers to something simpler than $\forall \exists \forall$? I suspect there might be fairly short Diophantine equations whose status is unkown.
In the attached Mathematica notebook, I used Mathematica
FindInstance function to count how many Diophantine equations have solutions and how many do not. As you will see, Mathematica is pretty good at this sort of thing. Unfrtunately, we do not get very far by brute force enumeration of all equations. For better results we would have to use more advanced enumeration techniques which avoid generation of equations which are known in advance to be decidable.
Attachment: diophantine.nb (also available as PDF diophantine.pdf).