Explicit countable elementary extension of $\mathbb{N}$ I would like to see an explicit example of a non-trivial elementary extension of the structure $(\mathbb{N}, +, \cdot, 0, 1)$ where $\mathbb{N}$ includes zero. Most of all I am interested in countable ones.
 A: It is worth pointing out is that nonstandard models of arithmetic are constructible in the logical theory WKL$_0$. Weak König's lemma is sometimes considered to be a form of the axiom of choice; however, it can be proven in classical Zermelo–Fraenkel set theory without the axiom of choice. In the sense of being constructible in ZF, such models can be called explicit. Such an explicit model was constructed by Skolem as early as 1933 using sequences of ordinary integers (i.e., sequences drawn from the so-called intended model).
A closely related discussion is taking place here.
A: Unfortunately, Tennenbaum's theorem (https://en.wikipedia.org/wiki/Tennenbaum%27s_theorem) shows that any such extension is non-computable. So there isn't really an explicit example. 

That said, if you are happy with ultrafilters, then fixing a nonprincipal ultrafilter $\mathcal{U}$ we can take the ultrapower of $\mathbb{N}$ along $\mathcal{U}$. As long as $\mathcal{U}$ is not countably closed (it's enough to assume for instance that $\mathcal{U}$ is an ultrafilter on $\mathbb{N}$), the result will be a nonstandard elementary extension of $\mathbb{N}$. Unfortunately, it will be uncountable - at least size continuum.
Note that the Henkinization proof of compactness is constructive: it actually builds you a model (countable, even!) of arithmetic which is not isomorphic to the standard model. This is mathematically much tamer in a variety of senses than the ultrapower construction.
