在模型論 中，型 是一階邏輯 中的一個相容的公式集合。一個完備型 是這類集合中的一個極大元素。
首先固定以下對象：
L
{\displaystyle {\mathcal {L}}}
T
{\displaystyle T}
L
{\displaystyle {\mathcal {L}}}
M
{\displaystyle {\mathcal {M}}}
T
{\displaystyle T}
模型 ，
A
⊂
M
{\displaystyle A\subset {\mathcal {M}}}
記
L
(
A
)
=
L
∪
{
c
a
:
a
∈
A
}
{\displaystyle {\mathcal {L}}(A)={\mathcal {L}}\cup \{c_{a}:a\in A\}}
M
{\displaystyle {\mathcal {M}}}
L
(
A
)
{\displaystyle {\mathcal {L}}(A)}
結構 ，記
T
h
A
(
M
)
{\displaystyle \mathrm {Th} _{A}({\mathcal {M}})}
設
n
∈
N
{\displaystyle n\in \mathbb {N} }
Σ
(
v
→
)
=
Σ
(
v
1
,
…
,
v
n
)
{\displaystyle \Sigma ({\vec {v}})=\Sigma (v_{1},\ldots ,v_{n})}
L
(
A
)
{\displaystyle {\mathcal {L}}(A)}
(
v
1
,
…
,
v
n
)
{\displaystyle (v_{1},\ldots ,v_{n})}
若
Σ
(
v
→
)
{\displaystyle \Sigma ({\vec {v}})}
T
h
A
(
M
)
{\displaystyle \mathrm {Th} _{A}({\mathcal {M}})}
T
h
A
(
M
)
{\displaystyle \mathrm {Th} _{A}({\mathcal {M}})}
n-型 。
此外，若
Σ
(
v
→
)
{\displaystyle \Sigma ({\vec {v}})}
完備型 ；一個型
Σ
(
v
→
)
{\displaystyle \Sigma ({\vec {v}})}
∀
ϕ
∈
L
(
A
)
ϕ
∈
Σ
(
v
→
)
∨
¬
ϕ
∈
Σ
(
v
→
)
{\displaystyle \forall \phi \in {\mathcal {L}}(A)\quad \phi \in \Sigma ({\vec {v}})\vee \neg \phi \in \Sigma ({\vec {v}})}
由佐恩引理 與圖法可推出每個型都包含於一個完備型。 通常也將型與完備型分別稱作部份型 與型 ，以下將採此稱呼。 以
S
n
M
(
A
)
{\displaystyle S_{n}^{\mathcal {M}}(A)}
T
h
A
(
M
)
{\displaystyle \mathrm {Th} _{A}({\mathcal {M}})}
N
{\displaystyle {\mathcal {N}}}
M
{\displaystyle {\mathcal {M}}}
基本擴展 ，
b
→
=
(
b
1
,
…
,
b
n
)
∈
N
{\displaystyle {\vec {b}}=(b_{1},\ldots ,b_{n})\in {\mathcal {N}}}
b
→
∈
N
{\displaystyle {\vec {b}}\in {\mathcal {N}}}
t
p
N
(
b
→
|
A
)
:=
{
ϕ
(
b
→
)
∈
L
(
A
)
:
N
⊨
ψ
(
b
→
)
}
{\displaystyle \mathrm {tp} ^{\mathcal {N}}({\vec {b}}|A):=\{\phi ({\vec {b}})\in {\mathcal {L}}(A):{\mathcal {N}}\models \psi ({\vec {b}})\}}
根據緊緻性定理 可推出：對所有型
p
∈
S
n
M
(
A
)
{\displaystyle p\in S_{n}^{\mathcal {M}}(A)}
M
{\displaystyle {\mathcal {M}}}
N
{\displaystyle {\mathcal {N}}}
b
→
∈
N
{\displaystyle {\vec {b}}\in {\mathcal {N}}}
p
=
t
p
N
(
b
→
|
A
)
{\displaystyle p=\mathrm {tp} ^{\mathcal {N}}({\vec {b}}|A)}
b
→
{\displaystyle {\vec {b}}}
實現 了 p；如果該模型中不存在這樣的
b
→
{\displaystyle {\vec {b}}}
省略 了 p。
以下取一階語言
L
=
⟨
<
⟩
{\displaystyle {\mathcal {L}}=\langle <\rangle }
Q
⊨
D
L
O
{\displaystyle \mathbb {Q} \models \mathrm {DLO} }
A
=
Q
{\displaystyle A=\mathbb {Q} }
p
=
t
p
1
Q
(
2
|
A
)
{\displaystyle p=\mathrm {tp} _{1}^{\mathbb {Q} }(2|A)}
x=2 時在
Q
{\displaystyle \mathbb {Q} }
ϕ
(
x
)
∈
L
(
A
)
{\displaystyle \phi (x)\in {\mathcal {L}}(A)}
x
≠
3
{\displaystyle x\neq 3}
x
<
5
{\displaystyle x<5}
∃
y
y
<
x
{\displaystyle \exists y\;y<x}
p 在
Q
{\displaystyle \mathbb {Q} }
Q
<
R
{\displaystyle \mathbb {Q} <\mathbb {R} }
q
:=
t
p
1
R
(
2
|
A
)
{\displaystyle q:=\mathrm {tp} _{1}^{\mathbb {R} }({\sqrt {2}}|A)}
Q
{\displaystyle \mathbb {Q} }
ϕ
α
(
x
)
:=
2
−
α
<
x
<
2
+
α
,
(
α
∈
Q
)
{\displaystyle \phi _{\alpha }(x):=2-\alpha <x<2+\alpha ,\quad (\alpha \in \mathbb {Q} )}
而這些公式在
Q
{\displaystyle \mathbb {Q} }
Q
{\displaystyle \mathbb {Q} }
Q
{\displaystyle \mathbb {Q} }
Q
{\displaystyle \mathbb {Q} }
戴德金切割 。
現在考慮另一個例子：取一階語言
L
=
⟨
+
,
−
,
⋅
,
0
,
1
,
<
⟩
{\displaystyle {\mathcal {L}}=\langle +,-,\cdot ,0,1,<\rangle }
A
=
∅
{\displaystyle A=\emptyset }
R
⊨
O
R
{\displaystyle \mathbb {R} \models \mathrm {OR} }
ϕ
n
(
x
)
:=
x
>
1
+
⋯
+
1
⏟
n
{\displaystyle \phi _{n}(x):=x>\underbrace {1+\cdots +1} _{n}}
Σ
:=
{
ϕ
n
:
n
∈
N
}
{\displaystyle \Sigma :=\{\phi _{n}:n\in \mathbb {N} \}}
任何
Σ
{\displaystyle \Sigma }
T
h
A
(
R
)
{\displaystyle \mathrm {Th} _{A}(\mathbb {R} )}
緊緻性定理 可證
Σ
{\displaystyle \Sigma }
Σ
{\displaystyle \Sigma }
R
{\displaystyle \mathbb {R} }
R
{\displaystyle \mathbb {R} }
A
⊂
M
,
|
A
|
<
|
M
|
{\displaystyle A\subset {\mathcal {M}},|A|<|{\mathcal {M}}|}
飽和模型 。
先前關於
(
Q
,
<
)
{\displaystyle (\mathbb {Q} ,<)}
T
⊨
D
L
O
{\displaystyle T\models \mathrm {DLO} }
S
1
T
(
A
)
{\displaystyle S_{1}^{T}(A)}
戴德金切割
(
L
,
U
)
{\displaystyle (L,U)}
A
=
L
∪
U
{\displaystyle A=L\cup U}
∀
x
∀
y
x
∈
L
∧
y
∈
U
⇒
x
<
y
{\displaystyle \forall x\;\forall y\quad x\in L\wedge y\in U\Rightarrow x<y}
註：為了使結論簡潔，在此容許 L 含最大元素（或 U 含最小元素），而且 L 或 U 可以是空集合。 此外，
S
1
T
(
A
)
{\displaystyle S_{1}^{T}(A)}
量詞消去 。
取定一個代數封閉域
K
{\displaystyle K}
A
⊂
K
{\displaystyle A\subset K}
K
0
{\displaystyle K_{0}}
A
{\displaystyle A}
交換環譜 的連續 映射：
i
:
S
n
(
A
)
⟶
S
p
e
c
(
K
0
[
X
1
,
…
,
X
n
]
)
{\displaystyle i:S_{n}(A)\longrightarrow \mathrm {Spec} (K_{0}[X_{1},\ldots ,X_{n}])}
p
↦
I
p
:=
{
f
∈
K
0
[
X
]
:
(
f
(
v
→
)
=
0
)
∈
p
}
{\displaystyle p\mapsto I_{p}:=\{f\in K_{0}[X]:(f({\vec {v}})=0)\in p\}}
同用利用量詞消去 性質，可以證明 i 給出集合的雙射 ，由此在
S
p
e
c
(
K
0
[
X
1
,
…
,
X
n
]
)
{\displaystyle \mathrm {Spec} (K_{0}[X_{1},\ldots ,X_{n}])}
ϕ
(
v
→
)
:=
f
1
(
v
→
)
=
0
∧
⋯
∧
f
m
(
v
→
)
=
0
{\displaystyle \phi ({\vec {v}}):=f_{1}({\vec {v}})=0\wedge \cdots \wedge f_{m}({\vec {v}})=0}
定義的開/閉集，其中
f
1
,
…
,
f
m
∈
K
0
[
X
1
,
…
,
X
n
]
{\displaystyle f_{1},\ldots ,f_{m}\in K_{0}[X_{1},\ldots ,X_{n}]}
超越擴張 上實現的型。
給定一個 n-型 p，一個自然的問題是研究省略 p 的模型。當 p 是孤立點時，所有模型都實現 p；反過來說，省略型定理 則斷言：設
L
{\displaystyle {\mathcal {L}}}
可數 語言，若 p 非孤立點，則有一個省略 p 的可數模型。
舉例來說，在特徵為零的代數封閉域理論中，取 p 為由一個相對於
Q
{\displaystyle \mathbb {Q} }
代數數 是個省略 p 的可數模型，而任何
Q
{\displaystyle \mathbb {Q} }
![{\displaystyle i:S_{n}(A)\longrightarrow \mathrm {Spec} (K_{0}[X_{1},\ldots ,X_{n}])}](https://wikimedia.org/api/rest_v1/media/math/render/svg/22e18e41a77e16cac32f61c08f268da510580831)
![{\displaystyle p\mapsto I_{p}:=\{f\in K_{0}[X]:(f({\vec {v}})=0)\in p\}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ddc1c16f2a96ac144d64fefa2f8d80eeabbbd996)
![{\displaystyle \mathrm {Spec} (K_{0}[X_{1},\ldots ,X_{n}])}](https://wikimedia.org/api/rest_v1/media/math/render/svg/dae9a9575ed9596b1689620ce880590d4b20a14d)
![{\displaystyle f_{1},\ldots ,f_{m}\in K_{0}[X_{1},\ldots ,X_{n}]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/c04ae5730a505ca1d8ff1b2ec891a68026b32ee3)