跳转到内容

Advertising:

满足（谓词逻辑）：修订间差异

来自GSXAB的知识库
下一编辑→
Gsxab​（留言 | 贡献）
6,428次编辑
无编辑摘要
 
Gsxab​（留言 | 贡献）
6,428次编辑
无编辑摘要
第4行： 第4行：
|eng_name=satisfy
|eng_name=satisfy
}}
}}
一个[[赋值（谓词逻辑）|赋值]]'''满足'''('''satisfies''')一个[[谓词公式]]，指赋值使得这个公式变成真命题。
一个[[赋值（谓词逻辑）|赋值]]'''满足'''('''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>\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>\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>\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> 。
* 类似地定义 <math>\mathfrak{I} \vDash \Gamma</math> 。


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


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

2025年12月25日 (四) 07:17的版本

满足
术语名称 满足
英语名称 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 范式
个体变项代入 可自由代入、易字、简单易字变形、易字变形
命题变元代入 置换定理

模板:模型论

检索自“https://knowledge.gsxab.top/index.php?title=满足（谓词逻辑）&oldid=6365”

Advertising: