(Request for) simple constructive proof of existence of nonstandard model of PA

alternative-prooflogicnonstandard-modelspeano-axioms

I know of two straightforward nonconstructive proofs of the existence of nonstandard models of arithmetic.

  1. 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.
  1. 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:

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.

Related Question