查看“︁量词”︁的源代码

[[分类:谓词逻辑]]
{{InfoBox
|name=量词
|eng_name=quantifier
}}
{{InfoBox
|name=辖域
|eng_name=scope
}}
{{InfoBox
|name=量化公式
|eng_name=quantified formula
}}
{{InfoBox
|name=约束出现
|eng_name=bound occurrence
}}
{{InfoBox
|name=自由出现
|eng_name=free occurrence
}}
'''量词'''('''quantifier''')指[[命题]]中约束个体的数量的词汇，包括[[全称量词|全称量词 <math>\forall</math>]] 和[[存在量词|存在量词 <math>\exists</math>]] 。

量词总要紧接一个个体变项，也就是被约束数量的个体，如 <math>\forall x</math> 中的 <math>x</math> ；
有时还会有限制取值的范围，称为量化域，如 <math>\forall x \in A</math> 中的 <math>A</math> 。
这部分被共同称为'''量化表达式'''。

量化表达式和所限制的公式构成'''量化公式'''('''quantified formula''')，其中被限制的公式称为这个量词的'''辖域'''('''scope''')。

在公式 <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''')，此时称其为'''自由变元'''。


{{谓词逻辑}}