量词
| 量词 | |
|---|---|
| 术语名称 | 量词 |
| 英语名称 | 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{ \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] 为约束变项/约束变元(bound variable)；
- 若不在这样的量化表达式的辖域中，称这次出现是自由的(free)，也称这次出现为 [math]\displaystyle{ x }[/math] 在 [math]\displaystyle{ \phi }[/math] 中的一个自由出现(free occurrence)，此时称公式中的这个 [math]\displaystyle{ x }[/math] 为自由变项/自由变元(free variable)。
注：
- “作用变项”不是标准术语。有的分类中将其称为“绑定变项”“绑定出现(binding occurrence)”。
- “作用变项”、“约束变项”、“自由变项”虽然以“变项”结尾，但不是关于某个个体变项本身的，而是关于符号串中的符号的。比如符号串 [math]\displaystyle{ p(x)\land\forall x q(x) }[/math] 中，不能分类个体变项 [math]\displaystyle{ x }[/math] 为某个分类，而是把分别出现在第 3 、 7 、 10 个位置的三个符号“[math]\displaystyle{ x }[/math]”各分类为自由变项、作用变项和约束变项。
常见量词
语义上，量词表达一个关于论域中全部对象或存在对象的陈述，因此分为两种：其中描述全部的称为全称量词 [math]\displaystyle{ \forall }[/math] ，描述存在的称为存在量词 [math]\displaystyle{ \exists }[/math] 。 此外，命题中的唯一量词和计数量词等也分类为广义量词，由于其可以转化为含有以上两种量词的复合命题，命题逻辑部分一般不进行特殊讨论。 在语义上，这些带有量词的命题称为量化命题(quantified proposition)。