Reverse Mathematics of Euclid's theorem

Euclid's theorem that there are infinitely many prime numbers has multiple proofs, ranging from Euclid's original theorem that constructs a new prime from a finite list of such, to Euler's proof that requires the theory of infinite products and sums. The latter is clearly ingenious, but overkill, whereas the former is elegant, simple, and often shown as an example of a proof to people with little mathematical background (eg students, readers of popular mathematics books).

I'm curious to know what fragment of arithmetic is needed to perform Euclid's proof, or otherwise, if there is an even lower bound on the logical strength of the theorem.

• You can prove Euclid’s result in bounded arithmetic ($I\Delta_0$) plus the assumption that $x^{\log x}$ exists, or in bounded arithmetic plus a pigeonhole principle that there are no definable injections from $n+1$ to $n$. See Paris, Wilkie and Woods (JSL 1988), Provability of the Pigeonhole Principle and the Existence of Infinitely Many Primes. This is already quite weak, and has been further weakened more recently, but it’s an open question whether bounded arithmetic on its own would suffice. – Matt F. Dec 28 '18 at 23:34
• Nothing better is known that the argument from the Paris–Wilkie–Woods paper, which can be formalized in the fragment $S^1_2+\mathit{rWPHP}(\mathrm{FP}^{\mathrm{NP}[O(\log n)]})$ (included in $T^3_2$) of bounded arithmetic with the $x^{\log x}$ function ($I\Delta_0+\Omega_1$) if one pays attention to the complexity of the functions used. The Woods and Cornaros paper is not an improvement, but a tangent: it concerns $I\Delta_0$ augmented with certain prime-counting functions, which are not known (and unlikely) to be definable in $I\Delta_0+\Omega_1$, only in $I\Delta_0+\mathit{EXP}$. – Emil Jeřábek Dec 29 '18 at 8:23
• @JoelDavidHamkins Absolutely. There are models of IOpen where primes are bounded. – Emil Jeřábek Dec 29 '18 at 8:26
• For the record, Euclid showed that for every finite set $S$ of primes, the prime factors of $1 + \prod S$ are not in $S$. Euclid did NOT start by assuming the finite set $S$ contains all primes. The error or thinking that that's what Euclid did may have originated with Dirichlet's posthumous book on number theory, where that's very close to the beginning of the book. – Michael Hardy Dec 30 '18 at 19:13
• A tangential comment, well-known but perhaps not as well-known as it should be: The hypothesis that $x^{\log x}$ exists is more natural than it looks. Call a natural number $n$ small if $2^n$ exists. Then the hypothesis says (in reasonable contexts) that any product of two small numbers is small. – Andreas Blass Dec 30 '18 at 22:32