满足（谓词逻辑）

满足
术语名称	满足
英语名称	satisfy

一个赋值满足(satisfies)一个谓词公式，指这个赋值使得这个公式被解释为真命题。换句话说，按照这个赋值把这个谓词公式中的个体常项、个体变项、函项、谓词映射到论域中的个体对象及关系使其成为命题后，得到的命题是真命题。

赋值满足公式集中的每个公式时，也说赋值满足这个公式集。一个结构上的任意赋值均满足公式或公式集，也就是对个体变项的任意映射，只固定个体常项、函项、谓词的像时，仍然保持得到真命题，称这个结构满足这个公式或公式集，此时称这个公式或公式集为一个理论，这个结构为这个理论的一个模型。

定义

对谓词公式 [math]\displaystyle{ \phi }[/math] 及模型 [math]\displaystyle{ \mathfrak{I} }[/math] 上的赋值 [math]\displaystyle{ \sigma }[/math] ，若公式在赋值后的命题 [math]\displaystyle{ \phi^\sigma }[/math] 为真命题，则称赋值 [math]\displaystyle{ \sigma }[/math] 满足(satisfies)公式 [math]\displaystyle{ \phi }[/math] ，记作 [math]\displaystyle{ \sigma \vDash \phi }[/math] 。

若对公式集 [math]\displaystyle{ \Gamma }[/math] 及模型 [math]\displaystyle{ \mathfrak{I} }[/math] 上的赋值 [math]\displaystyle{ \sigma }[/math] ，对 [math]\displaystyle{ \Gamma }[/math] 中任意公式 [math]\displaystyle{ \phi }[/math] 都有 [math]\displaystyle{ \sigma \vDash \phi }[/math] ，则说赋值 [math]\displaystyle{ \sigma }[/math] 满足公式集 [math]\displaystyle{ \Gamma }[/math] ，记为 [math]\displaystyle{ \sigma \vDash \Gamma }[/math] 。
若对公式 [math]\displaystyle{ \phi }[/math] 及模型 [math]\displaystyle{ \mathfrak{I} }[/math] ，对 [math]\displaystyle{ \mathfrak{I} }[/math] 上任意赋值 [math]\displaystyle{ \sigma }[/math] 都有 [math]\displaystyle{ \sigma \vDash \phi }[/math] ，则说模型 [math]\displaystyle{ \mathfrak{I} }[/math] 满足公式 [math]\displaystyle{ \phi }[/math] ，记为 [math]\displaystyle{ \mathfrak{I} \vDash \phi }[/math] 。
类似地定义 [math]\displaystyle{ \mathfrak{I} \vDash \Gamma }[/math] 。

⊨
字符	⊨
Unicode码位	`U+22A8` True, Is a Tautology, Satisfies, Results in
Latex命令序列	`\vDash`

谓词逻辑/一阶逻辑
命题结构	项	个体词（个体常项、个体变项）、论域/个体域、函项、项、闭项
	谓词	谓词（谓词常项、谓词变项）
	量词	量词（辖域、出现）、全称量词 [math]\displaystyle{ \forall }[/math] 、存在量词 [math]\displaystyle{ \exists }[/math]
谓词公式	形式定义	谓词语言 [math]\displaystyle{ \mathcal{L}^* }[/math] 、谓词公式、闭式
	逻辑语义	结构、指派/赋值、基本语义定义、解释、满足、模型
	语义分类	普遍有效公式、可满足式、不可满足式
	语义关系	逻辑等值/逻辑等价 [math]\displaystyle{ = }[/math]/[math]\displaystyle{ \Leftrightarrow }[/math] 、逻辑蕴涵 [math]\displaystyle{ \Rightarrow }[/math]
	范式	前束范式、 Skolem 范式
	个体变项代入	可自由代入、易字、简单易字变形、易字变形
	命题变元代入	置换定理

模型论
研究对象	理论和模型	形式语言 [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 测试
理论是否确定模型结构完备——理论的模型完备性理论
模型完备性		理论的模型完备性	理论的子模型完备性	理论的模型完备化