Simplest PA theorem whose proof requires encoding of sequences even though the statement itself doesn't

What is the simplest number-theoretic theorem whose proof requires exponentiation or finite sequences/sets (so any proof in Peano Arithmetic would need to use encodings of such things using e.g. Gödel's beta function) but the statement of the theorem itself does not require them?

By "simple" I mean that the proof is simple, not just that the statement of the theorem is simple. Therefore, e.g. the Green-Tao theorem does not count.

The example I have in mind is the following: "Let $p$ be an odd prime. Then $-1$ is a quadratic residue modulo $p$ if and only if $p\equiv 1 \pmod 4$." The proof I know uses Euler's criterion, which involves exponentiation (and the proof I know of Euler's criterion uses, among other things, Wilson's theorem which involves factorials).

• There are other ways how to prove that $-1$ is a quadratic residue modulo $p=1\pmod4$, however, they all do seem to need sequence coding in one way or another (e.g. by usig exponentiation or similar recursively defined functions, or counting the size or parity of definable bounded sets). – Emil Jeřábek Feb 18 '16 at 10:41
• I confess I don't quite understand the question. How does one go about proving rigorously a statement of the form, "Every proof of Theorem X requires encodings"? Don't we need to define a weak system in which it is impossible to define sequences? What candidate is there for such a system? – Timothy Chow Feb 18 '16 at 20:50
• Actually, Pavel Pudlák has once provided a definition of exponentiation which doesn't involve any coding of sequences, see here. – Wojowu Feb 21 '16 at 9:27
• Wojowu: You can prove, without using any encoding, that if $ab$ is a perfect square, say, with $a$, $b$ relatively prime, then $a$ and $b$ are perfect squares. The main basic ingredient is Euclid's lemma, that if $p$ is a prime that divides $xy$, then $p$ divides either $x$ or $y$. Therefore, if $p$ divides $x^2$ then $p^2$ divides $x^2$. Euclid's lemma follows from Bezout's identity, etc... – Gabriel Nivasch Feb 21 '16 at 11:13
• @GabrielNivasch I see now; you could divide $a$ by $p^2$ and then continue using induction. So that's something I have learned today :) – Wojowu Feb 21 '16 at 14:21

Consider the sentence $$\forall x\, \exists y\ x < y\, \&\, \text{prime}(y)$$ The usual simple proof establishes this with $y<x!$. We do not know if it can be proved in a weak arithmetic like $I\Delta_0$ that only proves the existence of polynomial-sized functions.
In 1988, Paris, Wilkie and Woods showed that the theorem follows in a weak arithmetic from the existence of the function $x^{\log(x)}$. In 2001, Atserias showed that it follows from the existence of the function $x^{\log(x)^{1/k}}$. So all our proofs now require super-polynomial functions, even though the statement does not.
• You don't need sequences to prove unboundedness of primes in PA. You prove by induction on $n$ that "for every $n$ there exists a $b$ that is divisible by every number small-equal to $n$." Then you add $1$ to such a $b$. No need to talk about factorials. – Gabriel Nivasch Feb 21 '16 at 3:47
• I skimmed through a course on elementary number theory, and the simplest example I found is the one I mentioned regarding whether $-1$ is a QR. – Gabriel Nivasch Feb 21 '16 at 4:00
• How does requiring superpolynomial functions have anything to do with coding of sequences? Sequences can be coded in $I\Delta_0$ in a completely straightforward way. In fact, sequences can even be coded in the theory of discretely ordered commutative semirings (aka $PA^-$). – Emil Jeřábek Feb 21 '16 at 14:59