子模型完备性
| 子模型完备性 | |
|---|---|
| 术语名称 | 子模型完备性 |
| 英语名称 | submodel completeness |
| 子模型完备的 | |
|---|---|
| 术语名称 | 子模型完备的 |
| 英语名称 | submodel complete |
子模型完备性(submodel completeness)指对一个一阶理论，这个理论的任意两模型若有同一子模型可以同构嵌入则其扩张对应可以初等嵌入同一模型。根据图引理，这也等价于其每个子模型都使得模型中的原子图加入后的理论是完备的。
定义
对形式语言 [math]\displaystyle{ \mathcal{L} }[/math] 中的一阶理论 [math]\displaystyle{ T }[/math] ，若对 [math]\displaystyle{ T }[/math] 的任意模型 [math]\displaystyle{ \mathfrak{M} }[/math] 的任意子模型 [math]\displaystyle{ \mathfrak{A} }[/math] ，理论 [math]\displaystyle{ T\cup D(\mathfrak{A}) }[/math] 完备，则称理论 [math]\displaystyle{ T }[/math] 是子模型完备的(submodel complete)。
性质
对形式语言 [math]\displaystyle{ \mathcal{L} }[/math] 中的一阶理论 [math]\displaystyle{ T }[/math] ，以下命题等价：
- [math]\displaystyle{ T }[/math] 是子模型完备的。
- 对 [math]\displaystyle{ T }[/math] 上的模型 [math]\displaystyle{ \mathfrak{A},\mathfrak{B},\mathfrak{C} }[/math] ，其中 [math]\displaystyle{ \mathfrak{A} }[/math] 同时是 [math]\displaystyle{ \mathfrak{B},\mathfrak{C} }[/math] 的子模型，则考虑语言 [math]\displaystyle{ \mathcal{L}_A }[/math] 上的模型和公式，对任意的仅存在量化公式（仅含存在量词且所有量化表达式都在公式头部的公式） [math]\displaystyle{ \phi }[/math] ，若满足 [math]\displaystyle{ \mathfrak{B}_A\vDash\phi }[/math] 则有 [math]\displaystyle{ \mathfrak{C}_A\vDash\phi }[/math] 。
- [math]\displaystyle{ T }[/math] 消除量词(eliminate quantifiers)：对任意公式 [math]\displaystyle{ \phi }[/math] 都存在不含量词的公式 [math]\displaystyle{ \psi }[/math] ，满足 [math]\displaystyle{ T\vDash (\forall v_0\cdots\forall v_n)(\phi\leftrightarrow\psi) }[/math] ，其中 [math]\displaystyle{ v_0\cdots v_n }[/math] 是其中的自由变元。
- 对 [math]\displaystyle{ T }[/math] 上的模型 [math]\displaystyle{ \mathfrak{A},\mathfrak{B},\mathfrak{C} }[/math] ，其中 [math]\displaystyle{ \mathfrak{A} }[/math] 是 [math]\displaystyle{ \mathfrak{B},\mathfrak{C} }[/math] 的子模型，则存在 [math]\displaystyle{ T }[/math] 的模型 [math]\displaystyle{ \mathfrak{D} }[/math] 使得 [math]\displaystyle{ \mathfrak{A} }[/math] 是 [math]\displaystyle{ \mathfrak{D} }[/math] 的子模型，且语言 [math]\displaystyle{ \mathcal{L}_A }[/math] 上的模型满足 [math]\displaystyle{ \mathfrak{B}_A\preceq\mathfrak{D}_A,\mathfrak{C}_A\preceq\mathfrak{D}_A }[/math] 。