Nonstandard element type (source code)

= Nonstandard element type
{title2=$p_\infty(x)=\{x>\overline n:n\in\mathbb N\}$}

In a model of <Peano arithmetic>, an element realizes this <partial type> exactly when it is not a standard numeral. A model omitting it is isomorphic to the standard natural-number structure. For a complete consistent extension $T$ of arithmetic, the type is nonprincipal exactly when $T$ is the <Theory of true arithmetic>: apply the <omitting types theorem> in one direction and use an actual standard witness to refute any proposed isolating formula in the other. For incomplete theories, a principal partial type can still be omitted by some models.