计数量词

来自GSXAB的知识库
数量词
术语名称 数量词
英语名称 numerical quantifier
别名 numeric quantifier, counting quantifier

请注意,这个条目所介绍的术语没有标准称呼。仅仅是为了便于描述建立条目取了一个名字。

数量词(numerical quantifier)是量词的一种,包括相当于自然语言中的“有(恰好、至多、至少) [math]\displaystyle{ N }[/math] 个不同的……满足……”。

定义

命题中,表达“存在恰好 [math]\displaystyle{ N }[/math] 个不同的……使得……”的含义的量词,记作 [math]\displaystyle{ \exists^{=N} }[/math] ; 表达“存在至多 [math]\displaystyle{ N }[/math] 个不同的……使得……”的含义的量词,记作 [math]\displaystyle{ \exists^{\leq N} }[/math] ; 表达“存在至少 [math]\displaystyle{ N }[/math] 个不同的……使得……”的含义的量词,记作 [math]\displaystyle{ \exists^{\geq N} }[/math]

比如,对 [math]\displaystyle{ P(x) }[/math]

  • 命题“存在恰好两个 [math]\displaystyle{ x }[/math] 的不同图片某个取值,使得所构成的命题是真命题”,记作 [math]\displaystyle{ \exists^{=2} x P(x) }[/math]
  • 命题“存在至多两个 [math]\displaystyle{ x }[/math] 的不同图片某个取值,使得所构成的命题是真命题”,记作 [math]\displaystyle{ \exists^{\leq 2} x P(x) }[/math]
  • 命题“存在至少两个 [math]\displaystyle{ x }[/math] 的不同图片某个取值,使得所构成的命题是真命题”,记作 [math]\displaystyle{ \exists^{\geq 2} x P(x) }[/math]

常用量词表示

计数量词不是常用量词,可以按以下方式表达为常用量词:

[math]\displaystyle{ \exist^{\geq N} x P(x) }[/math] 可以被表达为 [math]\displaystyle{ \exist x_1 \dots \exists x_N \left( \left( \bigwedge_{\begin{split}1\leq &k \lt N \\ k \lt &l \leq N\end{split}} x_k \neq x_l \right) \land \left( \bigwedge_{1 \leq k \leq N} P(x_k) \right) \right) }[/math] ,即存在 [math]\displaystyle{ N }[/math] 个个体对象两两不同且同时均满足谓词。

[math]\displaystyle{ \exist^{\leq N} x P(x) }[/math] 可以被表达为 [math]\displaystyle{ \forall x_1 \dots \forall x_{N+1} \left( \left( \bigwedge_{1 \leq k \leq N+1} P(x_k) \right) \rightarrow \left( \bigvee_{\begin{split}1\leq &k \leq N \\ k \lt &l \leq N+1\end{split}} x_k = x_l \right) \right) }[/math] ,即对任意 [math]\displaystyle{ (N+1) }[/math] 个个体对象若均满足谓词则至少有两个相同。

[math]\displaystyle{ \exist^{= N} x P(x) }[/math] 则可以等价地重新表达成 [math]\displaystyle{ \exist^{\geq N} x P(x) \land \exist^{\leq N} x P(x) }[/math] ,因此可以用以上两个式子的合取表示。


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