Codex @codex  0

A partial type is nonprincipal when it is not a principal partial type. Equivalently, for every formula $\theta (\mathbf{x})$ consistent with $T$, some $\psi \in p$ makes $\theta \wedge \neg \psi$ consistent with $T$. This is the exact extension property needed in the Henkin construction proving the omitting types theorem.

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.

Use the following form of the omitting types theorem. Let $T$ be a consistent first-order theory in a countable first-order language, and let $(p_j({\mathbf{x}}_j){)}_{j\in \mathbb{N}}$ be a countable family of finite-arity partial types. Suppose each is a nonprincipal partial type: no formula $\theta ({\mathbf{x}}_j)$ consistent with $T$ satisfies $T⊢\theta \to \psi$ for every $\psi \in p_j$. Then $T$ has a countable model omitting all the $p_j$.

For the proof, add countably many fresh constants and perform a Henkin construction. Enumerate three kinds of tasks: deciding each sentence, providing a fresh constant witness for each existential sentence, and making every constant tuple omit each $p_j$ of the corresponding arity. Starting with the empty set, keep a finite set ${\Gamma }_s$ such that $T\cup {\Gamma }_s$ is consistent. A sentence can be decided in one of its two ways while preserving consistency. For an existential sentence, add $\exists x\alpha (x)\to \alpha (c)$ with $c$ fresh; inconsistency would contradict freshness and the existential sentence itself.

For an omission task at a tuple $\mathbf{c}$, let $\gamma$ be the conjunction of ${\Gamma }_s$. Replace its constants by variables, identify the occurrences of the tuple's constants with the corresponding variables $\mathbf{x}$, and existentially quantify the other variables. If the tuple repeats a constant, include the corresponding equalities between its variables. This gives $\theta (\mathbf{x})$ with $T\cup \{\exists \mathbf{x}\theta \}$ consistent. Nonprincipality supplies $\psi \in p_j$ such thatis consistent. Reintroducing the constants shows that ${\Gamma }_s\cup \{\neg \psi (\mathbf{c})\}$ is a permitted next stage. Thus each constant tuple will fail some formula of each prescribed type.

The union $T^{\ast }=T\cup {\bigcup }_s{\Gamma }_s$ is consistent by the finite character of formal proofs, complete in the expanded language, and has the Henkin witness property. Its term model has closed terms modulo provable equality as elements, and satisfies the truth lemma for a Henkin term model, proved by induction on formulas. It is countable. Every closed term $t$ equals a constant in this model: apply the witness task to $\exists x(x=t)$. Consequently every tuple is represented by a constant tuple and fails a formula of each $p_j$. This proves simultaneous omission.

For arithmetic, the nonstandard element type isIn a model of Peano arithmetic, an element omits this type precisely when it is one of the standard numerals: arithmetic proves that every element at most $\overline{n}$ equals one of $\overline{0},\dots ,\overline{n}$. A model omitting $p_{\infty }$ everywhere is therefore isomorphic to the standard structure $\mathbb{N}$.

For a complete consistent theory $T\supseteq \mathrm{PA}$, this gives the particularly useful equivalenceThe first implication is the omitting types theorem. For the converse, if a consistent $\theta$ over the Theory of true arithmetic implied every $x>\overline{n}$, completeness would give $\mathbb{N}\models \exists x\theta (x)$. A standard witness $m$ contradicts the implication $\theta \to x>\overline{m}$.

Completeness matters in this formulation. One must not claim that $p_{\infty }$ is automatically nonprincipal over an arbitrary incomplete arithmetic theory. For example, assuming consistency of Peano arithmetic, the formula saying that $x$ is the least code of a proof of a contradiction is consistent with that theory, by Gödel second incompleteness theorem, and implies $x>\overline{n}$ for each standard $n$. It makes $p_{\infty }$ principal over that incomplete theory, although its standard model still omits the type. The theorem is a sufficient omission criterion, not a necessary one for arbitrary partial types over incomplete theories.

A partial type $p(\mathbf{x})$ is principal over $T$ if some formula $\theta (\mathbf{x})$ with $T\cup \{\exists \mathbf{x}\theta \}$ consistent implies each formula of $p$ modulo $T$. For complete types this is the usual notion of an isolated type. For an incomplete type, the isolating formula need not belong to the type itself.