Mathematics and Computation

A blog about mathematics for computers

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).

Comments

Andrej Bauer

I have to make a small correction. The sentence $\forall b \; c, \lnot (a = (S(S b))\cdot(S(S c)))$ does not mean "$a$ is a prime" but rather "$a$ is 0, 1 or a prime". Luckily, the short sentence with unknown status is not affected by this mistake.

jonathan

I believe that the "near-square" conjecture you state above is decidable. Since primality is diophantine, it can be determined with one existential quantifier. Therefore, the "near-square" conjecture is a universal-existential sentence, which is decidable by the result of Tung referenced here:

http://cs.nyu.edu/pipermail/fom/2006-October/011050.html

Jonathan

Andrej Bauer

Primality is diophantine, but as far as I am aware the equation(s) expressing it involve many variables, which gives us many existential quantifiers, not just one. And even if somehow we could express "n is prime" with a single existential "EE m. p(n,m)=0", would that not still give us a AA EE EE sentence "for all a there exists b and exists m such that p((a+b)^2 - 2, m)=0"? So I am afraid your comment does not convince me. (Note that Tung's result is about a single universal followed by a single existential.)

David

x+0=0 is a rather unusual axiom.

Andrej Bauer

Oops, thanks, I fixed the axiom so that it reads x+0=x.

Richard

“All true small sentences of PA are provable.”

Aren't all true sentences provable in general? Or, did I misunderstand the Completeness Theorem?

Interesting idea though.

Andrej Bauer

Yes, you misunderstand Gödel's Completeness Theorem. The theorem guarantees that valid formulae are provable, not true ones. The difference is perhaps a bit subtle: a formula is valid when it holds in every model. A formula is considered true when it holds in a preferred model (referred to as the standard model).

Lew

It appears that Hardy and Littlewood's conjecture that there are infinitely many primes of the form x^2+1 is still unsolved. This would give a sentence that is smaller by one symbol.

Wojowu

We can shorten this to $\exists a . \forall b . \exists c,d . S((a+b) \cdot (a+b))=S(S(c)) \cdot S(S(d))$ which says that all sufficiently large numbers of the form $n^2+1$ are composite. We don't know whether this is true or not yet.

How to comment on this blog: At present comments are disabled because the relevant script died. If you comment on this post on Mastodon and mention andrejbauer@mathstodon.xyz, I will gladly respond. You are also welcome to contact me directly.