Partial type ($p(\mathbf{x})$)

A partial type over a first-order theory $T$ is a set of first-order formulas in a fixed finite tuple of variables which is jointly consistent with $T$. A tuple realizes it when it satisfies every formula in the set. A complete type additionally decides every formula in those variables.

A principal formula of a type is a logical formula first-order consistent with the base first-order theory that, modulo that first-order theory, implies every logical formula of the partial type. For a complete type it isolates a single point of the type space. A realized finite-tuple partial type in a finite first-order structure has such a logical formula by conjoining one distinguishing logical formula for each competing tuple with a different partial type.

Fix a tuple in a finite first-order structure. For every tuple of a different complete type, choose a logical formula true at the first tuple and false at the competitor. The finite conjunction selects only tuples of the desired partial type inside the first-order structure. Every implication from that conjunction to a member of the partial type is true in the first-order structure and hence belongs to its complete theory. Thus the conjunction isolates the partial type, even in an infinite first-order language.

The quantifier-free type of a tuple records all atomic and negated atomic formulas it satisfies, equivalently all quantifier-free formulas. Equal such types identify the generated substructures by sending each term value at one tuple to the value of the same term at the other tuple. Equality formulas make this correspondence well defined, and the relational formulas make it an isomorphism.

In the constant-free language with multiplication as its sole nonlogical symbol, every term in one free variable is $x^k$ for some $k\ge 1$. Every atomic formula $x^r=x^s$ holds at both zero and one. Hence every quantifier-free formula, being a finite Boolean combination of those atoms, has the same truth value at both points. They have the same quantifier-free type, and neither singleton is quantifier-free definable. Quantifiers distinguish them: $\forall y(xy=x)$ defines zero, while $\forall y(xy=y)$ defines one. These formulas do not rely on named zero or one constants.

For $A\subseteq M$, an A-type over first-order structure $M$ is a set of formulas in a fixed finite tuple of variables, with parameters in $A$, consistent with the complete theory of $M$ expanded by constants for $A$. Every finite subset is realized in $M$. A complete type decides all formulas in its variables over those parameters.

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.

A first-order theory locally omits a family $\Gamma (\mathbf{x})$ if every formula $\theta (\mathbf{x})$ consistent with it has a consistent refinement $\theta \wedge \neg \gamma$ for some $\gamma \in \Gamma$. Equivalently no consistent formula implies all of $\Gamma$. In a countable language the omitting types theorem converts this local condition into a countable model with no realization of the family.

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.