可满足性(理论)
外观
| 可满足性 | |
|---|---|
| 术语名称 | 可满足性 |
| 英语名称 | satisfiability |
| 别名 | 语义一致性, semantic consistency |
| 可满足 | |
|---|---|
| 术语名称 | 可满足 |
| 英语名称 | satisfiable |
| 别名 | 语义一致的, semanticly consistent |
一个语言的可满足(satisfiable)理论,指在该语言中存在一个模型满足这个理论,或者说该语言中存在一个该理论的模型,也称为这个理论是语义一致的(semanticly consistent)。
定义
对语言 [math]\displaystyle{ \mathcal{L} }[/math] 中的一个理论 [math]\displaystyle{ T }[/math] ,若存在 [math]\displaystyle{ T }[/math] 的一个模型 [math]\displaystyle{ \mathfrak{M} }[/math] ,即存在 [math]\displaystyle{ \mathcal{L} }[/math] 的一个模型 [math]\displaystyle{ \mathfrak{M} }[/math] 有 [math]\displaystyle{ \mathfrak{M}\vDash T }[/math] ,则称理论 [math]\displaystyle{ T }[/math] 是可满足的(satisfiable),或理论 [math]\displaystyle{ T }[/math] 具有可满足性(satisfiability)。
| 模型论 | ||||
|---|---|---|---|---|
| 研究对象 | 理论和模型 | 形式语言 [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 测试 | |||
| 理论是否确定模型结构完备——理论的模型完备性理论 | ||||
| 模型完备性 | 理论的模型完备性 | 理论的子模型完备性 | 理论的模型完备化 | |