在模型论中,型是一阶逻辑中的一个相容的公式集合。一个完备型是这类集合中的一个极大元素。
首先固定以下对象:
- :一个一阶语言
- :一个-理论
- 为 的一个模型,
记 (即:将 A “加入”语言的常量符号)。于是 自然地成为 的一个结构,记 为相应的完备理论。
设 , 为一个 的子集,使其元素均为带 n 个自由变元 的公式。
- 若 与 相容,则称之为 上的 n-型。
- 此外,若 对集合包含关系是极大的,则称之完备型;一个型 是完备型的充要条件是
- 由佐恩引理与图法可推出每个型都包含于一个完备型。
- 通常也将型与完备型分别称作部份型与型,以下将采此称呼。
以 表示所有 上 n 个变元的型,集合 A 也称作参数集。设结构 为 的一个基本扩展,,则容易验证以下集合是个型,称之为 在 A 上的型:
根据紧致性定理可推出:对所有型 ,都存在一个 的基本扩展 及 使得 ,此时称 实现 了 p;如果该模型中不存在这样的 ,则称此模型省略了 p。
以下取一阶语言 ,并设 DLO 为稠密全序(或称稠密线性序)理论。此时有 。不妨取 ,此时 是一个型,它代表所有代入 x=2 时在 中成立的公式 ,例如 、、……。
p 在 里已经实现。此外也可以考虑基本扩展 及型 。q 无法在 中实现,因为 q 包含下述所有公式
而这些公式在 定义出的子集交集为空;在这个例子里,一个型无法被实现的原因可归于参数集 A“太大”,事实上 能实现所有带有限参数的型。一般来说,无理数给出了无法在 中实现的型,在 中描述这些“数”的一套经典办法是戴德金切割。
现在考虑另一个例子:取一阶语言 ,OR 为有序环的理论,。此时 。考虑下述公式:
任何 的有限子集都与 相容,所以由紧致性定理可证 包含于一个型; 无法在 中实现,却能在 的某个基本扩展——超实数中实现。一个能实现所有满足 的型的模型称作饱和模型。
取定一个代数封闭域 及其子集 。令 为 生成的子域,则可定义下述映到交换环谱的连续映射:
同用利用量词消去性质,可以证明 i 给出集合的双射,由此在 引出的拓扑较扎里斯基拓扑细,而扎里斯基拓扑里的闭集拉回后正好是 Stone 空间中由
定义的开/闭集,其中 。扎里斯基拓扑中对应到不可约子簇的一般点则拉回到在某个超越扩张上实现的型。
给定一个 n-型 p,一个自然的问题是研究省略 p 的模型。当 p 是孤立点时,所有模型都实现 p;反过来说,省略型定理则断言:设 是可数语言,若 p 非孤立点,则有一个省略 p 的可数模型。
举例来说,在特征为零的代数封闭域理论中,取 p 为由一个相对于的超越元素给出的型,任两个这样的超越元素都在一个基本扩展中同构,所以 p 的定义与选取无关。这是 Stone 空间中唯一的非孤立点。代数数是个省略 p 的可数模型,而任何的超越扩张都实现 p。其馀的型都由某个代数数给出,而且被所有模型实现。