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 Gödel). 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 Szemerédi'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.

Friedman's grand conjecture concerns 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.

  • 14
    $\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$ Commented Aug 24, 2010 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$ Commented Aug 24, 2010 at 19:06
  • 14
    $\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$ Commented Aug 24, 2010 at 19:51
  • 18
    $\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$ Commented Aug 25, 2010 at 0:25
  • 16
    $\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$ Commented Aug 25, 2010 at 0:41

9 Answers 9


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 Tarski's high school algebra problem.

  • 13
    $\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$ Commented Aug 25, 2010 at 0:24
  • 11
    $\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$ Commented Aug 25, 2010 at 1:54
  • 24
    $\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$ Commented Aug 25, 2010 at 13:13
  • $\begingroup$ I think you should clarify for non-specialists that "true" in the language of logicians means "deducible where I think it is correct to deduce it". $\endgroup$ Commented Jul 2, 2023 at 11:39
  • $\begingroup$ @SergeiAkbarov As far as I can see, "true" has the same meaning here as in number theory or any other branch of ordinary mathematics $\endgroup$ Commented Jul 4, 2023 at 14:02

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]=\operatorname{id}\rangle$.

Amenability of a finitely presented group $G$ with finite generating set $\Gamma$ is equivalent to the finiteness of the Følner function $$ \operatorname{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)\mathbin\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 a (rather) weak fragment primitive recursive arithmetic. See the related discussion in Justin's paper, "Fast growth in the Følner function for Thompson's group $F$", particularly the comments surrounding Question 1.2.

On the recent arguments about amenability or not of $F$, see this nice answer by Mark Sapir to Is Thompson's Group F amenable?

  • 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$ Commented Aug 25, 2010 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$ Commented Aug 25, 2010 at 3:58
  • 5
    $\begingroup$ This claim has been discussed on MathOverflow here. mathoverflow.net/questions/26821/is-thompsons-group-f-amenable $\endgroup$ Commented Aug 25, 2010 at 11:53
  • 1
    $\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
    Commented Sep 21, 2010 at 10:27
  • 1
    $\begingroup$ @LSpice Thanks! $\endgroup$ Commented Jul 2, 2023 at 21:21

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$ Commented Aug 24, 2010 at 19:37
  • 5
    $\begingroup$ @Richard: This is open, see, for example spot.colorado.edu/~szendrei/BLAST2010/miller_new.pdf $\endgroup$
    – Kiochi
    Commented Aug 24, 2010 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$ Commented Aug 24, 2010 at 19:59
  • 2
    $\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
    Commented Aug 24, 2010 at 21:02
  • $\begingroup$ @Kiochi's reference: Miller - An open problem involving finite algebras, braid groups, and cardinals (slides). $\endgroup$
    – LSpice
    Commented Jul 2, 2023 at 20:52

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

  • 3
    $\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
    Commented Nov 25, 2010 at 17:14
  • 7
    $\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$ Commented Nov 25, 2010 at 21:38
  • 2
    $\begingroup$ The inverse Ackermann function is not $\log^*$, but regardless of that, it is avaliable in EFA (as a provably total $\Delta_0$-definable function). So there is no reason to think Tarjan’s upper bound is not formalizable in EFA. Unsolvability of the Halting problem is likewise provable in EFA. $\endgroup$ Commented Jul 2, 2023 at 15:36

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.


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 of 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….

  • 2
    $\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
    Commented Aug 25, 2010 at 16:19
  • 4
    $\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$ Commented Aug 27, 2010 at 0:17
  • 1
    $\begingroup$ Just to update Richard Borcherds' comment from Aug 27 2010, we now know that the chromatic number of the plane is not 4. arxiv.org/abs/1804.02385 and arxiv.org/abs/1805.00157 $\endgroup$
    – David Roberts
    Commented Jan 16, 2021 at 4:03
  • 3
    $\begingroup$ In my opinion, the following question is "ordinary mathematics": What is the largest chromatic number of a finite graph that arises as a unit distance graph in the plane? When people talk about the "chromatic number of the plane," I submit that it is this question they're really interested in. And the answer to this question doesn't have anything to do with the axiom of choice. $\endgroup$ Commented Oct 1, 2022 at 17:37
  • 2
    $\begingroup$ Again, IMO, there's a bit of a bait-and-switch going on here. Using AC, one shows that the above question Q1 is "equivalent" to another question Q2. Then one deletes AC, so that Q1 and Q2 are no longer equivalent, and then points out that the answer to Q2 depends on your set-theoretic axioms. Fine. But this misleads people into thinking that Q1, the "real" question of interest, depends on set-theoretic axioms in a way that it really doesn't. $\endgroup$ Commented Oct 1, 2022 at 17:40

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-Löf 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.

  • The Whitehead problem is a problem in group theory, which Shelah proved independent from ZFC.
  • Gijswijt's sequence (A090822 in OEIS) is defined as follows: $a_1=1$, and for $n>1$, $a_n$ is defined as the largest number $k$ of nonempty blocks $Y$ such that $a_1,\ldots,a_{n-1}$ is of the form $X,\underbrace{Y,\ldots,Y}_k$. E.g. the first six entries of the sequence are $1,1,2,1,1,2$, letting $X$ be empty and $Y$ be $1,1,2$, then $a_6=2$. Gijswijt proved in the introductory 2007 paper "A slow-growing sequence defined by an unusual recurrence" that every positive integer appears in this sequence, however it was conjectured that this sequence is extremely slow-growing. This was verified in (Pol, "The first occurrence of a number in Gijswijt's sequence", 2022, arXiv 2209.04657), in which an exact formula for the position of the first appearance of $n$ appears is given, and this position turns out to be roughly the power tower $2^{2^{3^{4^{5^{\cdots^n}}}}}$! The exact bound is slightly lower, once explicitly defined constants $\epsilon_1$ and $\nu_m$ (for all $m\in\mathbb Z^+$) are given, $n$ first appears at position $\lfloor1-\epsilon_1+\epsilon_1\cdot 2^{\lceil\nu_1\cdot 2^{\lceil\nu_2\cdot 3^{\ldots^{\lceil\nu_{n-1}\cdot(n-1)\rceil}\ldots}\rceil}\rceil}\rfloor$. ($\nu_1$ is approximately $0.6917$ and the listed values on p.42 of $\nu_m$ for $1\leq m\leq 10$ appear to be increasing, I am not sure how to verify if the $\nu_m$ are increasing and would be grateful if there were more information on how to do this.)
  • $\begingroup$ How does the upper bound imply unprovability in EFA? You’d need a matching lower bound for that. $\endgroup$ Commented Jul 2, 2023 at 15:40
  • $\begingroup$ @EmilJeřábek Unfortunately I can only find polynomial lower bounds, such as one in (Hass, Nowik, Unknot Diagrams Requiring a Quadratic Number of Reidemeister Moves to Untangle). Lackenby has an unpublished improvement of the upper bound to polynomial level, referenced in his "Elementary Knot Theory", arXiv 1604.03778. I will change this to some other result with a known lower bound, such as "every positive integer appears in A090822". $\endgroup$
    – C7X
    Commented Jul 3, 2023 at 9:11

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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