3
$\begingroup$

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

$\endgroup$
15
  • 1
    $\begingroup$ 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). $\endgroup$ Feb 18, 2016 at 10:41
  • 2
    $\begingroup$ 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? $\endgroup$ Feb 18, 2016 at 20:50
  • 1
    $\begingroup$ It's a "soft" question. I agree it's not formally well defined. $\endgroup$ Feb 19, 2016 at 2:12
  • 1
    $\begingroup$ Actually, Pavel Pudlák has once provided a definition of exponentiation which doesn't involve any coding of sequences, see here. $\endgroup$
    – Wojowu
    Feb 21, 2016 at 9:27
  • 2
    $\begingroup$ 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... $\endgroup$ Feb 21, 2016 at 11:13

1 Answer 1

4
$\begingroup$

Maybe the closest example in the literature is the infinitude, or more precisely unboundedness, of the primes.

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.

$\endgroup$
5
  • 4
    $\begingroup$ 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. $\endgroup$ Feb 21, 2016 at 3:47
  • 1
    $\begingroup$ 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. $\endgroup$ Feb 21, 2016 at 4:00
  • $\begingroup$ @GabrielNivasch, I agree that the proof does not make explicit use of sequences or factorials. The results I quoted are one way of answering Timothy Chow's worries above, and as I said, they may be the closest thing that has been studied in the literature. $\endgroup$
    – user44143
    Feb 21, 2016 at 13:23
  • $\begingroup$ 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^-$). $\endgroup$ Feb 21, 2016 at 14:59
  • $\begingroup$ @EmilJeřábek, the question was about "exponentiation or finite sequences". $\endgroup$
    – user44143
    Feb 21, 2016 at 15:02

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.