谓词公式分类：修订间差异

2025年12月27日 (六) 13:02的版本

有效式
术语名称	有效式
英语名称	effective formula

不可满足式
术语名称	不可满足式
英语名称	unsatisfiable formula

可满足式
术语名称	可满足式
英语名称	satisfiable formula

根据谓词公式在全部解释（结构和赋值）下的真值，可以将谓词公式分为有效式(effective formula)、仅可满足式、不可满足式(unsatisfiable formula)几类。

分类

有效式

有效式(effective formula)指任何赋值下，一个谓词公式 [math]\displaystyle{ \phi }[/math] 的真值都为真。此时任意赋值都满足这一谓词公式 [math]\displaystyle{ \phi }[/math] ，记作 [math]\displaystyle{ \vDash \phi }[/math] 。

仅可满足式

仅可满足式指在所有赋值下，一个谓词公式的真值在有些赋值下为真，在有些赋值下为假。

不可满足式

不可满足式(unsatisfiable formula)指任何赋值下，一个谓词公式 [math]\displaystyle{ \phi }[/math] 的真值都为假。此时任意赋值都满足这一谓词公式的否定 [math]\displaystyle{ \lnot\phi }[/math] ，即 [math]\displaystyle{ \vDash \lnot\phi }[/math] 。

可满足式

有效式和仅可满足式，可以总称为一个谓词公式存在有的真值使其为真，此时称谓词公式可满足(satisfiable)，合称为可满足式(satisfiable formaula)。

谓词逻辑/一阶逻辑
命题结构	项	个体词（个体常项、个体变项）、论域/个体域、函项、项、闭项
	谓词	谓词（谓词常项、谓词变项）
	量词	量词（辖域、出现）、全称量词 [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 范式
	个体变项代入	可自由代入、易字、简单易字变形、易字变形
	命题变元代入	置换定理

@@ 第1行： / 第1行： @@
-[[分类:谓词逻辑]]
+[[分类:谓词逻辑]]{{DEFAULTSORT:wei4ci2gong1shi4fen1lei4}}
+{{#seo:
+|keywords=有效式, 仅可满足式, 可满足式, 不可满足式
+|description=本文介绍谓词公式的分类方法，包括重言式、矛盾式和偶然式的定义，以及可满足式、不可满足式这一根据可满足性的分类方式。
+|modified_time={{REVISIONYEAR}}-{{REVISIONMONTH}}-{{REVISIONDAY2}}
+|published_time=2023-07-01
+}}
 {{InfoBox
 |name=有效式
@@ 第12行： / 第18行： @@
 |eng_name=satisfiable formula
 }}
+根据[[谓词公式]]在全部[[解释（谓词逻辑）|解释]]（[[结构（谓词逻辑）|结构]]和[[赋值（谓词逻辑）|赋值]]）下的[[真值]]，可以将谓词公式分为'''有效式'''('''effective formula''')、'''仅可满足式'''、'''不可满足式'''('''unsatisfiable formula''')几类。
+== 分类 ==
+=== 有效式 ===
+'''有效式'''('''effective formula''')指任何赋值下，一个谓词公式 <math>\phi</math> 的真值都为真。此时任意[[赋值（谓词逻辑）|赋值]]都[[满足（谓词逻辑）|满足]]这一谓词公式 <math>\phi</math> ，记作 <math>\vDash \phi</math> 。
+=== 仅可满足式 ===
+'''仅可满足式'''指在所有赋值下，一个谓词公式的真值在有些赋值下为真，在有些赋值下为假。
+=== 不可满足式 ===
+'''不可满足式'''('''unsatisfiable formula''')指任何赋值下，一个谓词公式 <math>\phi</math> 的真值都为假。此时任意[[赋值（谓词逻辑）|赋值]]都[[满足（谓词逻辑）|满足]]这一谓词公式的否定 <math>\lnot\phi</math> ，即 <math>\vDash \lnot\phi</math> 。
-根据[[谓词公式]]在全部[[解释（谓词逻辑）|解释]]和[[赋值（谓词逻辑）|赋值]]下的[[真值]]，可以将谓词公式分为以下几类。
+=== 可满足式 ===
-* '''有效式'''('''effective formula''')：任何赋值下，谓词公式的真值都为真。即，任意[[赋值（谓词逻辑）|赋值]]都[[满足（谓词逻辑）|满足]]这一谓词公式 <math>\phi</math> ，记作 <math>\vDash \phi</math> 。
-* '''仅可满足式'''：谓词公式有些赋值为真，有些赋值下为假。
-* '''不可满足式'''('''unsatisfiable formula''')：任何赋值下，谓词公式的真值都为假。即，任意[[赋值（谓词逻辑）|赋值]]都[[满足（谓词逻辑）|满足]]这一谓词公式的否定 <math>\lnot\phi</math> ，即 <math>\vDash \lnot\phi</math> 。
-此外，前两者也称谓词公式是否'''可满足'''('''satisfiable''')，为'''可满足式'''。
+有效式和仅可满足式，可以总称为一个谓词公式存在有的真值使其为真，此时称谓词公式'''可满足'''('''satisfiable''')，合称为'''可满足式'''('''satisfiable formaula''')。
 {{谓词逻辑}}