量词

来自GSXAB的知识库
量词
术语名称 量词
英语名称 quantifier
辖域
术语名称 辖域
英语名称 scope
量化公式
术语名称 量化公式
英语名称 quantified formula
约束出现
术语名称 约束出现
英语名称 bound occurrence
自由出现
术语名称 自由出现
英语名称 free occurrence

量词(quantifier)指命题中约束个体的数量的词汇,包括全称量词[math]\displaystyle{ \forall }[/math]存在量词[math]\displaystyle{ \exists }[/math]

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

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

在公式 [math]\displaystyle{ \phi }[/math] 中,有个体变项 [math]\displaystyle{ x }[/math] ,对其每次出现(occurrence):

  • 直接出现在量词后的称为作用变元,不视为出现。
  • [math]\displaystyle{ x }[/math] 的出现是在带有该个体变项的量化表达式(如 [math]\displaystyle{ \forall x }[/math][math]\displaystyle{ \exists }[/math])辖域中,称为 [math]\displaystyle{ x }[/math][math]\displaystyle{ \phi }[/math] 中的一次约束出现(bound occurrence),此时称其为约束变元
  • 若不在这样的量化表达式的辖域中,称为 [math]\displaystyle{ x }[/math][math]\displaystyle{ \phi }[/math] 中的一个自由出现(free occurrence),此时称其为自由变元


谓词逻辑/一阶逻辑
命题结构 个体词(个体常项、个体变项)、个体域、函项、项谓词(谓词常项、谓词变项)
量词(辖域、出现)全称量词 [math]\displaystyle{ \forall }[/math]存在量词 [math]\displaystyle{ \exists }[/math]
谓词公式 解释/模型赋值
分类 普遍有效公式、可满足式、不可满足式
范式 前束范式Skolem 范式