FOM: 23-symbol formulas

[Harvey Friedman]

Reply to M. Frank 3:55AM 10/26/99:

>In his post #65, Harvey Friedman conjectured that
>
>CONJECTURE 1.1. Let phi be a formula in the language of PA with at most 20
>symbols. The universal closure of phi is provable or refutable in PA.

To put this in perspective, the whole of the technical content of posting
#66, PA/an approch, 8:02PM 10/21/99, is to devise a good plan for proving
Conjecture 1.1 for formulas without quantifiers, and with 20 replaced by
14. This is already challenging, and suggests all sorts of number theoretic
questions, many of which are probably doable - as can be seen in posting
#66.

And, as indicated in #66, one is ultimately interested in doing this for 14
where quantifiers and schematic letters are allowed. In this ultimate form
for 14, one does get information about PA with ostensibly great
foundational import. This is because PA itself is made up of such formulas.
And the obvious objection that the number of symbols in this setup is an
artificial measure should be soundly dispensed with by showing that the
same kind of results hold for a huge range of measures of simplicity.

>I just wanted to point out that this conjecture, even if true as stated,
>would be very hard to extend at all past the number 20.  For instance, (so
>far as I can tell from a MathSciNet search) it is still an open question
>in number theory whether there are infinitely many primes of the form x^2
>+ 1, i.e. whether the universal closure of the 23-symbol formula
>
>(exists b)(forall c)(forall d) not s[(a+b)*(a+b)] = ssc * ssd
>
>is true.  (The best result seems to be by Iwaniec in 1978, that infinitely
>many numbers of form x^2 + 1 are products of two primes.)

This is an important point which is cleverly done and I appreciate it very
much. I wonder if this is tight in the sense that you can't do something
like this for 22 instead of 23? I may well have picked a good, safe - but
challenging - number, 20, for my conjecture.

Also, it does seem that one would have to go quite a bit beyond 23 in order
to do such a thing without quantifiers.

In any case, one might try eventually for a result like this: find a small
finite number of simple open number theoretic questions with the property
that the universal closure of every formula of PA with at most 23 symbols
is provably equivalent in PA to a Boolean combination of these questions -
or even provably equivalent in PA to one of these questions or its
negation.

>Unfortunately, I haven't figured out the relationship of Conjecture 1.1
>to the other conjectures in Friedman's post #65, and so don't know how
>relevant this is to the ideas that the axioms of number theory are forced
>on us by their simplicity.

It does not, on the face of it, prevent us from establishing that the
axioms of number theory are forced upon us by their simplicity, since that
can be done along the lines indicated by considering only schemes with at
most 14 symbols.

>The only moral I can draw is that, in a list
>of formulas by simplicity, open problems will show up much before the
>formulas we can currently prove undecidable.

Absolutely, and that is very important to know.