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