Are the real numbers ever needed to prove a property of the natural numbers?

Suppose no one had invented/discovered the real numbers yet (so e.g., no calculus), would this constrain the possible theorems or knowledge we could have about the natural numbers?


Since we are talking about whether real numbers are necessary, it only makes sense to talk about theorems that do not require real numbers merely to state the theorem, since that is a very trivial sense of "necessary".

The properties that can be stated directly in terms of the natural numbers are called arithmetical in the literature. These are the properties that are obtained by starting with multivariable polynomial equations over the natural numbers and closing under logical operations and universal and existential quantification over the naturals. Although it may seem as if this is a very limited collection of properties, it turns out after much nontrivial work that many statements can be stated arithmetically (for example, the Riemann Hypothesis, Fermat's last theorem, the Prime Number Theorem, and the statement "$\pi$ is irrational" can all be rephrased as arithmetical statements).

Next, it is also necessary to look at provability in fixed formal theories. After all, if we took every true arithmetical statement as an axiom, this system would be able to prove every true arithmetical statement (trivially) without the use of real numbers. But that is not the point, and it makes the question uninteresting. So we need to specify which set of axioms we are considering for the natural numbers, just so that we have some collection of properties that are not provable. The most common axiom system for studying arithmetical statements is first-order Peano arithmetic, PA.

Thus one way of stating the question that is both precise and interesting is:

Are there formal systems that extend PA by allowing us to talk about real numbers, and which prove every (arithmetical) statement provable from PA as well as additional arithmetical statements?

The answer to that is yes. One example of such a system is Zermelo-Frankel set theory, ZF. This is able to prove every arithmetical statement provable in PA, as well as many more.

It is not necessary to go all the way to set theory. For example, there is a system well known in logic called "second order arithmetic" ($Z_2$) which is a natural system for studying just the natural numbers and real numbers. This system, $Z_2$, is strictly between Peano arithmetic and ZF in terms of the arithmetical statements it is able to prove.

P.S. In terms of the statements I listed above, it is known that PA proves the Prime Number Theorem and that $\pi$ is irrational. It is suspected that Fermat's Last Theorem is provable in PA, although this has not been shown rigorously. And nobody knows if the Riemann Hypothesis is provable even in ZF.