Editing Peano axioms (section)

=== Nonstandard models ===

{{Main|Non-standard model of arithmetic}}
Although the usual [[natural number]]s satisfy the axioms of [[#Equivalent axiomatizations|PA]], there are other models as well (called "[[non-standard model]]s"); the [[compactness theorem]] implies that the existence of nonstandard elements cannot be excluded in first-order logic.{{sfn|Hermes|1973|loc=VI.4.3|ps=, presenting a theorem of [[Thoralf Skolem]]}} The upward [[Löwenheim–Skolem theorem]] shows that there are nonstandard models of PA of all infinite cardinalities. This is not the case for the original (second-order) Peano axioms, which have only one model, up to isomorphism.{{sfn|Hermes|1973|loc=VI.3.1}} This illustrates one way the first-order system PA is weaker than the second-order Peano axioms.

When interpreted as a proof within a first-order [[set theory]], such as [[Zermelo–Fraenkel set theory|ZFC]], Dedekind's categoricity proof for PA shows that each model of set theory has a unique model of the Peano axioms, up to isomorphism, that embeds as an initial segment of all other models of PA contained within that model of set theory. In the standard model of set theory, this smallest model of PA is the standard model of PA; however, in a nonstandard model of set theory, it may be a nonstandard model of PA. This situation cannot be avoided with any first-order formalization of set theory.

It is natural to ask whether a countable nonstandard model can be explicitly constructed. The answer is affirmative as [[Skolem]] in 1933 provided an explicit construction of such a [[Non-standard model of arithmetic|nonstandard model]].  On the other hand, [[Tennenbaum's theorem]], proved in 1959, shows that there is no countable nonstandard model of PA in which either the addition or multiplication operation is [[computable function|computable]].{{sfn|Kaye|1991|loc=Section 11.3}} This result shows it is difficult to be completely explicit in describing the addition and multiplication operations of a countable nonstandard model of PA. There is only one possible [[order type]] of a countable nonstandard model. Letting ''ω'' be the order type of the natural numbers, ''ζ'' be the order type of the integers, and ''η'' be the order type of the rationals, the order type of any countable nonstandard model of PA is {{nowrap|''ω'' + ''ζ''·''η''}}, which can be visualized as a copy of the natural numbers followed by a dense linear ordering of copies of the integers.

==== Overspill ====

A '''cut''' in a nonstandard model ''M'' is a nonempty subset ''C'' of ''M'' so that ''C'' is downward closed (''x'' < ''y'' and ''y'' &isin; ''C'' ⇒ ''x'' &isin; ''C'') and ''C'' is closed under successor. A '''proper cut''' is a cut that is a proper subset of ''M''. Each nonstandard model has many proper cuts, including one that corresponds to the standard natural numbers.   However, the induction scheme in Peano arithmetic prevents any proper cut from being definable.  The overspill lemma, first proved by Abraham Robinson, formalizes this fact.

{{math theorem|name=Overspill lemma{{sfn|Kaye|1991|pages=70ff.}}|math_statement= Let ''M'' be a nonstandard model of PA and let ''C'' be a proper cut of ''M''. Suppose that <math>\bar a</math> is a tuple of elements of ''M'' and <math>\varphi(x, \bar a)</math> is a formula in the language of arithmetic so that
:<math>M \vDash \varphi(b, \bar a)</math> for all ''b'' &isin; ''C''.
Then there is a ''c'' in ''M'' that is greater than every element of ''C'' such that
:<math>M \vDash \varphi(c, \bar a).</math>
}}