Mathematical logic and foundations Definition

Type

Builds on Theory Well-formed formula Model Signature

Definition

Let $L$ be a signature, let $T$ be an $L$ -theory, and let $n \ge 1$ . An $n$ -type of $T$ is a set $p(x_1, \dots, x_n)$ of $L$ -formulas whose free variables are among $x_1, \dots, x_n$ , such that $T \cup p$ is satisfiable. This means that some model $M$ of $T$ has a tuple $(a_1, \dots, a_n)$ that satisfies every formula of $p$ . The type $p$ is complete if for every $L$ -formula $\varphi(x_1, \dots, x_n)$ , either $\varphi \in p$ or $\neg \varphi \in p$ . A model $M$ of $T$ realizes $p$ if some tuple of $M$ satisfies every formula of $p$ , and omits $p$ otherwise. The set of complete $n$ -types of $T$ is written $S_n(T)$ .

Let $M$ be a model and $A$ a set of elements of $M$ . Let $L_A$ be $L$ extended by a new constant for each element of $A$ . A type over $A$ is a type of the $L_A$ -theory of $M$ . The set of complete $n$ -types over $A$ is written $S_n^M(A)$ .

Remarks

For a tuple $\bar{a}$ of a model $M$ , the set $\operatorname{tp}(\bar{a})$ of all formulas satisfied by $\bar{a}$ in $M$ is a complete type of the theory of $M$ .

Example: let $T$ be the theory of $(\N, 0, 1, +, \cdot, <)$ and let $p(x) = \set{x > 1 + \cdots + 1 \ (k \text{ terms}) : k \ge 1}$ . Each finite part of $p$ is satisfied in $\N$ by a large number, so by compactness $T \cup p$ has a model, and $p$ is a $1$ -type. The standard model $\N$ omits $p$ , while every nonstandard model of $T$ realizes it.

Non-example: in the theory of fields, $\set{x = 0, \; x \cdot x = 1}$ is not a type, since $x = 0$ gives $x \cdot x = 0 \ne 1$ in every field.

The set $S_n(T)$ carries a natural topology, with basic open sets $\set{p : \varphi \in p}$ ; it is a compact, totally disconnected Hausdorff space by the compactness theorem.

Reading path

To understand this page from the ground up, read these 5 pages in order. The foundations come first.

Show the path as a graph

Each page uses the pages above it. The colour of the bar on a box shows how strong the evidence is, and the box also gives it as text. The list has the same pages.

no evidence level

Model concept
Signature concept
Theory concept
Well-formed formula concept
Type definition

Tag	`VA7AK1R5AN`
URI	`m2://VA7AK1R5AN`
Kind	definition
Writing	W0 stub
MSC	03C07, 03C50
Defines	Type
Uses	Theory, Well-formed formula, Model, Signature
Changed	2 November 2026

Type

Definition

Remarks

Reading path

Further reading

What this page needs for W1

What links here