在模型論中，型是一階邏輯中的一個相容的公式集合。一個完備型是這類集合中的一個極大元素。

嚴格定義
首先固定以下對象：

\mathcal{L} ：一個一階語言

T ：一個\mathcal{L}-理論

\mathcal{M} 為 T 的一個模型，A \subset \mathcal{M}

記 \mathcal{L}(A) = \mathcal{L} \cup \{c_a : a \in A \}（即：將 A 「加入」語言的常量符號）。於是 \mathcal{M} 自然地成為 \mathcal{L}(A) 的一個結構，記 \mathrm{Th}_A(\mathcal{M}) 為相應的完備理論。

設 n \in \mathbb{N}，\Sigma(\vec v) = \Sigma(v_1, \ldots, v_n) 為一個 \mathcal{L}(A) 的子集，使其元素均為帶 n 個自由變元 (v_1, \ldots, v_n) 的公式。

• 若 \Sigma(\vec v) 與 \mathrm{Th}_A(\mathcal{M}) 相容，則稱之為 \mathrm{Th}_A(\mathcal{M}) 上的 n-型。
• 此外，若 \Sigma(\vec v) 對集合包含關係是極大的，則稱之完備型；一個型 \Sigma(\vec v) 是完備型的充要條件是

: \forall \phi \in \mathcal{L}(A) \quad \phi \in \Sigma(\vec v) \vee \neg\phi \in \Sigma(\vec v)
: 由佐恩引理與圖法可推出每個型都包含於一個完備型。

• 通常也將型與完備型分別稱作部份型與型，以下將採此稱呼。

以 S^\mathcal{M}_n(A) 表示所有\mathrm{Th}_A(\mathcal{M}) 上 n 個變元的型，集合 A 也稱作參數集。設結構 \mathcal{N} 為 \mathcal{M} 的一個基本擴展，\vec b = (b_1, \ldots, b_n) \in \mathcal{N}，則容易驗證以下集合是個型，稱之為 \vec b \in \mathcal{N} 在 A 上的型：

: \mathrm{tp}^\mathcal{N}(\vec b|A) := \{\phi(\vec b) \in \mathcal{L}(A) : \mathcal{N} \models \psi(\vec b) \}

根據緊緻性定理可推出：對所有型 p \in S^\mathcal{M}_n(A)，都存在一個 \mathcal{M} 的基本擴展 \mathcal{N} 及 \vec b \in \mathcal{N} 使得 p = \mathrm{tp}^\mathcal{N}(\vec b|A)，此時稱 \vec b 實現 了 p；如果該模型中不存在這樣的 \vec b，則稱此模型省略了 p。

例子
以下取一階語言 \mathcal{L} = \langle ，並設 DLO 為稠密全序（或稱稠密線性序）理論。此時有 \mathbb{Q} \models \mathrm{DLO}。不妨取 A = \mathbb{Q}，此時 p = \mathrm{tp}^\mathbb{Q}_1(2|A) 是一個型，它代表所有代入 x=2 時在 \mathbb{Q} 中成立的公式 \phi(x) \in \mathcal{L}(A)，例如 x \neq 3、x 、\exists y \; y ……。

p 在 \mathbb{Q} 裡已經實現。此外也可以考慮基本擴展 \mathbb{Q} 及型 q := \mathrm{tp}^\mathbb{R}_1(\sqrt{2}|A)。q 無法在 \mathbb{Q} 中實現，因為 q 包含下述所有公式
: \phi_\alpha(x) := 2-\alpha
而這些公式在 \mathbb{Q} 定義出的子集交集為空；在這個例子裡，一個型無法被實現的原因可歸於參數集 A「太大」，事實上 \mathbb{Q} 能實現所有帶有限參數的型。一般來說，無理數給出了無法在 \mathbb{Q} 中實現的型，在 \mathbb{Q} 中描述這些「數」的一套經典辦法是戴德金切割。

現在考慮另一個例子：取一階語言 \mathcal{L} = \langle +, -, \cdot, 0, 1, ，OR 為有序環的理論，A = \emptyset。此時 \mathbb{R} \models \mathrm{OR}。考慮下述公式：
: \phi_n(x) := x > \underbrace{1 + \cdots + 1}_{n}
: \Sigma := \{\phi_n : n \in \mathbb{N} \}

任何 \Sigma 的有限子集都與 \mathrm{Th}_A(\mathbb{R}) 相容，所以由緊緻性定理可證 \Sigma 包含於一個型；\Sigma 無法在 \mathbb{R} 中實現，卻能在 \mathbb{R} 的某個基本擴展——超實數中實現。一個能實現所有滿足 A \subset \mathcal{M}, |A| 的型的模型稱作飽和模型。

Stone空間
固定 n > 0，所有 n-型構成的空間 S^\mathcal{M}_n(A) 具備一個自然的拓撲結構，其開集由形如 \langle \phi(\vec v) \rangle := \{ p \in S^\mathcal{M}_n(A) : \phi(\vec v) \in p \} 的子集經過聯集與有限交集形成。它滿足下述性質：

• 每個 \langle \phi(\vec v) \rangle 都是既開且閉的；因此 S^\mathcal{M}_n(A) 是全不連通空間。
• S^\mathcal{M}_n(A) 是緊空間，這是緊緻性定理的直接推論。
• p 是孤立點的充要條件是存在 \phi(\vec v) 使得 p = \langle \phi(\vec v) \rangle，此時對任何公式 \psi(\vec v) ，ψ 屬於 p 的充要條件是：

: \mathrm{Th}_A(\mathcal{M}) \vdash \forall \vec v \; \phi(\vec v) \leftrightarrow \psi(\vec v)

事實上，\mathcal{L}(A) 裡所有帶 n 個自由變元的公式構成一個布爾代數，而根據定義，n-型正是其中的極大濾子；可以證明拓撲空間 S^\mathcal{M}_n(A) 等同於布爾代數理論中考慮的 Stone 空間。

個案研討
稠密全序
先前關於 (\mathbb{Q}, 的評註適用於任何稠密全序集。設 T \models \mathrm{DLO}，而 A 是其中的子集，則 S^T_1(A) 的元素一一對應到 A 所定義的戴德金切割 (L, U)：
: A = L \cup U
: \forall x \; \forall y \quad x \in L \wedge y \in U \Rightarrow x
: 註：為了使結論簡潔，在此容許 L 含最大元素（或 U 含最小元素），而且 L 或 U 可以是空集合。

此外，S^T_1(A) 的非孤立點對應到沒有最大/最小元素的切割。證明關鍵在運用 DLO 的量詞消去。

代數封閉域
取定一個代數封閉域 K 及其子集 A \subset K。令 K_0 為 A 生成的子域，則可定義下述映到交換環譜的連續映射：
: i: S_n(A) \longrightarrow \mathrm{Spec}(K_0[X_1, \ldots, X_n])
: p \mapsto I_p := \{f \in K_0[X] : (f(\vec v)=0) \in p\}

同用利用量詞消去性質，可以證明 i 給出集合的雙射，由此在 \mathrm{Spec}(K_0[X_1, \ldots, X_n]) 引出的拓撲較扎里斯基拓撲細，而扎里斯基拓撲裡的閉集拉回後正好是 Stone 空間中由
: \phi(\vec v) := f_1(\vec v)=0 \wedge \cdots \wedge f_m(\vec v)=0
定義的開/閉集，其中 f_1, \ldots, f_m \in K_0[X_1, \ldots, X_n]。扎里斯基拓撲中對應到不可約子簇的一般點則拉回到在某個超越擴張上實現的型。

省略型定理
給定一個 n-型 p，一個自然的問題是研究省略 p 的模型。當 p 是孤立點時，所有模型都實現 p；反過來說，省略型定理則斷言：設 \mathcal{L} 是可數語言，若 p 非孤立點，則有一個省略 p 的可數模型。

舉例來說，在特徵為零的代數封閉域理論中，取 p 為由一個相對於\mathbb{Q}的超越元素給出的型，任兩個這樣的超越元素都在一個基本擴展中同構，所以 p 的定義與選取無關。這是 Stone 空間中唯一的非孤立點。代數數是個省略 p 的可數模型，而任何\mathbb{Q}的超越擴張都實現 p。其餘的型都由某個代數數給出，而且被所有模型實現。

文獻

• Wilfrid Hodges, A shorter model theory (1997), Cambridge University Press ISBN 0-521-58713-1
• C. C. Chang, H. J. Keisler Model theory ISBN 0-7204-0692-7
• David Marker Model Theory: An Introduction ISBN 0-387-98760-6
• [http://www.maths.ox.ac.uk/~zilber/lect.pdf Boris Zilber 在牛津的模型論講義]