formalizing Euclid's theorem How can one formalize Euclid's theorem (i. e. that there are infinitely many prime numbers) in Peano-Arithmetic (firstorder)?
 A: $$\forall x(\exists y > x)[y > 1 \land (\forall w \leq y)(\forall z \leq y)(w \times z = y \to (w = 1 \lor z = 1))]$$
For any number $x$, there is a larger number $y$ which is prime, i.e. greater than one and such that for any pair of factors $w, z$ one of them has to be unity.
Depending on how you have set up the formal language for PA, you'll then need to unpack the restricted quantifiers in your favoured way -- but that's routine.
You don't need, strictly speaking, to restrict the third and fourth quantifiers: but regimenting "$y$ is prime" by
$$y > 1 \land (\forall w \leq y)(\forall z \leq y)(w \times z = y \to (w = 1 \lor z = 1)))$$
makes it clear that primeness is a so-called $\Delta_0$ property, that doesn't require unbounded quantifiers in its definition -- you can settle primeness without any unbounded searches. 
(Fine print: you don't need the $y > 1$ clause in the first formula above, as because of the initial quantifiers you get something equivalent without it: but if you want to "follow the English" more closely then you should include it.)
