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.)
 A: 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.
A: 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. 
