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.