查看“︁满足（谓词逻辑）”︁的源代码

[[分类:谓词逻辑]][[分类:模型论]]
{{InfoBox
|name=满足
|eng_name=satisfy
}}
一个[[赋值（谓词逻辑）|赋值]]'''满足'''('''satisfies''')一个[[谓词公式]]，指这个赋值使得这个公式被[[解释（谓词逻辑）|解释]]为真命题。换句话说，按照这个赋值把这个谓词公式中的[[个体词（谓词逻辑）|个体常项、个体变项]]、[[函项]]、[[谓词]]映射到论域中的个体对象及关系使其成为命题后，得到的命题是真命题。

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

== 定义 ==

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

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

{{CharMetaInfo
|char=&#x22A8;
|unicodeCodePoint={{UnicodeCodePoint|U+22A8|True, Is a Tautology, Satisfies, Results in}}
|latex=\vDash
}}


{{谓词逻辑}}
{{模型论}}