# (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.

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$$.

• Can you clarify what you mean by constructive here? PA is a classical theory: arguably, even the the existence of a standard model is non-constructive (a constructive metatheory will never prove that $\mathbb{N}$ satisfies all theorems of PA). Jan 14, 2022 at 3:19
• Of course, by Tennenbaum's theorem, the elementary operations in non-standard models of PA are never computable, which further limits how "constructive" the existence of such models can be. Jan 14, 2022 at 3:27
• @Gregory Wouldn’t the term model produced in the proof of the compactness theorem qualify in that loose sense? (But per Tenenbaum’s theorem, it’s not going to be something that you can “inspect” in some concrete way.) Jan 14, 2022 at 4:47
• @GregoryNisbet How about ultrapower constructions? As long as you can "get your hand on" an non-principal ultrafilter you can get a non-standard model whose structure can be described fairly straightforwardly. Jan 14, 2022 at 4:53
• "For building the term model (which I don't completely understand), how big of a problem is it that $k$ has a predecessor (that's unrepresentable (?))?" In what sense is the predecessor of $k$ unrepresentable? In fact, for any nonstandard $\mathcal{M}\models\mathsf{PA}$, the set of *(parameter-freely-)*definable elements of $\mathcal{M}$ forms a substructure of $\mathcal{M}$ which is again a nonstandard model of $\mathsf{PA}$. So in a precise sense building a nonstandrad model of $\mathsf{PA}$ is exactly as hard as building a completion of $\mathsf{PA}$ + $\{c>\underline{n}: n\in\mathbb{N}\}$. Jan 14, 2022 at 5:19

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.

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.

• Two quick comments. (1) Even though the natural map $X\rightarrow X^I/\mathfrak{U}$ isn't surjective in a nontrivial situation, we may still have $X\cong X^I/\mathfrak{U}$ via a different map. E.g. if $X$ is a pure set of cardinality $2^{\aleph_0}$ and $I=\mathbb{N}$, this is guaranteed to happen. (2) More substantively, I don't really think that ultraproducts are "as explicit as one could hope" - an ultrafilter is an extremely complicated object, and is overkill for producing (say) a nonstandard model of $\mathsf{PA}$, which can be done computably from the halting problem (or even much less). Jan 14, 2022 at 17:09
• Sure. I'm not referring to that kind of complexity, though. The filterpower construction doesn't involve any formal language or formal provability or even inductive/recursive constructions, so I imagine it is much easier for non-logicians to understand. Jan 14, 2022 at 22:50