Is the axiom of induction constructively verifiable for a non-standard model of arithmetic?

There exist models of the natural numbers which include infinite numbers. Such models are called non-standard models of arithmetic. Just like the standard model $\mathbb{N}$, the non-standard models satisfy the induction axiom for formulas, although in this case only for forumlas expressible in the first-order language of Peano arithmetic.

The proof of this fact is usually given as: there exist models of Peano arithmetic satisfying any finite subset of the axioms Peano + $\exists c.0<c,S0<c,SS0<c,\dotsc$, therefore by the compactness theorem, there exists a model satisfying all of them.) See for example Henning Makholm's analogous answer about Presburger arithmetic at Nonstandard models of Presburger Arithmetic

Can one instead ask for an explicit verification that the induction axiom holds in some simple nonstandard model, instead of appealing to powerful model theoretic theorems?

In answers like this one, we get explicit constructions of these non-standard models. In short, we adjoin to our well-ordered infinite chain $\omega=\{0,1,2,3,\dotsc\}$ another chain, $\dotsc < c-1<c<c+1<\dotsc$ of order type $\omega^*+\omega,$ with $n<c+m, \forall n\in\mathbb{N},m\in\mathbb{Z}$. If we're modeling PA, so that our model has addition and multiplication, we will adjoin a more intricate order type (a densely ordered collection of such chains), as explained at this question, whereas if we just want to model the successor operation and induction, a single chain will suffice.

That this model will satisfy most of the Peano axioms is obvious, but validity of the induction axiom is not. It in fact contradicts naive intuition (presumably based in second-order thinking?) about how mathematical induction works, which is that it bootstraps up a connected well-ordered total chain from the first element through all successors. Second order thinking suggests this should not be valid through the disconnected total chain present in the non-standard model.

The proof that the induction axiom holds for nonstandard models typically relies on the compactness theorem is nonconstructive, since it relies on some weak form of the axiom of choice. Is this obligatory? Is there a possibility of an explicit verification of the induction axiom for this model?

Or is this analogous to the existence of a Hamel basis of the real numbers over the rationals? Is it possible that in some choice-negating set theory like Solovay's model, where all sets of reals are Lebesgue-measurable, that also all models of numbers which satisfy the induction axioms are order-isomorphic to $\omega$?

• It depends on what you mean by 'constructive', of course, but I'd say the answer is No, given Tennenbaum's Theorem: "No countable nonstandard model of PA is recursive. Moreover, neither the addition nor the multiplication of such a model can be recursive." Commented Apr 9, 2016 at 5:50
• the "explicit construction" you link to is not what anyone else would call explicit. It satisfies the induction schema axioms because it is defined to be a model for those axioms. End of story. Commented Apr 9, 2016 at 7:20
• I looked carefully at the answer you linked and I didn't see $\Bbb N \cup \{ \ldots < c-1 < c < c+1 < \ldots \}$ written anywhere. Since you tagged "first-order logic" in your question, I assume you are talking the first-order version of Peano arithmetic, where $+$ and $\times$ are part of the language and their properties given by axioms, and with an induction scheme. Then your structure doesn't even have an interpretation for $+$ and $\times$ so you can't even ask if it's a model of Peano arithmetic. Commented Apr 9, 2016 at 16:52
• Ctrl+F presburger -> "then you can have non-standard models of the following kind: a copy of $\Bbb N$ followed by a discretely-ordered infinite sequence of copies of $\Bbb Z$" I still don't see it. Presburger has $+$ in its language, so just $\Bbb N \cup \Bbb Z$ won't do. Commented Apr 9, 2016 at 17:24
• Also the induction scheme in Presburger arithmetic can't use formulas using $\times$ so it is significantly weaker than first-order Peano's induction scheme. Commented Apr 9, 2016 at 17:27

Well, "constructively verifable" means different things in different contexts. But I am going to take it here as "true without the axiom of choice".

So first of all, the compactness theorem holds for countable languages in $\sf ZF$. So if you add just one constant symbol, compactness still works, and you get a nonstandard model of Peano.

In fact, you can push this a whole lot more. Every well-orderable language has compactness, and I was once told that there's a much more general characterization of when a language will satisfy compactness. It was something akin to having a linear order and another property which I cannot recall.

So even if you added $2^{\aleph_0}$ new constant symbols you should still have compactness. But if you wanted to add $2^{2^{\aleph_0}}$, then in Solovay's model (for example) you won't be able to linearly order this language and therefore you will invariably won't be able to generate a model of $\sf PA$ of that cardinality -- or any larger one.

Right. So what about verifying something constructively? Here's where I think you're missing something. If you have compactness, then you don't need to verify anything. The compactness theorem gives you the wanted conclusion and that's it. If compactness fails, e.g. for the reason your added constants cannot be linearly ordered, then there's nothing to verify because there's no resulting model.

So what does it mean to verify the axioms? I think that you really mean to ask "can we prove such a model exists?", and then the answer -- for adding one constant -- is yes.

• Thanks Asaf. Are you saying the compactness theorem is not a consequence of AC? Or have I misunderstood you? Compactness can be proved without AC, but only for countable languages? Commented Apr 9, 2016 at 15:25
• The latter. Compactness in general is a consequence of choice, yes. But for a countable language you can do without. Just like being well-orderable is a consequence of choice, but for countable sets we can do without choice. Commented Apr 9, 2016 at 15:48

Thoralf Skolem first gave a construction of a nonstandard model of PA (in a way that did not involve the axiom of choice) in 1933. The article is in Swedish so I won't give the reference unless the OP is interested. It was eventually realized that countable theories can have nonstandard interpretations in ZF (again without C). The Solovay theory you mentioned is much more recent and deals with a different phenomenon.