(Request for) simple constructive proof of existence of nonstandard model of PA I know of two straightforward nonconstructive proofs of the existence of nonstandard models of arithmetic.

*

*By the existence of the standard model of PA, PA is satisfiable and has an infinite model. By Upward Löwenheim–Skolem, there therefore exists a model of PA of every infinite cardinality. Pick any infinite cardinal not equal to $\omega$ and its associated model is a nonstandard model of PA.



*Let $k$ be a new constant symbol. Add to PA infinitely many sentences $\{S^i(0) \neq k : i \in \mathbb{N}\}$ and call the new theory PA+. Every finite subset of the theory PA+ is satisfiable, we can simply pick $k$ to be one larger than the largest $i$. Therefore PA+ is finitely satisfiable and, by compactness, satisfiable.

The compactness proof seems to be very common. For example, it is used here and here. (Tangentially, the fact that Wikipedia does not include a Löwenheim–Skolem argument makes me wonder whether "non-standard models of arithmetic" are generally assumed to be countable or if there's something else I'm missing something. The argument seems very simple.)
I'm wondering if there's a simple constructive proof of the existence of nonstandard models of arithmetic.
I'm especially curious if there's a way of extending the compactness argument (2) to pick a particular model satisfying the new axioms regarding $k$.
 A: Ultrapowers are certainly important and worth understanding, but in my opinion - especially if we're looking at nonstandard models of arithmetic in particular - they are not optimally constructive.
Let me give a minor tweak to the standard term model idea. Given a (consistent and complete) theory $T$ in a language $\Sigma$, let $$\mathsf{Def}_T=\{\varphi\in \mathsf{Form}_1: T\vdash\exists !x\varphi(x)\},$$ where $\mathsf{Form}_1$ is the set of single-variable formulas in the language of $T$. Note that $\mathsf{Def}_T$ comes equipped with a natural equivalence relation, $\approx_T$, given by $$\varphi\approx_T\psi\quad\iff\quad T\vdash\forall x(\varphi(x)\leftrightarrow\psi(x)).$$ The set $\mathsf{Def}_T/\approx_T$ is a natural candidate for the underlying set of a model of $T$; intuitively, its elements are the "specific objects" which $T$ can describe in a concrete way. In particular, if $T$ has the following (weak) witness property $$\forall\varphi\in\mathsf{Form}_1: \quad [T\vdash\exists x\varphi(x)]\implies [\exists \eta_\varphi\in\mathsf{Def}_T(T\vdash\forall x(\eta_\varphi(x)\rightarrow\varphi(x))],$$ the obvious way of turning $\mathsf{Def}_T/\approx_T$ into a $\Sigma$-structure $\mathfrak{D}_T$ actually does result in a model of $T$. Moreover, note that this whole process is completely computable ... relative to $T$ itself. In particular, we have:

Let $\mathsf{PA}^+=\mathsf{PA}\cup\{c>\underline{n}:n\in\mathbb{N}\}$. Given a complete consistent extension $T$ of $\mathsf{PA}^+$, we can build a model of $T$ together with its elementary diagram.

And the complexity of true arithmetic notwithstanding, completions of $\mathsf{PA}^+$ can be found quite low-down in the computability-theoretic universe: by the low basis theorem, such theories exist which are much simpler than the halting problem.
Separately, note that - since $\mathsf{PA}^+$ (for the same reason as $\mathsf{PA}$) "has definable Skolem functions" - if $T$ is any complete consistent extension of $\mathsf{PA}^+$ then $\mathfrak{D}_T$ is the prime model of $T$, so the $T\leadsto\mathfrak{D}_T$ construction is even quite natural from a "global" point of view.
A: The ultrapower construction is a general way of getting a new structure elementarily equivalent to a given one.
It is as explicit as one could hope – the non-constructiveness is, in effect, concentrated entirely in the ultrafilter that the construction takes as an input.
Let $X$ be a set.
This is supposed to be the set of elements of the structure we are interested in.
Let $I$ be a set.
An filter on $I$ is a set $\mathfrak{U}$ of subsets of $I$ that satisfies the following conditions:

*

*$I \in \mathfrak{U}$.

*If $I_0 \in \mathfrak{U}$ and $I_1 \in \mathfrak{U}$ then $I_0 \cap I_1 \in \mathfrak{U}$.

*If $I_0 \in \mathfrak{U}$ and $I_0 \subseteq I_1 \subseteq I$, then $I_1 \in \mathfrak{U}$.

For example, the set of cofinite subsets of $I$, i.e. $\{ I' \subseteq I : I \setminus I' \text{ is finite} \}$, is a filter on $I$.
Given $x_0$ and $x_1$ in $X^I$, define $x_0 = x_1 \pmod{\mathfrak{U}}$ to mean that $\{ i \in I : x_0 (i) = x_1 (i) \} \in \mathfrak{U}$.
It is straightforward to verify that this is an equivalence relation on $X^I$.
The filterpower $X^I / \mathfrak{U}$ is defined to be the set $X^I$ modulo this equivalence relation.
It is clear that given a map $f : X \to Y$, the induced map $f^I : X^I \to Y^I$ respects equality modulo $\mathfrak{U}$, so we get an induced map $f^I / \mathfrak{U} : X^I / \mathfrak{U} \to Y^I / \mathfrak{U}$.
So, by considering the projections $X \times Y \to X$ and $X \times Y \to Y$, we obtain a natural map $(X \times Y)^I / \mathfrak{U} \to (X^I / \mathfrak{U}) \times (Y^I / \mathfrak{U})$.
It is straightforward to verify that this is a bijection.
Thus, any binary operation on $X$, i.e. any map $X \times X \to X$, induces a binary operation on $X^I / \mathfrak{U}$ in a natural way.
Similarly for $n$-ary operations in general, for all finite $n$.
It is also clear that if $f : X \to Y$ is injective then $f^I / \mathfrak{U} : X^I / \mathfrak{U} \to Y^I / \mathfrak{U}$ is also injective.
Thus, any $n$-ary relation on $X$ induces an $n$-relation on $X^I / \mathfrak{U}$ in a natural way, for all finite $n$.
More concretely, given $x_0, \ldots, x_{n-1}$ in $X^I$ and some $n$-ary relation $R$ on $X$, the induced $n$-ary relation $R^I / \mathfrak{U}$ on $X^I / \mathfrak{U}$ relates the images of $x_0, \ldots, x_{n-1}$ in $X^I / \mathfrak{U}$ if and only if $\{ i \in I : (x_0 (i), \ldots, x_{n-1} (i)) \in R \} \in \mathfrak{U}$.
Hence, if $X$ carries a $\Sigma$-structure for some finitary signature $\Sigma$, then $X^I / \mathfrak{U}$ has a natural induced $\Sigma$-structure.
Moreover, this makes the diagonal embedding $X \to X^I / \mathfrak{U}$ into a homomorphism of $\Sigma$-structures.
The remarkable fact is this:
Theorem (Łoś).
If $\mathfrak{U}$ is an ultrafilter on $I$, i.e. $\mathfrak{U}$ is a filter on $I$ such that, for every $I' \subseteq I$, either $I' \in \mathfrak{U}$ or $I \setminus I' \in \mathfrak{U}$, then the diagonal embedding $X \to X^I / \mathfrak{U}$ is an elementary equivalence of $\Sigma$-structures.
Since the construction of $X^I / \mathfrak{U}$ as a set does not depend on $\Sigma$, we could just as well take $\Sigma$ to be the signature consisting of all $n$-ary operations on $X$ and $n$-ary relations on $X$.
This means it is possible to equip $X^I / \mathfrak{U}$ with any and all (finitary first order) structure that $X$ has, in a way that makes $X^I / \mathfrak{U}$ satisfy exactly the same (first order) properties as $X$.
In particular we could do so for $X = \mathbb{N}$ and obtain on $X^I / \mathfrak{U}$ not only the structure of a model of Peano arithmetic but also a linear order (with a least element and no greatest element), a rig structure, etc.
But could it be that $X \to X^I / \mathfrak{U}$ is actually an isomorphism?
Well, if $\mathfrak{U}$ is a principal ultrafilter, i.e. there is $i \in I$ such that $\mathfrak{U} = \{ I' \subseteq I : i \in I' \}$, then the diagonal embedding $X \to X^I / \mathfrak{U}$ is a bijection.
However, if $I$ is infinite, we can apply Zorn's lemma to deduce that a non-principal ultrafilter on $I$ exists: it is easy to check that any maximal proper filter on $I$ is an ultrafilter, and if $I$ is infinite then the cofinite filter is proper, hence contained in an ultrafilter; but an ultrafilter containing the cofinite filter cannot be principal.
If $\mathfrak{U}$ is an ultrafilter on $I$ containing the cofinite filter and $X$ has at least two distinct elements, then it is straightforward to see that $X \to X^I / \mathfrak{U}$ is not surjective.
We may think of those elements of $X^I / \mathfrak{U}$ that are in the image of the diagonal embedding as standard elements and those that are not are non-standard elements.
For example, let $X = I = \mathbb{N}$.
Then, $x (i) = i$ defines a non-standard element $x$ of $X^I / \mathfrak{U}$.
Abusing notation somewhat, we may identify elements of $X$ with the corresponding standard elements of $X^I / \mathfrak{U}$.
Clearly, for any $n \in \mathbb{N}$, $\{ i \in I : n < x (i) \} \in \mathfrak{U}$, so we have $n < x$ in $X^I / \mathfrak{U}$ for all $n \in \mathbb{N}$; in words, $x$ is greater than any standard element!
More generally, for a fixed finite $n$, given any set $\Phi$ of $n$-ary predicates on $X$ such that every finite subset is simultaneously satisfiable, by choosing $I$ and $\mathfrak{U}$ appropriately, we may find an explicit $n$-tuple of elements of $X^I / \mathfrak{U}$ satisfying all of $\Phi$ simultaneously.
The trick is to choose $I = X^n$.
Consider the set of all $I' \subseteq I$ such that there exists a finite subset $\Phi' \subseteq \Phi$ such that $I'$ contains the set of all $n$-tuples of elements of $X$ that simultaneously satisfy $\Phi'$.
This is a proper filter on $I$, so is contained in some ultrafilter $\mathfrak{U}$.
Let $x_j : I \to X$ be the $j$-th projection $X^n \to X$.
Then $(x_0, \ldots, x_{n-1})$, considered as an $n$-tuple of elements of $X^I / \mathfrak{U}$, simultaneously satisfies all of $\Phi$: indeed, for each $\phi \in \Phi$, the set of all $i \in I$ that satisfy $\phi (x_0 (i), \ldots, x_{n-1} (i))$ is in $\mathfrak{U}$, so we have $\phi (x_0, \ldots, x_{n-1})$ in $X^I / \mathfrak{U}$ as required.
