Primes in nonstandard models of PA What is known about prime numbers in nonstandard models of PA?
Restricted to true natural numbers the sets are identical, but does there always exist nonstandard primes? Can we explicitly define one in some model?
 A: The question of whether there always exist non-standard primes has been fully answered by Henning Makholm. We make some remarks about defining a non-standard prime in some model. 
We stick with tradition by working with $\mathbb{N}_0$, the non-negative integers with ordinary addition and multiplication.  Let $I$ be the set of non-negative integers, which will be viewed as an index set. Let $D$ be a non-principal ultrafilter on $I$. Then the ultrapower $\mathbb{N}_0^I/D$ is in a natural way a non-standard model of the theory whose axioms are all sentences of the language of PA that are true in $\mathbb{N}_0$. For some information about ultraproducts and ultrapowers, please see this Wikipedia article. 
Extremely briefly, to construct $\mathbb{N}_0^I/D$, we first look at $\mathbb{N}_0^I$, the set of all functions from $I$ to (the underlying set of) $\mathbb{N}_0$, that is, at all sequences $(a_0,a_1,a_2,\dots)$ where the $a_i \in \mathbb{N}_0$. If  $(a_0,a_1,a_2,\dots)$ and $(b_0,b_1,b_2,\dots)$ are two such sequences, then we say that
$$(a_0,a_1,a_2,\dots) \:\:\equiv_D\:\: (b_0,b_1,b_2,\dots)$$
if  $\{i: a_i=b_i\} \in D$. The relation $\equiv_D$ is an equivalence relation. The ultrapower $\mathbb{N}_0^I/D$ has as underlying set the equivalence classes. We can define addition and multiplication on these equivalence classes coordinatewise modulo $D$. If we do, it turns out that  $\mathbb{N}_0^I/D$ is a non-standard model of arithmetic.
Now let $(p_i)=(p_0,p_1,p_2, \dots)$ be the sequence of (ordinary) primes, say in the natural order, though that does not matter. Then the equivalence class modulo $D$ of $(p_i)$ turns out to be a non-standard prime.   
Is this explicit? It looks fairly explicit, but one can certainly argue that it is not. The construction of a non-principal ultrafilter on $I$ requires the Axiom of Choice (well, not full AC, but it certainly cannot be proved in ZF).  So the entire ultrapower construction is non-constructive.  But given the ultrafilter, everything after that is explicit.)
If we like negative numbers, we can perform exactly the same construction with $\mathbb{Z}$, and work with the ultrapower $\mathbb{Z}^I/D$.  
A: Euclid's proof of the infinitude of primes can be adjusted to show that for any natural number $n$ there is a prime larger than $n$, and in this form the proof can be carried out in PA.
In a nonstandard model of PA, the nonstandard elements are all larger than the standard ones, so if there is a nonstandard element, Euclid's proof shows that there must also be a nonstandard prime.
Nonstandard elements (prime or not) cannot be explicitly defined in the language of PA. (If they could, the induction axiom scheme would be able to show that they didn't exist after all).
A: The other answers are somewhat misleading on the role of choice and/or ultrafilters in all this. Skolem constructed models of the natural numbers that properly extend the "usual" ones, in ZF.  Here a number is an equivalence class of definable functions on the "usual" numbers.  If one takes a function that enumerates the "usual" primes, its equivalence class will give an infinite prime, all that in ZF.
