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

Question

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

Answer 1

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.

Answer 2

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.