By high school mathematics I mean Elementary Function Arithmetic (EFA), where one is allowed +,×, xy, and a weak form of induction for formulas with bounded quantifiers. This is much weaker than primitive recursive arithmetic, which is in turn much weaker than Peano arithmetic, which is in turn much weaker than ZFC that we normally work in.

However there seem to be very few theorems (about integers) that are known to require anything more than this incredibly weak system to prove them. The few theorems that I know need more than this include:
*Consistency results for various stronger systems (following Godel). This includes results such as the Paris Harrington theorem and Goodstein sequences that are cleverly disguised forms of consistency results.
*Some results in Ramsey theory, saying that anything possible will happen in a sufficiently large set. Typical examples: Gowers proved a very large lower bound for Szemeredi's lemma showing that it cannot be proved in elementary function arithmetic, and the Robertson-Seymour graph minor theorem is known to require such large functions that it is unprovable in Peano arithmetic.

I can think of no results at all (about integers) outside these areas (mathematical logic, variations of Ramsey theory) that are known to require anything more than EFA to prove. A good rule of thumb is that anything involving unbounded towers of exponentials is probably not provable in EFA, and conversely if there is no function this large then one might suspect the result is provable in EFA.

So my question is : does anyone know of natural results in "ordinary" mathematics (number theory, algebraic geometry, Lie groups, operator algebras, differential geometry, combinatorics, etc...) in which functions larger than a finite tower of exponentials occur in a serious way? In practice this is probably more or less equivalent to asking for theorems about integers unprovable in EFA.

Related links: http://en.wikipedia.org/wiki/Grand_conjecture about Friedman asking a similar question.

By the way, encoding deep results as Diophantine equations and so on is cheating. And please do not make remarks suggesting that Fermat's last theorem needs inaccessible cardinals unless you understand Wiles's proof.

  • 10
    $\begingroup$ Richard, the Ramsey like statements (like the Paris-Harrington result or the Kanamori-McAloon theorem), Goodstein's theorem, and the fact that the first player always wins the Hercules vs. the Hydra game are not "cleverly disguised" consistency statements. I'm not sure how the Paris-Harrington theorem or the Hercules vs. the Hydra result were discovered, but at least the other two examples were not obtained trying to code anything. They were combinatorial statements that logicians happened to look at and for which we could apply teh general "Indicators" techniques. $\endgroup$ Aug 24 '10 at 19:05
  • 6
    $\begingroup$ Also, Harvey Friedman has several examples that are (very?) natural and are not coding tricks in disguise. There is a draft of a book of his on these results ("Boolean relation theory") on his site. $\endgroup$ Aug 24 '10 at 19:06
  • 11
    $\begingroup$ Paris and Harrington were deliberately trying to construct a natural-looking combinatorial result equivalent to consistency of Peano arithmetic. Goodstein sequences were deliberately designed by Goodstein to encode ordinal induction up to &epsilon;<sub>0</sub>. And the Hydra game was found as an interpretation of Goodstein sequences. In other words, these examples were indeed all invented by logicians trying to encode consistency results. $\endgroup$ Aug 24 '10 at 19:51
  • 14
    $\begingroup$ You are asking a logic question, but you seem to count as cheating any answer that comes from logic, no matter how beautiful or amazing (e.g. Goodstein, Paris-Harrington, diophantine undecidability, etc.). Why should you exclude those methods and results? After all, if you are interested in what is provable in EFA, then consistency questions about EFA and related systems would seem to be both relevant and natural, especially because these logic results provide a thorough answer to your question with an intricate hierarchy of consistency strength. $\endgroup$ Aug 25 '10 at 0:25
  • 11
    $\begingroup$ I'm excluding examples from logic because I already know of many such examples. I am interested in finding out if there are other areas of mathematics that make serious use of logical systems of consistency strength stronger than EFA, to test the hypothesis that almost all "ordinary mathematics" could be done in an astonishingly weak logical system. $\endgroup$ Aug 25 '10 at 0:41

I don't know whether this is what you had in mind, but in 1980 Alex Wilkie showed that if one uses the axioms

  1. $x + y = y + x$
  2. $(x + y) + z = x + (y + z)$
  3. $x \cdot 1 = x$
  4. $x \cdot y = y \cdot x$
  5. $(x \cdot y) \cdot z = x \cdot (y \cdot z)$
  6. $x \cdot (y + z) = x \cdot y + x \cdot z$
  7. $1^x = 1$
  8. $x^1 = x$
  9. $x^{y + z} = x^y \cdot x^z$
  10. $(x \cdot y)^z = x^z \cdot y^z$
  11. $(x^y)^z = x^{y \cdot z}$,

then one cannot prove the (true) identity $$ ((1+x)^y+(1+x+x^2)^y)^x\cdot ((1+x^3)^x+(1+x^2+x^4)^x)^y $$ $$ \ \ \ \ \ \ \ \ \ = ((1+x)^x+(1+x+x^2)^x)^y\cdot ((1+x^3)^y+(1+x^2+x^4)^y)^x. $$ See http://en.wikipedia.org/wiki/Tarski%27s_high_school_algebra_problem.

  • 12
    $\begingroup$ I think EFA adds high school induction to Wilkie's axioms. I've no idea whether this is enough to prove that identity, since I go cross-eyed from just looking at it. $\endgroup$ Aug 25 '10 at 0:24
  • 10
    $\begingroup$ Also, surely you wouldn't be bothered much by having to add - to your list of "high school math," right? And that certainly solves this problem. $\endgroup$ Aug 25 '10 at 1:54
  • 20
    $\begingroup$ while this example is quite interesting. It seems Wilkie's trick was to find an expression without the "-" symbol (which is also absent from the 11 "axioms"), but whose simple formal proof would require it. I don't know how EFA is defined, but certainly it must allow for a definition of negation, with all the standard properties. $\endgroup$ Aug 25 '10 at 13:13

I believe this example may qualify. It is open whether Thompson's group $F$ is amenable.

We may present $F$ as $\langle A,B\mid [AB^{-1},A^{-1}BA]=[AB^{-1},A^{-2}BA^2]={\rm id}]\rangle$.

Amenability of a finitely presented group $G$ with finite generating set $\Gamma$ is equivalent to the finiteness of the Følner function $$ Føl_{G,\Gamma}(n)=\min(|X|\mid X\subseteq G,\text{ $X$ is ($1/n$)-Følner with respect to $\Gamma$} ), $$ where $X$ is $\varepsilon$-Følner with respect to $\Gamma$ iff $$ \sum_{\gamma\in\Gamma}|(X\cdot\gamma)\triangle X|<\varepsilon|X|. $$ Here, $\triangle$ denotes symmetric difference, as usual.

Justin Moore proved recently the following:

Theorem. For every finite symmetric generating set $\Gamma\subseteq F$ there is a constant $C>1$ such that if $X\subseteq F$ is a $C^{-n}$-Følner set with respect to $\Gamma$, then $X$ contains at least $exp_n(0)$ elements.

Here, $exp_0(n)=n$ and $exp_{m+1}(n)=2^{exp_m(n)}$.

This means that either $F$ is not amenable, or its amenability is not provable in primitive recursive arithmetic.

On the recent arguments about amenability or not of $F$, see this nice answer by Mark Sapir.

  • 3
    $\begingroup$ It certainly does qualify. Natural lower bounds of unbounded towers of exponentials are exactly what I was looking for. This is the first example I've seen outside logic or Ramsey theory. $\endgroup$ Aug 25 '10 at 3:54
  • $\begingroup$ There seems to be a claim that F is amenable: E.T. Shavgulidze, The Thompson group F is amenable, Infinite Dimensional Analysis, Quantum Probability and Related Topics, 12 (2009), no. 2, 173–191 $\endgroup$ Aug 25 '10 at 3:58
  • 4
    $\begingroup$ This claim has been discussed on MathOverflow here. mathoverflow.net/questions/26821/is-thompsons-group-f-amenable $\endgroup$ Aug 25 '10 at 11:53
  • $\begingroup$ To add some balance, there is also some evidence (see, for example, front.math.ucdavis.edu/1008.3868) that Thompson group is not amenable, although personally I voted several times for amenability. But there are amenable groups whose Følner functions grow faster than any iterated exponent. See Erschler, Anna On isoperimetric profiles of finitely generated groups. Geom. Dedicata 100 (2003), 157--171. $\endgroup$
    – user6976
    Sep 21 '10 at 10:27

The statement that the periodicity of Laver tables tends to infinity is not provable in PRA (hence also EFA), although it is provable under the assumption of a rank-into-rank embedding.

  • $\begingroup$ Nice example. It's hard to believe that this really requires a hypothesis as monstrous as rank into rank; does anyone know if this can be proved in (say) Peano arithmetic? $\endgroup$ Aug 24 '10 at 19:37
  • 5
    $\begingroup$ @Richard: This is open, see, for example spot.colorado.edu/~szendrei/BLAST2010/miller_new.pdf $\endgroup$
    – Kiochi
    Aug 24 '10 at 19:51
  • $\begingroup$ Dehorney seems to have used these ideas to prove new theorems about orders on braid groups, which is undeniably "ordinary mathematics". Does anyone happen to know if these braid group theorems lie beyond EFA? $\endgroup$ Aug 24 '10 at 19:59
  • 1
    $\begingroup$ Richard -- some of these theorems (in particular, the algorithm for distinguishing braids) do formally not require large cardinals at all. Rather they were inspired by research on large cardinals. See Dehornoy, From large cardinals to braids via distributive algebra, Journal of knot theory and ramifications, 4, 1, 33-79 and also talk slides math.unicaen.fr/~dehornoy/Talks/DyfShort.pdf (posted by John Stillwell as a comment to my answer here mathoverflow.net/questions/14574/…). $\endgroup$
    – algori
    Aug 24 '10 at 21:02

Since Ackermann's function is not available in EFA, Tarjan's upper bound – the inverse Ackermann function – for the run-time of the union-find data structure is not provable in EFA. This probably doesn't matter much, since a weaker upper bound like $\mathcal{O}(\log (\log (\log n)))$ is not really worse from a practical point of view.

Another example: is the unsolvability of the Halting Problem provable in EFA? While this is an example from logic, I would argue that this has very practical and thus "ordinary" implications, like the impossibility of automatically checking whether the source code of an arbitrary computer program adheres to the specification. (Well, you can restrict the programming language to make this possible, but then you lose the ability to write interpreters for this programming language.)

  • 1
    $\begingroup$ But it seems to me the inverse Ackermann function (i.e. $\log^*$) is available in EFA. Anyway, this kind of things depends heavily on how one formalizes the statement so it seems to me that non-existence of a function can only mean that a specific formalization of the theorem is not provable. $\endgroup$
    – Kaveh
    Nov 25 '10 at 17:14
  • 3
    $\begingroup$ Except that $\log *$ is not the inverse Ackermann function. :-) As for the formalization, you might have a point if it were only the upper bound; there could be better bounds that can be formalized but which haven't been proven yet. However, if I am informed correctly, the bound is actually sharp, so you'd have an algorithm whose asymptotic complexity cannot be formalized in EFA. $\endgroup$ Nov 25 '10 at 21:38

This is a great question! And this is not an answer. The paper by Shelah and Soifer, Axiom of choice and chromatic number of the plane shows that the chromatic number in the plane "is not countable (if it exists) in a consistent system of axioms with limited choice." Is the chromatic number of plane part of "ordinary mathematics"? Unclear...

  • $\begingroup$ Well, given that I've seen a couple of high school math contest questions asking contestants to provide lower bounds for the chromatic number of the plane (if I recall correctly) it's certainly close to the boundary. $\endgroup$
    – dvitek
    Aug 25 '10 at 15:50
  • 1
    $\begingroup$ "Is chromatic number of the plane ordinary mathematics?"... How is it not? The question was not created by motivations from logic, if by 'ordinary' you mean 'not motivated by concerns outside the domain of interest (usually logic)'. $\endgroup$
    – Mitch
    Aug 25 '10 at 16:19
  • $\begingroup$ To me it is part of "ordinary mathematics," but I wasn't sure if it satisfied Richard Borcherds' notion. The reason I thought this example perhaps does not answer his question is that he wanted occurences of "functions larger than a finite tower of exponentials." $\endgroup$ Aug 25 '10 at 20:46
  • 3
    $\begingroup$ Shelah and Soifer prove their main result not about the chromatic number of the plane, which is known to be 4, 5, 6, or 7, but about the chromatic number of a different but related graph. They have some evidence that the chromatic number of the plane itself depends on the model of set theory, which is rather surprising (at least to me). I cant make up my mind whether this counts as ordinary mathematics. $\endgroup$ Aug 27 '10 at 0:17
  • $\begingroup$ @Joseph, I looked at one of the papers by Shelah and Soifer, and it proves the chromatic number of an infinite unit-distance graph is not countable. Is this the same thing as the chromatic number of the plane not being countable? Maybe this graph can't be proven to be unit distance in the plane without a sufficiently rich set of axioms. $\endgroup$
    – Peter Shor
    Nov 23 '10 at 15:46

Here is another example: The 1-related Baumslag group $\langle a,b | a^{a^b}=a^2\rangle$ has Dehn function $d(n)$ which is exactly (up to the natural equivalence) $2^{2^{2...}}$ $\log n$ times, see Platonov, A. N. An isoparametric function of the Baumslag-Gersten group. (Russian. Russian summary) Vestnik Moskov. Univ. Ser. I Mat. Mekh. 2004, , no. 3, 12--17, 70; translation in Moscow Univ. Math. Bull. 59 (2004), no. 3, 12--17 (2005). Recall that the Dehn function is the smallest function that bounds the number of defining relations needed to deduce a relation $w=1$ with $|w|\le n$ which is true in the group (or the minimal number of factors in the product of conjugates of the defining relations that are equal to $w$ in the group). The notation $a^b$ means $b^{-1}ab$.


An innocent looking problem in which the Ackermann function unexpectedly comes up is the length of Davenport-Schinzel sequences. I won't bother to say in detail what they are, because Wikipedia does a good job.


Actually, what one gets is a bound of the form na(n), where a is the inverse of the Ackermann function, but then one can ask how big n needs to be for the bound to be worse than Cn.


I think we're heading towards an era where "ordinary" mathematics includes logic, at least the parts of it that can be described as applied mathematics (used in practical problems of the real world). For example, the ML programming language is based on polymorphic lambda calculus. I'm no expert but I have the impression that the proof that polymorphic lambda calculus is strongly normalizing is equivalent to second order arithmetic. There are fancier languages based in even more powerful (?) theories, like Coq implements Martin-Lof type theory more or less directly. I'm just a programmer trying to learn these languages but people disigning them and writing compilers for them (e.g. implementing type inference) seem to me to often be up to their elbows in proof theory. I saw a thesis by someone about ordinal analysis of programs (after all, by the Curry-Howard correspondence, programs are proofs..). I wondered if software engineers (at least those in high-assurance programming) will someday use proof-theoretic ordinals in their daily work just like electrical engineers now use complex numbers.

In complexity theory, there are some proofs that P vs NP is independent of some sizeable fragments of PA, but maybe those fragments are weaker than EFA.


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.