By high school mathematics I mean Elementary Function Arithmetic (EFA), where one is allowed +, ×, x^{y}, 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.

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$7more comments