型（模型）
| 型 | |
|---|---|
| 术语名称 | 型 |
| 英语名称 | type |
| 实现 | |
|---|---|
| 术语名称 | 实现 |
| 英语名称 | realize |
型(type)是关于理论的数学对象，被模型中的元组实现(realize)。用于描述模型中某个或某些特殊个体对象视角的特征。具体地说，我们在固定观察论域中的某些个体对象与一个子集（或参数集）的关系时，通过全部的能够为这些对象和子集成立的公式集合来描述它们所符合的特征，称这样的公式集为这个元组实现的一个型。型可以理解为论域中元素和参数集之间基于共同满足公式所建立的关系。而模型论域中存在元组实现的型称为这个模型实现的型，参见完备、部分（型）。
定义
对形式语言 [math]\displaystyle{ \mathcal{L} }[/math] 的理论 [math]\displaystyle{ T }[/math] 和某个参数集 [math]\displaystyle{ A }[/math] ，将这个参数集中的个体以个体常项的方式添加到语言中得到形式语言 [math]\displaystyle{ \mathcal{L}_A }[/math] 。考虑 [math]\displaystyle{ \mathcal{L}_A }[/math] 中的公式集合 [math]\displaystyle{ \Sigma }[/math] ，其中的自由变元只有 [math]\displaystyle{ n }[/math] 个，记为 [math]\displaystyle{ x_1,\cdots,x_n }[/math] ，若 [math]\displaystyle{ T \cup \Sigma }[/math] 在 [math]\displaystyle{ \mathcal{L}_A }[/math] 中一致（或者说有模型，存在某个 [math]\displaystyle{ \mathcal{L}_A }[/math]-模型及其上的赋值满足这一理论）,则称集合 [math]\displaystyle{ \Sigma }[/math] 是理论 [math]\displaystyle{ T }[/math] 在集合 [math]\displaystyle{ A }[/math] 上的 [math]\displaystyle{ n }[/math]-型( [math]\displaystyle{ n }[/math]-type of [math]\displaystyle{ T }[/math] over [math]\displaystyle{ A }[/math])。
对形式语言 [math]\displaystyle{ \mathcal{L} }[/math] 中的模型 [math]\displaystyle{ \mathfrak{M}=(M,I) }[/math] ，以及其个体域的任意子集 [math]\displaystyle{ A\subseteq M }[/math] ，将这个子集中的个体以个体常项的方式添加到语言中得到形式语言 [math]\displaystyle{ \mathcal{L}_A }[/math] 。考虑 [math]\displaystyle{ \mathcal{L}_A }[/math] 中的公式集合 [math]\displaystyle{ \Sigma }[/math] ，其中的自由变元只有 [math]\displaystyle{ n }[/math] 个，记为 [math]\displaystyle{ x_1,\cdots,x_n }[/math] ，则若存在一些元素 [math]\displaystyle{ b_1,\cdots,b_n\in M }[/math] ，满足 [math]\displaystyle{ \mathfrak{M}\vDash \Sigma[b_1/x_1,\cdots,b_n/x_n] }[/math] ，则称集合 [math]\displaystyle{ \Sigma }[/math] 是模型 [math]\displaystyle{ \mathfrak{M} }[/math] 在集合 [math]\displaystyle{ A }[/math] 上由元组 [math]\displaystyle{ \bar{b}=(b_1,\cdots,b_n) }[/math] 实现的 [math]\displaystyle{ n }[/math]-型( [math]\displaystyle{ n }[/math]-type realized by [math]\displaystyle{ \bar{b} }[/math] in/of [math]\displaystyle{ \mathfrak{M} }[/math] over [math]\displaystyle{ A }[/math])。
若对任意有限子集 [math]\displaystyle{ \Pi\subseteq\Sigma }[/math] 都存在这样的元素 [math]\displaystyle{ b_1,\cdots,b_n\in M }[/math] （或表达为“都被实现”，且满足不同的有限子集中的元素不要求相同），则称集合 [math]\displaystyle{ \Sigma }[/math] 是模型 [math]\displaystyle{ \mathfrak{M} }[/math] 在集合 [math]\displaystyle{ A }[/math] 上的 [math]\displaystyle{ n }[/math]-型( [math]\displaystyle{ n }[/math]-type of [math]\displaystyle{ \mathfrak{M} }[/math] over [math]\displaystyle{ A }[/math])。若模型 [math]\displaystyle{ \mathfrak{M} }[/math] 在集合 [math]\displaystyle{ A }[/math] 上的型 [math]\displaystyle{ \Sigma }[/math] 中，对集合 [math]\displaystyle{ \Sigma }[/math] 本身（可能是无穷集合）也存在这样的元素，也就是存在一组元组实现这个集合，则也称型 [math]\displaystyle{ \Sigma }[/math] 在模型 [math]\displaystyle{ \mathfrak{M} }[/math] 中被实现([math]\displaystyle{ \Sigma }[/math] is realized in [math]\displaystyle{ \mathfrak{M} }[/math])（即省略掉“由……”）。
当不需要讨论 [math]\displaystyle{ n }[/math] 或 [math]\displaystyle{ n }[/math] 的具体取值不重要时， n-型也直接省略为型(type)。
举例
公式 [math]\displaystyle{ x\neq 3, x\leq 4, \exists y (y\lt x) }[/math] 所构成的集合，是一阶自然数算术语言中的一个型。确切地说，是自然数的模型中由元组 [math]\displaystyle{ (1) }[/math] 或 [math]\displaystyle{ (2) }[/math] 或 [math]\displaystyle{ (4) }[/math] 在集合 [math]\displaystyle{ \{3,4\} }[/math] （出现在公式中的参数集）上实现的 1-型。
反过来，如果不做参数集限制，自然数的模型中元组 [math]\displaystyle{ (2) }[/math] 所实现的完备 1-型，作为集合，包含任意含有同一个自由变项（比方说 [math]\displaystyle{ x }[/math]）且这一自由变项代入 2 时成立的公式，包括且不限于 [math]\displaystyle{ x\gt 1, x\neq 3, x\leq 4, \exists y (y\lt x) }[/math] 。
公式集 [math]\displaystyle{ \{0\lt x\}\cup\{x\lt \tfrac{1}{n}|n\in\mathbb{N}^*\} }[/math] ，其任意有限子集在有理数序中可满足，因此这一公式集是有理数序在参数集 [math]\displaystyle{ \{0,1\} }[/math] 上的一个 1-型，但这个公式集本身不被满足，因此这个 1-型并没有被有理数实现。
性质
- 实现被某个特定的初等扩张保持。若 [math]\displaystyle{ X\subseteq A }[/math] ，且 [math]\displaystyle{ \mathfrak{A}_X }[/math] 实现了 [math]\displaystyle{ \Sigma }[/math] ，则存在 [math]\displaystyle{ \mathfrak{B} }[/math] 满足 [math]\displaystyle{ \mathfrak{A}\preceq\mathfrak{B} }[/math] 且 [math]\displaystyle{ \mathfrak{B}_X }[/math] 也实现 [math]\displaystyle{ \Sigma }[/math] 。
- 对模型 [math]\displaystyle{ \mathfrak{A} }[/math] ，存在一个模型 [math]\displaystyle{ \mathfrak{B} }[/math] 使得 [math]\displaystyle{ \mathfrak{A}\preceq\mathfrak{B} }[/math] 且 [math]\displaystyle{ \mathfrak{B}_A }[/math] 实现 [math]\displaystyle{ \mathfrak{A}_A }[/math] 所实现的每个模型。
- 对任意有限模型和其上的型，总是能构造出一个以这个模型为起点的初等链，使这个链中每个模型都实现这个型。
| 模型论 | ||||
|---|---|---|---|---|
| 研究对象 | 理论和模型 | 形式语言 [math]\displaystyle{ \mathcal{L} }[/math] 的理论 [math]\displaystyle{ T }[/math] | 形式语言 [math]\displaystyle{ \mathcal{L} }[/math] 的模型 [math]\displaystyle{ \mathfrak{A} }[/math] | |
| 刻画性质 | 语法一致性、可满足性/语义一致性、完备性 | 签名、基数（有限、无穷） | ||
| 相互关系 | 模型 [math]\displaystyle{ \mathfrak{A} }[/math] 的理论（理论集 [math]\displaystyle{ \operatorname{Th}\mathfrak{A} }[/math] ） | 理论 [math]\displaystyle{ T }[/math] 的模型 | ||
| 模型间的关系 | ||||
| 同构 | 同构 [math]\displaystyle{ \cong }[/math] | |||
| 子模型相关 | 子模型（子结构）、扩张 | 模型链 | 同构嵌入 | |
| 初等子模型相关 | 初等子模型（初等子结构） [math]\displaystyle{ \preceq }[/math] 、初等扩张 [math]\displaystyle{ \succeq }[/math] | 初等链、初等链的极限 | 初等嵌入 | |
| 初等等价 | 初等等价 [math]\displaystyle{ \equiv }[/math] | |||
| 相关定理 | Tarski 初等链定理、 Tarski–Vaught 测试 | |||
| 图引理、初等图引理 （常量符号“加入”语言 [math]\displaystyle{ \mathcal{L}_A }[/math] /常量符号“加入”模型 [math]\displaystyle{ \mathfrak{M}_A }[/math] 、 原子图 [math]\displaystyle{ D(\mathfrak{A}) }[/math] 、初等图 [math]\displaystyle{ D_{el}(\mathfrak{A}) }[/math]） | ||||
| 理论是否完备、是否确定模型结构——理论的不同构模型数目问题 | ||||
| 刻画 | Löwenheim–Skolem 定理、 [math]\displaystyle{ \kappa }[/math]-范畴性 | |||
| 应用 | 模型分类 | 标准模型、非标准模型 | ||
| 定理 | （Gödel 不完备定理）、转换原理、 Łoś–Vaught 测试 | |||
| 理论是否确定模型结构完备——理论的模型完备性理论 | ||||
| 模型完备性 | 理论的模型完备性 | 理论的子模型完备性 | 理论的模型完备化 | |