Status of Harvey Friedman's grand conjecture?

To Mark Sapir:

The conjecture says "can be proved in EFA". If it "was not proved in EFA" then that does not count. However, I am still interested if it "was not proved in EFA". Since EFA can still develop some theory of recursive functions, the fact that recursive functions are mentioned, or even used, does not imply that the proof is outside EFA.

It is also true that EFA is fully capable of proving recursive unsolvability theorems.

The only proofs we have that given mathematical statements are not provable in EFA is to show that the mathematical statements inherently give rise to functions that are not bounded by any finite height exponential stack. Is this definitely the case here? Or is there a conjecture to that effect?

Harvey Friedman

To Mark Sapir:

No, I had composed a comment and for some reason it didn't go through. Maybe it was too long for that comment box.

A key question is whether FLT can be proved in EFA, or even PA. Note that FLT does not mention indefinitely iterated exponentials, but it still may not be provable in EFA. Angus MacIntyre has a manuscript with an attempt at proving FLT in PA = Peano Arithmetic. Take a look at http://www.cwru.edu/artsci/phil/Proving_FLT.pdf

EFA proves various standard facts about nonrecursive functions, including that such and such is not algorithmically decidable. So that doesn't imply unprovability in EFA.

It is not reasonable to explicitly allow indefinitely iterated exponentials in the statement.

So this leaves us with the usual examples of known unprovability in EFA. This is typically where we have a statement of the form (forall n)(therexists m)(something innocent holds), where there is no definitely iterated exponential bound on m in terms of n.

(This is not to rule out more subtle cases of unprovability in EFA that do not involve high rates of growth. Very specifically, e.g., FLT and appropriately formulated versions of Mordell's Conjecture. But we do not know if this is the case).

Examples of this kind of unprovability (high rates of growth) are well known. Most well known is probably the Finite Ramsey Theorem.

I made the conjecture that in the standard revered core mathematics, this does not happen. Rather than use "standard revered core mathematics", I pointed to the Annals of Mathematics - sometimes with qualifications that the article not be written by people referring to themselves as logicians.

I also picked the Annals of Mathematics because I wanted to discard specialized and contrived examples, basically designed to test the conjecture.

In order to see if in fact the conjecture has been refuted when taken literally - independently of whether the conjecture is true for, say, 99, 99.9 or 99.99 or 99.999 percent, or whatever - we should examine a very specific sentence "readily formalizable in the language of EFA: (which only includes 0,1,+,x,exponentiation, and quantifiers over nonnegative integers), which is not provable in EFA, and which appears explicitly as a statement in the Annals of Mathematics.

So I cannot tell yet whether you indeed have a counterexample to this conjecture.

Of course the real problem is to what extent EFA is sufficient to prove normal important fundamental mathematical statements already formulated in the natural course of mathematics to date. The Annals of Math question is a test question. There is a huge hierarchy of successively stronger systems starting with EFA (and some lower than EFA, but that is a different story), going up to PA and well beyond.

The next strongest system normally discussed is SEFA = super exponential function arithmetic, which surrounds the function 2^[n] = 2^2^...^2, where there are n 2's. FInite Rmasey Theorem is provable in SEFA. There are much more systems after that, but I will stop here.

Gowers proved a lower bound of "unbounded tower of exponentials" size for Szemeredi's lemma, which I think means this cannot be proved in EFA. So the question is whether any papers in Annals of math from before 2000 use this. A quick search of MathSciNet produces one paper related to Szemeredi's theorem from 1999 (Bergelson, V. Leibman, A. "Set-polynomials and polynomial extension of the Hales-Jewett theorem", mathscinet, eudml.) so this might be close to a counterexample, but I don't know if the large lower bound for Szemeredi's lemma translates into anything large for Szemeredi's theorem.