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$.
Best Answer
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:
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.