Status of Harvey Friedman's grand conjecture? - MathOverflow

Status of Harvey Friedman's grand conjecture?

2010-09-21T00:29:27Z

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?

[1] http://cs.nyu.edu/pipermail/fom/1999-April/003014.html

Answer by Mark Sapir for Status of Harvey Friedman's grand conjecture?

2010-09-21T10:08:17Z

My papers Sapir, Mark V.; Birget, Jean-Camille; Rips, Eliyahu Isoperimetric and isodiametric functions of groups. Ann. of Math. (2) 156 (2002), no. 2, 345--466. arXiv:9811105

Birget, J.-C.; Olʹshanskii, A. Yu.; Rips, E.; Sapir, M. V. Isoperimetric functions of groups and computational complexity of the word problem. Ann. of Math. (2) 156 (2002), no. 2, 467--518. arXiv:9811106

disprove the Harvey Friedman's grand conjecture because arbitrary recursive functions are considered there.

Update: I am no longer sure that these papers are "counterexamples". It looks like I misunderstood the question. At least the theorems there are about finite objects (Turing machines and group presentations, computable numbers). But the proofs do not produce large functions. Of course some of the groups that can be constructed by the procedures described in the papers will have solvable word problem (which is also a finitary problem) in the ordinary sense but unsolvable word problem in the sense of EFA. But this is not explicitly written in the papers (because I and other co-authors did not know what EFA is till today).

Answer by Harvey Friedman for Status of Harvey Friedman's grand conjecture?

2010-09-21T11:13:52Z

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

Answer by Richard Borcherds for Status of Harvey Friedman's grand conjecture?

2010-09-21T14:26:04Z

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".) so this might be close to a counterexample, butI dont know if the large lower bound for Szemeredi's lemma translates into anything large for Szemeredi's theorem.

Answer by Harvey Friedman for Status of Harvey Friedman's grand conjecture?

2010-09-22T00:01:28Z

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.

Answer by David Roberts for Status of Harvey Friedman's grand conjecture?

2011-09-05T07:05:03Z

Colin McLarty has updated his paper on the foundations necessary for Grothendieck-style algebraic geometry. The punchline is that only finite-order arithmetic is necessary for all the derived functor cohomology technology, for an arbitrary small site.

The second punchline is that of course for a specific arithmetic problem, one only needs a countable site, and one can, in principle, arrive at a bound on what order arithmetic one needs. I say in principle because McLarty states that it may/will be difficult to perform the necessary arithmetic estimates for the whole of a rather lengthy proof.

Edit: McLarty now (1 December 2011) says that for derived functor cohomology over a Noetherian scheme, with coefficients in an arbitrary sheaf of modules (on the Zariski site), only requires second-order arithmetic. In particular, coherent cohomology falls under this umbrella. This also brings such results into the realm of reverse mathematics, which deals with hierarchies of theories of second-order arithmetic.

Answer by Emil Jeřábek for Status of Harvey Friedman's grand conjecture?

2011-09-05T12:48:47Z

The cut elimination theorem (for, say, classical first-order logic) is not provable in $I\Delta_0+\mathrm{EXP}$ (aka EFA), it requires $I\Delta_0+\mathrm{SUPEXP}$. While this is a theorem from logic rather than mainstream mathematics, it (and all kinds of related results) is so important that I’d be rather surprised if it were never mentioned in Annals of Mathematics. (On the other hand, Friedman must be well aware of this example, so presumably it is not supposed to count for whatever reason.)

Answer by none for Status of Harvey Friedman's grand conjecture?

2011-12-01T21:05:11Z

"Mathematische Annalen" and Annals of Mathematics aren't the same journal, but they have similar titles, so I'll try to slip this in.

Gentzen's proof of Con(PA) using transfinite induction on $\epsilon_0$ appeared in Mathematische Annalen in 1936 (cite pasted from Wikipedia):

G. Gentzen, 1936. 'Die Widerspruchfreiheit der reinen Zahlentheorie'. Mathematische Annalen, 112:493–565. Translated as 'The consistency of arithmetic', in (M. E. Szabo 1969).

Obviously this theorem can't be proved in PA itself, much less EFA. I guess it doesn't really count but it seems sort of relevant. It's surely a major theorem.