There are various open problems in the subject of logical number theory concerning the possibility of proving this or that well-known standard results over this or that weak theory of arithmetic, usually weakened by restricting the quantifier complexity of the formulas for which one has an induction axiom. It particular, the question of proving the infinitude of the primes in Bounded Arithmetic has received attention.
Does this question make known contact with "workaday number theory" – number theory not informed by concepts from logic and model theory? I understand that proof of the infinitude of the primes in bounded arithmetic could not use any functions that grow exponentially (since the theory doesn't have the power to prove the totality of any such function). So especially I mean to ask:
1) If one had such a proof, would it have consequences about the primes or anything else in the standard model of arithmetic?
2) If one proves that no such proof exists, would that have consequences…
3) Do any purely number theoretic conjectures if settled in the right way, settle this question of its kin?
As a side question, I'd be interested to know the history of this question. I first heard about it from Angus Macintyre and that must have been 25 years ago.
Best Answer
First, let me discuss the precise open question and why it is interesting to logicians. Then I will discuss potential ramifications outside of pure logic.
The main open question is whether the theory IΔ0 can prove the existence of arbitrarily large primes. The theory IΔ0 is the theory over the language of basic arithmetic ($0,1,+,\times,{\leq}$, together with their usual defining axioms) where induction is limited to bounded formulas (Δ0 formulas): formulas wherein all quantifiers are of the bounded form $\forall x(x \leq t \rightarrow \cdots)$ and $\exists x(x \leq t \land \cdots)$ where $t$ is a term of the language possibly involving variables other than $x$. While this theory has been around for quite some time, one of the earliest papers studying this system in detail is Paris & Wilkie On the scheme of induction for bounded arithmetic formulas [Ann. Pure Appl. Logic 35 (1987), no. 3, 261–302, MR904326]. The currently open question regarding the unboundedness of primes occurs there, probably for the first time in print.
Why is this question interesting to logicians? There is a standard fact about the proof theory of ∀∃-formulas which explains the interest. Over IΔ0, this fact takes the following form due to Parikh:
Fact. If IΔ0 proves $\forall x \exists y \phi(x,y)$, where $\phi(x,y)$ is a bounded formula, then IΔ0 proves $\forall x \exists y(y \leq t(x) \land \phi(x,y))$ where $t(x)$ is a term of the language (i.e. a polynomial in $x$).
Thus, IΔ0 cannot prove certain statements such as $\forall x \exists y (2^x = y)$ since $2^x$ grows faster than any polynomial. (Here, $2^x = y$ is an abbreviation for a bounded formula that expresses the properties of the exponential function $2^x$. That formula is rather complex, so I will not explain it here.) In fact, any proof that involves functions of exponential growth at intermediate stages cannot be formalized in IΔ0 because of this. This applies in particular to Euclid's proof which takes a rather large product of primes relative to the input $x$ in order to prove that there is a prime larger than $x$. However, by Bertrand's Postulate, the formula $\forall x \exists y(\mathrm{prime}(y) \land y \geq x)$ does not by itself impose exponential growth. Thus, the fact leaves open the question whether some other proof of the infinitude of primes can be formalized in IΔ0.
What are potential ramifications outside of logic? A natural question to ask about primes is whether there is some kind of efficient formula for producing large primes. (Cf. the Polymath 4 Project.) One can ask further about the growth rate and the computational complexity of such a function. Proof mining techniques show that if IΔ0 proves the infinitude of primes, then there must be a relatively simple function of moderate growth rate to produce large primes. In fact, there must be such a function that produces primes provably in IΔ0.
The existence of such a function should not be a surprise. Indeed, the simple function $p(x)$ that returns the first prime greater than $x$ has very moderate growth rate by Bertrand's Postulate. However, the function produced by a proof of the unboundedness of primes in IΔ0 will have other important characteristics. In particular, it will have rather low computational complexity. The precise relationship between IΔ0 and computational complexity is a little subtle and I don't want to make this statement more precise here. (Some details were added below.) However, there are good reasons to believe that such a proof could yield a polynomial time computable function of moderate growth that produces large primes, which would be a major breakthrough.
What can we say if there is no IΔ0 proof of the existence of arbitrarily large primes? Well, for one thing, a model of IΔ0 where primes are bounded would be a rather interesting object with potential applications to the structure theory of integral domains. However, it turns out that there is not much one can say here about the standard model, but the reason is subtle.
The key problem is the definition of prime number. In the discussion above, I implicitly assumed the standard definition $\mathrm{prime}(x)$ iff $$x > 1 \land (\forall y, z \leq x)(x = yz \rightarrow y = 1 \lor z = 1).$$ However, there are other potential definition of primes. For example, one could define prime numbers as those which pass the AKS primality test. These various equivalent definitions are not necessarily equivalent over IΔ0. Therefore, it is possible that IΔ0 fails to prove the existence of arbitrarily large "traditional primes" but that IΔ0 does prove the existence of arbitrarily large "AKS primes." Since the standard model can't tell the difference between these two notions of primality, this could still give an efficient way to produce large primes as discussed above.
Let me clarify the relationship between proofs in IΔ0 and computational complexity. The polynomial hierarchy is closely tied to slightly different systems of bounded arithmetic, namely the systems $S^n_2$, $T^n_2$ pioneered by Sam Buss. Note that these are somewhat orthogonal to IΔ0. On the one hand, these systems include the smash function $x \# y = 2^{|x||y|}$ which is not provably total in IΔ0. On the other hand, the amount of induction in these systems is even more restricted than in IΔ0.
It is hard to give a precise relationship between time complexity and proofs in IΔ0. The claims I made above are rather based on the (admittedly optimistic) expected success of proof mining on a hypothetical proof the unboundedness of primes in IΔ0.
In any case, there is an inherent weakness to this approach. Complexity theorists do not impose limits on the amount of induction they use in their proofs. For example, complexity theorists will freely use the equivalence of "traditional primes" and "AKS primes" in their arguments. Therefore, the existence of a simple way to generate large primes is not at all equivalent to the existence of a proof of the existence of arbitrarily large primes in IΔ0 or other systems of bounded arithmetic.