型（模型）

型
术语名称	型
英语名称	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{ \bar{b}=(b_1,\cdots,b_n) }[/math] 在集合 [math]\displaystyle{ A }[/math] 上实现的 [math]\displaystyle{ n }[/math]-型( [math]\displaystyle{ n }[/math]-type realized by [math]\displaystyle{ \bar{b} }[/math] in [math]\displaystyle{ \mathfrak{M} }[/math] over [math]\displaystyle{ A }[/math])，记作 [math]\displaystyle{ \mathrm{tp}^\mathfrak{M} (\bar{b}/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])。