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


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

  • 20
    $\begingroup$ Harvey, let me be the first to welcome you to MathOverflow! $\endgroup$ – Joel David Hamkins Sep 21 '10 at 13:33
  • $\begingroup$ Harvey, I am not sure I understand the question then. There are examples of groups with non-recursive Dehn functions, and with Dehn functions unbounded by any (finitely) iterated exponents. The simplest example of the latter is Platonov's theorem about the Dehn function of $\langle a,b | a^{a^b}=a^2\rangle$. The theorems in the papers in question are about arbitrary groups and their Dehn functions and the complexity of their word problem. That includes Platonov's example, earlier examples by Novikov and Boone of groups with non-recursive Dehn functions, and many others. $\endgroup$ – Mark Sapir Sep 21 '10 at 13:35
  • 2
    $\begingroup$ I am new to this site. I already sent in a comment on this, and cliked Add Comment. Did it appear? $\endgroup$ – Harvey Friedman Sep 21 '10 at 14:59
  • $\begingroup$ @Harvey: Do you mean your answer above? Yes, I see it. I just do not understand the words "give rise". For example, does Platonov's example give rise to the function which is an iterated exponent. That is the function that bounds (from below) the length of a rewriting proof that a given word in that group is equal to 1 in that group. $\endgroup$ – Mark Sapir Sep 21 '10 at 17:13

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.

  • 1
    $\begingroup$ @Harvey: One of the statements in one of the two papers I mention is this: For every Turing machine $M$ with time function $T(n)$ recognizing language $L$ there exists a finitely presented group $G$ (and its presentation can be explicitly written down) with Dehn function $\sim T^4(n)$. There is also a ("nice") function $f$ from words in the alphabet of $L$ to products of generators of $G$ such that $f(w)=1$ in $G$ iff $w\in L$. That is the group "recognizes" the same language as $M$. Now what if $M$ is very "bad", so that $T(n)$ is bigger than, say, any primitive recursive function? $\endgroup$ – Mark Sapir Sep 22 '10 at 0:41

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.

  • 4
    $\begingroup$ My favorite example of a statement not provable in EFA is this: If n >> k and f:[n]^k into [r], there exists distinct a_1,...,a_k+1 such that f(a_1,...,a_k) = f(a_2,...,a_k+1). Here [n] = {1,...,n}. This is an item in what I called "adjacent Ramsey theory". $\endgroup$ – Harvey Friedman Sep 22 '10 at 2:07
  • $\begingroup$ Please change n >> k to n >> k,r. $\endgroup$ – Harvey Friedman Sep 22 '10 at 3:00

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.

  • $\begingroup$ So I guess for almost anything in modern arithmetic geometry, finite-order arithmetic is an upper bound on what one needs. Winding this down to PA would be the next step. $\endgroup$ – David Roberts Sep 5 '11 at 7:06

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.)


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).

  • 2
    $\begingroup$ Do the theorems involve only finitary mathematical objects? $\endgroup$ – S. Carnahan Sep 21 '10 at 10:15
  • 1
    $\begingroup$ Is arbitrary recursive function a finitary mathematical object? $\endgroup$ – Mark Sapir Sep 21 '10 at 13:04
  • 5
    $\begingroup$ For the purpose of investigating provability in EFA or PA or other systems, the general notion of recursive function is finitary. However, there is a problem with specific recursive functions. It is finitary if it is merely regraded as a partial recursive function. However, how do you know that it is defined everywhere? That represents a statement that may not be provable in EFA or PA. In any case, such rules make good sense, as can be seen by appropriate examples. Incidentally, it is well worth looking at cwru.edu/artsci/phil/Proving_FLT.pdf Harvey Friedman $\endgroup$ – Harvey Friedman Sep 22 '10 at 2:25
  • $\begingroup$ @Harvey: I agree. $\endgroup$ – Mark Sapir Sep 22 '10 at 2:42

"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). DOI: 10.1007/BF01565428, free eudml link.

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.

  • 1
    $\begingroup$ I'm rather curious as to what Friedman would say about this, journal issues aside. I suspect it must somehow be forbidden under the "finitary objects" clause... $\endgroup$ – Charles Dec 2 '11 at 4:57
  • 1
    $\begingroup$ Con(PA) is a perfectly well-behaved $\Pi^0_1$ statement in the language of PA. It says (under a suitable encoding) that for all natural numbers $n$, $n$ is not a Gödel number of a proof that 1=0. I don't know if it can be stated in EFA though. $\endgroup$ – none Dec 2 '11 at 7:28
  • $\begingroup$ Robinson arithmetic can be substituted for PA here. $\endgroup$ – David Roberts Dec 2 '11 at 7:45

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.