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.
Best Answer
I don't know whether this is what you had in mind, but in 1980 Alex Wilkie showed that if one uses the axioms
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.