Friedman [1] conjectured
Every theorem published in the Annals of Mathematics whose
statement involves only finitary mathematical objects (i.e., what logicians
call an arithmetical statement) can be proved in EFA. EFA is the weak
fragment of Peano Arithmetic based on the usual quantifier free axioms for
0,1,+,x,exp, together with the scheme of induction for all formulas in the
language all of whose quantifiers are bounded. This has not even been
carefully established for Peano Arithmetic. It is widely believed to be
true for Peano Arithmetic, and I think that in every case where a logician
has taken the time to learn the proofs, that logician also sees how to
prove the theorem in Peano Arithmetic. However, there are some proofs which
are very difficult to understand for all but a few people that have
appeared in the Annals of Mathematics – e.g., Wiles' proof of FLT.
Have there been any serious challenges to this or the weaker conjecture with Peano arithmetic in place of exponential function arithmetic?
Best Answer
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