Status of Harvey Friedman's grand conjecture? - MathOverflow most recent 30 from http://mathoverflow.net 2013-05-21T08:03:56Z http://mathoverflow.net/feeds/question/39452 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/39452/status-of-harvey-friedmans-grand-conjecture Status of Harvey Friedman's grand conjecture? Charles 2010-09-21T00:29:27Z 2011-12-02T07:43:08Z <p>Friedman [1] conjectured</p> <blockquote> <p>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 <a href="http://www.math.ohio-state.edu/~friedman/pdf/GodelLect060202.pdf" rel="nofollow" title="exponential function arithmetic">EFA</a>. 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.</p> </blockquote> <p>Have there been any serious challenges to this or the weaker conjecture with Peano arithmetic in place of exponential function arithmetic?</p> <p>[1] <a href="http://cs.nyu.edu/pipermail/fom/1999-April/003014.html" rel="nofollow">http://cs.nyu.edu/pipermail/fom/1999-April/003014.html</a></p> http://mathoverflow.net/questions/39452/status-of-harvey-friedmans-grand-conjecture/39481#39481 Answer by Mark Sapir for Status of Harvey Friedman's grand conjecture? Mark Sapir 2010-09-21T10:08:17Z 2011-10-17T15:29:41Z <p>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. <a href="http://arxiv.org/abs/math/9811105" rel="nofollow">arXiv:9811105</a></p> <p>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. <a href="http://arxiv.org/abs/math/9811106" rel="nofollow">arXiv:9811106</a></p> <p>disprove the Harvey Friedman's grand conjecture because arbitrary recursive functions are considered there.</p> <p>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).</p> http://mathoverflow.net/questions/39452/status-of-harvey-friedmans-grand-conjecture/39487#39487 Answer by Harvey Friedman for Status of Harvey Friedman's grand conjecture? Harvey Friedman 2010-09-21T11:13:52Z 2010-09-21T11:13:52Z <p>To Mark Sapir:</p> <p>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. </p> <p>It is also true that EFA is fully capable of proving recursive unsolvability theorems. </p> <p>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? </p> <p>Harvey Friedman</p> http://mathoverflow.net/questions/39452/status-of-harvey-friedmans-grand-conjecture/39503#39503 Answer by Richard Borcherds for Status of Harvey Friedman's grand conjecture? Richard Borcherds 2010-09-21T14:26:04Z 2010-09-21T14:26:04Z <p>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.</p> http://mathoverflow.net/questions/39452/status-of-harvey-friedmans-grand-conjecture/39559#39559 Answer by Harvey Friedman for Status of Harvey Friedman's grand conjecture? Harvey Friedman 2010-09-22T00:01:28Z 2010-09-22T00:01:28Z <p>To Mark Sapir:</p> <p>No, I had composed a comment and for some reason it didn't go through. Maybe it was too long for that comment box.</p> <p>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 <a href="http://www.cwru.edu/artsci/phil/Proving_FLT.pdf" rel="nofollow">http://www.cwru.edu/artsci/phil/Proving_FLT.pdf</a> </p> <p>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.</p> <p>It is not reasonable to explicitly allow indefinitely iterated exponentials in the statement. </p> <p>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. </p> <p>(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).</p> <p>Examples of this kind of unprovability (high rates of growth) are well known. Most well known is probably the Finite Ramsey Theorem. </p> <p>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.</p> <p>I also picked the Annals of Mathematics because I wanted to discard specialized and contrived examples, basically designed to test the conjecture.</p> <p>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 <em>appears explicitly</em> as a statement in the Annals of Mathematics. </p> <p>So I cannot tell yet whether you indeed have a counterexample to this conjecture. </p> <p>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. </p> <p>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. </p> http://mathoverflow.net/questions/39452/status-of-harvey-friedmans-grand-conjecture/74560#74560 Answer by David Roberts for Status of Harvey Friedman's grand conjecture? David Roberts 2011-09-05T07:05:03Z 2011-12-02T07:43:08Z <p>Colin McLarty has updated his <a href="http://arxiv.org/abs/1102.1773" rel="nofollow">paper</a> 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. </p> <p>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.</p> <hr> <p>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 <em>second-order</em> 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.</p> http://mathoverflow.net/questions/39452/status-of-harvey-friedmans-grand-conjecture/74580#74580 Answer by Emil Jeřábek for Status of Harvey Friedman's grand conjecture? Emil Jeřábek 2011-09-05T12:48:47Z 2011-09-05T12:48:47Z <p>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.)</p> http://mathoverflow.net/questions/39452/status-of-harvey-friedmans-grand-conjecture/82409#82409 Answer by none for Status of Harvey Friedman's grand conjecture? none 2011-12-01T21:05:11Z 2011-12-01T21:05:11Z <p>"Mathematische Annalen" and Annals of Mathematics aren't the same journal, but they have similar titles, so I'll try to slip this in.</p> <p>Gentzen's proof of Con(PA) using transfinite induction on $\epsilon_0$ appeared in Mathematische Annalen in 1936 (cite pasted from Wikipedia):</p> <ul> <li>G. Gentzen, 1936. 'Die Widerspruchfreiheit der reinen Zahlentheorie'. Mathematische Annalen, 112:493–565. Translated as 'The consistency of arithmetic', in (M. E. Szabo 1969).</li> </ul> <p>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.</p>