Formalizing Euclid's proof of the infinitude of primes

Euclid's proof of the infinitude of primes requires me to take an arbitrary finite set of primes and multiply them together. If I want to formalize this proof in Peano Arithmetic, I need to know that any finite set of numbers has a product. Carl Mummert's comment on Russell O'Connor's answer to this question points out that this is trickier than it sounds, since "finite" means "indexed by a natural number", which is not the same thing as "indexed by a standard natural number". So one needs an inductive definition of the product to prove it exists.

The obvious inductive definition is:

$$\prod_{k=1}^{S(n)}a_k = a_{S(n)}\prod_{k=1}^n a_k$$

where I write $S$ for "successor". Is this enough to fill the "gap" in Euclid's proof, or am I missing something? (I ask because, in the discussion linked above, there seems to be a hint that it's not quite this simple.)

• I think what you need is totality of exponentiation (to code tuples). – user5810 Sep 20 '11 at 21:10
• You need to be precise about what symbols you have in your version of PA. If you are using first order sentences concerning $+$, $\times$, $0$, $1$, $=$ etcetera, then it is quite a challenge to even represent the concept of a finite set of integers. I blogged about this at sbseminar.wordpress.com/2009/12/07/… If your notation lets you talk about finite sets, then life is easier and you can roughly do what you say. – David E Speyer Sep 20 '11 at 21:54
• IIRC the proof is formalized in even weaker theories e.g. $\mathsf{I\Delta_0}+Exp$. Coding finite sets is not difficult if you use a goof coding, e.g. write number in binary, add symbol 2 between them, read the resulting string in base 4. – Kaveh Sep 20 '11 at 22:11
• @Kaveh: I'm wondering -- why do you call it a "goof" coding? – The_Sympathizer Sep 21 '11 at 1:30
• Mike: D and F are adjacent on US (and Canadian, since Kaveh is in Toronto) keyboards. – François G. Dorais Sep 21 '11 at 1:36

Two points. The first is that one theory that is sufficient for the task is PRA - primitive recursive arithmetic - or any theory that interprets it. The definition in the question works fine in that setting. There are weaker theories where you can code things, as well. The key point is that in PRA there is a definable unary function Set($n)$ which says $n$ codes a "finite" set, and a definable binary relation Element($n$,$k)$ which says that $n$ is an element of the set coded by $k$. These have the property that for every $l$ in any model of PRA there is a $k$ which codes the "finite" set of numbers $n < l$ that are prime.

This sort of coding requires quite a bit of work to set up, but it is viewed as completely routine unless you try to really plumb the depths of the weakest possible theory. PRA is already an extremely weak theory.

Second, there is some benefit to rephrasing things before formalizing them. Rather than proving "no finite set of primes includes all the primes", it is more natural in arithmetic to prove "the set of primes is not bounded". These are equivalent in the real world, but the latter entirely avoids the issue of coding finite sets. We still have to prove, by induction, that for every $k$ there is an $n$ that is a multiple of every prime less than $k$ (using the method from the question to define $k!$); that if $a | n$ then $a \not | n+1$; and that every number has a prime factor. None of these requires coding finite sets.

• I agree about benefiting from avoiding sets, because coding is an unpleasant distraction. On the other hand, it may be worth noting that the proof outlined in Carl's third paragraph uses $\Sigma^0_1$ induction (to get the existence of something like factorials), and that this much induction would also suffice to code finite sets if one wanted to. So what one gains by avoiding sets is not a reduction in the needed axioms but rather a clearer view of the essentials of the proof. – Andreas Blass Sep 21 '11 at 13:01

The definition of iterated product is the easy part of the proof, the bottleneck is elsewhere. Even quite weak theories of bounded arithmetic, such as PV (this is an open theory with function symbols for polynomial-time functions), can prove that the product of a sequence of natural numbers exists (and is divisible by each element of the sequence), by formalizing the usual inductive definition in a straightforward way.

The next thing you need is to show that every number greater than one is divisible by a prime. PV is not known (and not expected) to prove this, but it is provable in the slightly stronger theory $S^1_2$. Thus, $S^1_2$ can formalize Euclid’s proof as the statement “there is no sequence containing all primes”.

As Carl noted, this is not a very natural rendering of the statement “there are infinitely many primes” (especially in weak theories, where sequences can only have logarithmic length). The statement one really wants to prove is “the set of primes is unbounded”. In order to infer this from Euclid’s proof, you need the principle that any bounded set can be put in a sequence, and this is equivalent to the axiom that exponentiation is total. Thus, formalization of Euclid’s proof in this sense can be done in $I\Delta_0+\mathrm{EXP}$ (and a fortiori in very strong theories like PRA).

It is possible to prove that there exist unboundedly many primes in theories weaker than $I\Delta_0+\mathrm{EXP}$, but this requires a much more elaborate proof than Euclid’s. Paris, Wilkie and Woods have shown the unboundedness of primes in the theory $I\Delta_0+\Omega_1$ (where $\Omega_1$ roughly says that $x^{\log x}$ exists for every $x$), and more precisely, in its subtheory $I\Delta_0+\mathrm{WPHP}(\Delta_0)$ (the latter is the weak pigeonhole principle: there is no $\Delta_0$-definable injection from $[0,2x]$ to $[0,x]$). It can be seen that their proof actually goes through in the theory $S^1_2+\mathrm{rWPHP}(\Theta)$ (itself included in $T^3_2$ and $S^4_2$), where $\Theta$ is the set of provably total $\Sigma^b_2$-definable functions of $S^1_2$ (which coincides with functions from the complexity class $\mathrm{FP}^{\mathrm{NP}[\mathrm{wit},\log n]}$), and $\mathrm{rWPHP}(\Theta)$ is a version of WPHP where the injection is supplied with an explicit retraction, both coming from $\Theta$. To the best of my knowledge, this is the weakest theory known to prove the unboundedness of primes.

• Do you know if Sylvester's theorem (described at the end of that article) is also provable in $\hspace{1.09 in}$ that "weakest theory known ... unboundedness of primes"? $\;$ – user5810 Sep 22 '13 at 10:20
• A reasonable guess is that Sylvester’s theorem is provable in this or a slightly stronger theory, but I haven’t read Alan Woods’s PhD thesis to verify this. I may look at it later. – Emil Jeřábek Sep 28 '13 at 15:15
• I have convinced myself that Woods’s proof of Sylvester’s theorem can be formalized in $S^1_2+\mathrm{rWPHP}(\Theta)$, with the caveat that the weak pigeonhole principle needs to be stated as going from something like $x+x/\log x$ to $x$ rather than from $2x$ to $x$. (These kinds of variants are often equivalent, but in this case I don’t think that the needed amplification can be carried out in $S^1_2$, one would need to raise the base theory to $T^1_2$.) – Emil Jeřábek Sep 30 '13 at 15:45
• Also, what I wrote about “the weakest theory known” is not literally true. $I\Delta_0+\mathrm{WPHP}(\Delta_0)$ is (likely) incomparable with $S^1_2+\mathrm{rWPHP}(\Theta)$: the latter includes the totality of the $\omega_1$ function (not provable in the former theory), while apart from that, it has induction and WPHP for a much smaller class of formulas. – Emil Jeřábek Sep 30 '13 at 15:51