Is all ordinary mathematics contained in high school mathematics? 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.
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.
 A: 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$.  
A: 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...
A: 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.
http://en.wikipedia.org/wiki/Davenport%E2%80%93Schinzel_sequence
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.
A: I don't know whether this is what you had in mind, but in 1980 Alex Wilkie showed that if one uses the axioms


*

*$x + y = y + x$

*$(x + y) + z = x + (y + z)$

*$x \cdot 1 = x$

*$x \cdot y = y \cdot x$

*$(x \cdot y) \cdot z = x \cdot (y \cdot z)$

*$x \cdot (y + z) = x \cdot y + x \cdot z$

*$1^x = 1$

*$x^1 = x$

*$x^{y + z} = x^y \cdot x^z$

*$(x \cdot y)^z = x^z \cdot y^z$

*$(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.
A: 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.
A: 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.
A: 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 ﬁnite 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.
A: In 2011, the paper "An Upper Bound on Reidemeister Moves" gave an upper bound for knot manipulation: given two equivalent knots with $<n$ crossings, an upper bound on the number of applications of Reidemeister moves needed to reach ambient isotopy between the knots is $a(2^{1,000,000\times n})$, if we let $a(0)=n$ and $a(i+1)=2^{a(i)}$.
A: 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.)
