量词：修订间差异

2025年12月19日 (五) 14:01的版本

量词
术语名称	量词
英语名称	quantifier

辖域
术语名称	辖域
英语名称	scope

量化公式
术语名称	量化公式
英语名称	quantified formula

约束出现
术语名称	约束出现
英语名称	bound occurrence

自由出现
术语名称	自由出现
英语名称	free occurrence

量词(quantifier)是谓词逻辑中的核心语法单元，语法上与个体变项一同作用于一个含该个体变项的谓词公式，构成新的谓词公式。语义上，量词表达这一公式解释成的命题是关于论域中全部或部分对象的一般性陈述，即约束个体的数量，称为对其的量化(quantify)。

语法上，含有量词的表达式可以分为两部分。第一部分中，量词总是紧接一个个体变项，也就是被约束数量的个体词，如 [math]\displaystyle{ \forall x }[/math] 中的 [math]\displaystyle{ x }[/math] ；有时还会有限制取值的范围，称为量化域，如 [math]\displaystyle{ \forall x \in A }[/math] 中的 [math]\displaystyle{ A }[/math] 。这部分被共同称为量化表达式。第二部分是所限制的子公式，称为这个量词的辖域(scope)。量化表达式和辖域共同构成一个量化公式(quantified formula)。由于量化域部分可以转化为公式的一部分，对含有量化域的量化命题，命题逻辑部分一般不进行特殊讨论。

语义上，量词表达一个关于论域中全部对象或存在对象的陈述，因此分为两种：其中描述全部的称为全称量词 [math]\displaystyle{ \forall }[/math] ，描述存在的称为存在量词 [math]\displaystyle{ \exists }[/math] 。此外，命题中的唯一量词和计数量词等也分类为广义量词，由于其可以转化为含有以上两种量词的复合命题，命题逻辑部分一般不进行特殊讨论。在语义上，这些带有量词的命题称为量化命题(quantified proposition)。

形式上，在公式 [math]\displaystyle{ \phi }[/math] 中，若有个体变项 [math]\displaystyle{ x }[/math] ，则语法上对公式中的每个 [math]\displaystyle{ x }[/math] ：

在量词后（[math]\displaystyle{ \mathsf{Q}x }[/math] 中的 [math]\displaystyle{ x }[/math]）的称为作用变元。
否则称为 [math]\displaystyle{ x }[/math] 在 [math]\displaystyle{ \phi }[/math] 中的一次出现(occurrence)：
- 若 [math]\displaystyle{ x }[/math] 的一次出现在带有该个体变项的量化表达式（如 [math]\displaystyle{ \forall x }[/math] 或 [math]\displaystyle{ \exists }[/math]）辖域中，称这次出现本身是约束的(bound)，也称这次出现为 [math]\displaystyle{ x }[/math] 在 [math]\displaystyle{ \phi }[/math] 中的一次约束出现(bound occurrence)，称公式中的这个 [math]\displaystyle{ x }[/math] 为约束变元；
- 若不在这样的量化表达式的辖域中，称这次出现是自由的(free)，也称这次出现为 [math]\displaystyle{ x }[/math] 在 [math]\displaystyle{ \phi }[/math] 中的一个自由出现(free occurrence)，此时称公式中的这个 [math]\displaystyle{ x }[/math] 为自由变元。

注：“作用变元”、“约束变元”、“自由变元”虽然以“变元”结尾，但不代表对个体变元本身的分类，而是语法上对符号串中的每处个体变元符号的分类。

谓词逻辑/一阶逻辑
命题结构	项	个体词（个体常项、个体变项）、论域/个体域、函项、项、闭项
	谓词	谓词（谓词常项、谓词变项）
	量词	量词（辖域、出现）、全称量词 [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:liang4ci2}}
+{{#seo:
+|keywords=量词, 全称量词, 存在量词, 谓词逻辑, 量化
+|description=量词是谓词逻辑中表达“所有”或“存在”等量化概念的逻辑算子，主要包括全称量词∀和存在量词∃。它们是谓词逻辑区别于命题逻辑的核心特征，使逻辑能够表达一般性陈述和存在性陈述。
+|modified_time={{REVISIONYEAR}}-{{REVISIONMONTH}}-{{REVISIONDAY2}}
+|published_time=2023-07-01
+}}
 {{InfoBox
 |name=量词
@@ 第20行： / 第26行： @@
 |eng_name=free occurrence
 }}
-'''量词'''('''quantifier''')指[[命题]]中约束个体的数量的词汇，包括[[全称量词|全称量词 <math>\forall</math>]] 和[[存在量词|存在量词 <math>\exists</math>]] 。
+'''量词'''('''quantifier''')是谓词逻辑中的核心语法单元，语法上与[[个体词（谓词逻辑）|个体变项]]一同作用于一个含该个体变项的[[谓词公式]]，构成新的谓词公式。
+语义上，量词表达这一公式解释成的命题是关于论域中全部或部分对象的一般性陈述，即约束个体的数量，称为对其的'''量化'''('''quantify''')。
-量词总要紧接一个个体变项，也就是被约束数量的个体，如 <math>\forall x</math> 中的 <math>x</math> ；
+语法上，含有量词的表达式可以分为两部分。
-有时还会有限制取值的范围，称为量化域，如 <math>\forall x \in A</math> 中的 <math>A</math> 。
+第一部分中，量词总是紧接一个个体变项，也就是被约束数量的个体词，如 <math>\forall x</math> 中的 <math>x</math> ；
+有时还会有限制取值的范围，称为'''量化域'''，如 <math>\forall x \in A</math> 中的 <math>A</math> 。
 这部分被共同称为'''量化表达式'''。
+第二部分是所限制的子公式，称为这个量词的'''辖域'''('''scope''')。
+量化表达式和辖域共同构成一个'''量化公式'''('''quantified formula''')。
+由于量化域部分可以转化为公式的一部分，对含有量化域的量化命题，命题逻辑部分一般不进行特殊讨论。
+语义上，量词表达一个关于论域中全部对象或存在对象的陈述，因此分为两种：其中描述全部的称为[[全称量词|全称量词 <math>\forall</math>]] ，描述存在的称为[[存在量词|存在量词 <math>\exists</math>]] 。
+此外，命题中的[[唯一量词]]和[[计数量词]]等也分类为'''广义量词'''，由于其可以转化为含有以上两种量词的复合命题，命题逻辑部分一般不进行特殊讨论。
+在语义上，这些带有量词的命题称为'''量化命题'''('''quantified proposition''')。
-量化表达式和所限制的公式构成'''量化公式'''('''quantified formula''')，其中被限制的公式称为这个量词的'''辖域'''('''scope''')。
+形式上，在公式 <math>\phi</math> 中，若有个体变项 <math>x</math> ，则语法上对公式中的每个 <math>x</math> ：
+* 在量词后（<math>\mathsf{Q}x</math> 中的 <math>x</math>）的称为'''作用变元'''。
+* 否则称为 <math>x</math> 在 <math>\phi</math> 中的一次'''出现'''('''occurrence''')：
+** 若 <math>x</math> 的一次出现在带有该个体变项的量化表达式（如 <math>\forall x</math> 或 <math>\exists</math>）辖域中，称这次出现本身是'''约束'''的('''bound''')，也称这次出现为 <math>x</math> 在 <math>\phi</math> 中的一次'''约束出现'''('''bound occurrence''')，称公式中的这个 <math>x</math> 为'''约束变元'''；
+** 若不在这样的量化表达式的辖域中，称这次出现是'''自由'''的('''free''')，也称这次出现为 <math>x</math> 在 <math>\phi</math> 中的一个'''自由出现'''('''free occurrence''')，此时称公式中的这个 <math>x</math> 为'''自由变元'''。
-在公式 <math>\phi</math> 中，有个体变项 <math>x</math> ，对其每次出现(occurrence)：
+注：“作用变元”、“约束变元”、“自由变元”虽然以“变元”结尾，但不代表对个体变元本身的分类，而是语法上对符号串中的每处个体变元符号的分类。
-* 直接出现在量词后的称为'''作用变元'''，不视为出现。
-* 若 <math>x</math> 的出现是在带有该个体变项的量化表达式（如 <math>\forall x</math> 或 <math>\exists</math>）辖域中，称为 <math>x</math> 在 <math>\phi</math> 中的一次'''约束出现'''('''bound occurrence''')，此时称其为'''约束变元'''；
-* 若不在这样的量化表达式的辖域中，称为 <math>x</math> 在 <math>\phi</math> 中的一个'''自由出现'''('''free occurrence''')，此时称其为'''自由变元'''。
 {{谓词逻辑}}