Is all ordinary mathematics contained in high school mathematics?

Question

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.

Answer 1

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.

Answer 2

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.

Answer 3

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?

Answer 4

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

Answer 5

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

Answer 6

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.

Answer 7

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

Answer 8

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.

Answer 9

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