谓词逻辑

在逻辑学中, 谓词逻辑是在命题逻辑的基础上加入量词得到的逻辑, 量词包括全称和存在两个逻辑连接词.

根据量词的强大程度, 谓词逻辑可以进一步被分类为一阶逻辑、二阶逻辑乃至高阶逻辑等. Russell 简单类型论是一种高阶逻辑的例子.

推导规则

主条目: 推导规则

下文中, 相继式记作 $\Gamma ⊢\phi$, 其中 $\Gamma$ 是命题的集合, 代表语境, $\phi$、$\chi$ 等符号表示单个命题. 为了可读性, 将类似 $\Gamma \cup \{\phi \}$ 等拼接语境的集合操作全部用 $\Gamma ,\phi$ 这样的用逗号分隔的写法表示.

•	全称概括: 如果 $x$ 不是 $\Gamma$ 中公式的自由变元, 则: $$\frac{\Gamma ⊢\chi }{\Gamma ⊢\forall x.\chi }$$

•	全称列举: $$\frac{\Gamma ⊢\forall x.\chi }{\Gamma ⊢\chi [x\mapsto t]}$$

•	存在概括: $$\frac{\Gamma ⊢\chi [x\mapsto t]}{\Gamma ⊢\exists x.\chi }$$

•	存在列举: 如果 $x$ 不是 $\Gamma ,\chi$ 中公式的自由变元, 则: $$\frac{\Gamma ⊢\exists x.\phi \Gamma ,\phi ⊢\chi }{\Gamma ⊢\chi }$$

术语翻译

谓词逻辑 • 英文 predicate logic

谓词 • 英文 predicate • 德文 Prädikat (n) • 法文 prédicat (m) • 拉丁文 praedicatum (n) • 古希腊文 κατηγότημα (n)

量词 • 英文 quantifier • 德文 Quantor (m) • 法文 quantificateur (m) • 拉丁文 quantificator (m) • 古希腊文 ποσοδείκτης (m)