First-order proof that there is no largest prime Is there a first-order proof on $(\mathbb{N},+,*,\le)$ that there is no upper bound on primes. ie that $$\neg\exists{q}{\forall{p}{(\forall{m,n}\space m*n=p\rightarrow m=1\vee n=1)\rightarrow p\le q}}$$
If not, can someone provide an example of an elementary extension of $(\mathbb{N},+,*,\le)$ in which there is a largest prime.
 A: First order PA proves there are unboundedly many primes (which I take it answers the intended question). Essentially, you can replicate in PA the familiar argument that  runs "Take any $n$, then any prime factor of $n! + 1$ is larger than $n$, etc.". To do this, we can show how to define the factorial in  PA (using the $\beta$-function trick, assuming the factorial isn't built in), prove PA knows that the function has the requisite properties, prove PA knows basic facts about divisibility, etc. etc.
For details, see e.g. Kaye's wonderful Models of Peano Arithmetic, Section 5.3.
A: Because the recursive functions are representable, the usual proofs can all be carried out in first-order Peano arithmetic.  The various induction proofs one needs to establish the basic results are all instances of the PA induction scheme.
Added: We do not need the representability machinery to formalize a version of the standard "Euclid" proof. For we do not really need the factorial function. All we need is the fact that for all $x\ge 0$, there exists a $y\ge 1$ such that for all $t$ with $1\le t\le x$, we have $t$  divides $y$. 
The standard proofs of the usual divisibility results, most importantly that any natural number greater than $1$ is divisible by some prime, can be almost mechanically translated to proofs in PA.
A: Here is a semi-formal proof of this statement in PA. By semi-formal, I mean that I will use terms like "is prime" or "dividing" which are not part of the base language, but which are easily expressed in it, and I will assume you have already built up a library of basic number theoretic facts.
Lemma 1: For all $n >1$, there is a prime dividing $n$.
Proof: By induction on $n$. Base case $n=2$ is trivial. Assume the statement for $n<m$. If $m$ is prime, then it is also true for $n=m$. If $k$ is a nontrivial divisor of $m$ then, by induction, $k$ has a prime divisor so $n$ does as well. $\square$
Lemma 2: For all $n \geq 1$, there exists $N \geq 1$ such that, for all $k$ with $1 \leq k \leq n$, we have $k|N$.
Proof: By induction on $n$. Base case $n=1$ is trivial. If $M$ is divisible by all $k$ with $1 \leq k < m$, then $Mm$ is divisible by all $k$ with $1 \leq k \leq m$. $\square$
Theorem: For all $n$, there is a prime greater than $n$. 
Proof: By Lemma 2, there is an $N$ such that $k|N$ for $1 \leq k \leq n$. By Lemma 1, there is a prime $p$ which divides $N+1$. If $p \leq n$, then $p|N$ and $p|N+1$, a contradiction. So $p>n$, as desired. $\square$.

It is interesting to note that Lemma 2 asserts a relation of exponential growth. (That is to say, it is a theorem of the form $\forall n \exists N : \cdots$ where the smallest $N$ satisfying the $\cdots$ is exponential in $n$.) It is known that certain very weak fragments of PA can't prove the existence of a relation of exponential growth; it would be interesting to know whether they can prove infinitude of primes.
