一阶谓词逻辑

一阶逻辑命题符号化

客体

• 客体：客观存在的实体，如人、物、事物等。
• 个体词：所研究对象中独立存在的客体。
  • 个体常项：具体的事物，用 $a$ 、 $b$ 、 $c$ 等表示 。
  • 个体变项：抽象的事物，用 $x$ 、 $y$ 、 $z$ 等表示。
• 个体域：个体变项的取值范围。
  • 有限个体域：如 $\{a,b,c\}$，$\{1,2\}$ 等。
  • 无限个体域：如全体自然数 $\mathbb{N}$，全体实数 $\mathbb{R}$ 等。
  • 全总个体域：由宇宙间一切事物组成的个体域。

谓词

• 谓词：对客体的性质、特征、关系等进行描述的符号。常用大写字母表示，如 $P$ 、 $Q$ 、 $R$ 等。 例如 $A(x)$ 表示 $x$ 满足性质 $A$。
  • 谓词常项：如，$F(a):a$ 是男性。
  • 谓词变项：如，$F(x):x$ 是男性。
  • $n$ 元谓词：含有 $n$ 个变项的谓词。
    • 一元谓词：表示一个客体的性质。
    • 多元谓词：表示多个客体之间的关系。
    • 零元谓词：不含个体变项的谓词，即命题常项或命题变项。

量词

$\mathrm{\forall }$ 和 $\mathrm{\exists }$ 称为量词。

• 全称量词：$\mathrm{\forall }$，表示“对任意”、“对一切”。
• 存在量词：$\mathrm{\exists }$，表示“存在”、“至少有一个”。 如 $\mathrm{\forall }xP(x)$ 表示“对任意 $x$，$x$ 满足性质 $P$”。

对于 $\mathrm{\forall }$ 用 $\to$ 而不是 $\wedge$ 对于 $\mathrm{\exists }$ 用 $\wedge$ 而不是 $\to$

变元的约束

在公式 $\mathrm{\forall }xA$ 和 $\mathrm{\exists }xA$ 中，$x$ 称为指导变元，$A$ 为对应量词的 辖域。 在辖域内，$x$ 称为约束出现，$A$ 中不是约束出现的其他变项称为自由出现。 若 $A$ 中没有自由出现的变项，则称 $A$ 为闭式。

公式的解释

若公式在任何解释和该解释下的任何赋值下都为真，则称该公式为永真式。 若公式在任何解释和该解释下的任何赋值下都为假，则称该公式为永假式。 若公式在某个解释和该解释下的某个赋值下为真，则称该公式为可满足式。

一阶逻辑公式是不可判定的，即无法判断一个公式是否永真、永假或可满足。

代换实例

设 $A_0$ 是含命题变项 $p_1,p_2,\dots ,p_n$ 的命题公式，$A_1,A_2,\dots ,A_n$ 是 $n$ 个谓词公式，用 $A_i$ ($1\le i\le n$) 处处代替 $A_0$ 中的 $p_i$，所得公式 $A$ 称为 $A_0$ 的代换实例。

例如，$F(x)\to G(x)$，$\mathrm{\forall }xF(x)\to \mathrm{\exists }yG(y)$ 等都是 $p\to q$ 的代换实例。

重言式的代换实例都是永真式，矛盾式的代换实例都是矛盾式。

一阶逻辑的等值演算与推理

基本等值式

命题逻辑的基本等值式

基本等值式在一阶逻辑中仍然成立，如双重否定律、德摩根律等。需要代换实例。

量词的等值式

消去量词等值式

设 $D=\{a_1,a_2,\dots ,a_n\}$

1. $\mathrm{\forall }xA(x)\iff A(a_1)\wedge A(a_2)\wedge \cdots \wedge A(a_n)$
2. $\mathrm{\exists }xA(x)\iff A(a_1)\vee A(a_2)\vee \cdots \vee A(a_n)$

量词否定等值式

1. $\mathrm{\neg }\mathrm{\forall }xA(x)\iff \mathrm{\exists }x\mathrm{\neg }A(x)$
2. $\mathrm{\neg }\mathrm{\exists }xA(x)\iff \mathrm{\forall }x\mathrm{\neg }A(x)$

量词辖域收缩与扩张等值式

$A(x)$ 是含 $x$ 的自由出现的公式，$B$ 中不含 $x$ 的自由出现的公式。

• 关于全称量词的：

  • $\mathrm{\forall }x(A(x)\wedge B)\iff \mathrm{\forall }xA(x)\wedge B$
  • $\mathrm{\forall }x(A(x)\vee B)\iff \mathrm{\forall }xA(x)\vee B$
  • $\mathrm{\forall }x(A(x)\to B)\iff \mathrm{\exists }xA(x)\to B$
  • $\mathrm{\forall }x(B\to A(x))\iff B\to \mathrm{\forall }xA(x)$

• 关于存在量词的：

  • $\mathrm{\exists }x(A(x)\wedge B)\iff \mathrm{\exists }xA(x)\wedge B$
  • $\mathrm{\exists }x(A(x)\vee B)\iff \mathrm{\exists }xA(x)\vee B$
  • $\mathrm{\exists }x(A(x)\to B)\iff \mathrm{\forall }xA(x)\to B$
  • $\mathrm{\exists }x(B\to A(x))\iff B\to \mathrm{\exists }xA(x)$

量词分配等值式

• $\mathrm{\forall }x(A(x)\wedge B(x))\iff \mathrm{\forall }xA(x)\wedge \mathrm{\forall }xB(x)$
• $\mathrm{\exists }x(A(x)\vee B(x))\iff \mathrm{\exists }xA(x)\vee \mathrm{\exists }xB(x)$
• $\mathrm{\exists }x(A(x)\to B(x))\iff \mathrm{\forall }xA(x)\to \mathrm{\exists }xB(x)$

形式类似的重演蕴含式

• $\mathrm{\forall }x(A(x)\vee B(x))\Leftarrow \mathrm{\forall }xA(x)\vee \mathrm{\forall }xB(x)$
• $\mathrm{\exists }x(A(x)\wedge B(x))\Rightarrow \mathrm{\exists }xA(x)\wedge \mathrm{\exists }xB(x)$
• $$\begin{array}{rl}\mathrm{\exists }xA(x)\to \mathrm{\forall }xB(x)& \Rightarrow \mathrm{\forall }x(A(x)\to B(x))\\ \Rightarrow \mathrm{\forall }xA(x)\to \mathrm{\forall }xB(x)& \Rightarrow \mathrm{\exists }xA(x)\to \mathrm{\exists }xB(x)\end{array}$$

置换规则、换名规则、代替规则

置换规则

若 $A\iff B$ 则 $F(A)\iff F(B)$

换名规则

将公式 $A$ 中某量词辖域内的所有约束变元替换为该辖域中未出现的个体变项符号，得到的公式 $A^{\prime }$ 与 $A$ 等值。

代替规则

设 $A$ 为一公式，将 $A$ 中的某个自由出现的变项用未曾出现在 $A$ 中的个体常项符号代替，得到的公式 $A^{\prime }$ 与 $A$ 等值。

一阶逻辑前束范式

设 $A$ 为一阶逻辑公式，若 $A$ 的量词部分出现在公式的最前面，则称 $A$ 为前束范式。即 $A$ 可以表示为：

$$Q_1{x}_1{Q}_2{x}_2\cdots Q_n{x}_{n}B$$

其中 $Q_i$ 为量词，$x_i$ 为变项，$B$ 为不含量词的公式。

一阶逻辑中的任何公式都存在与之等值的前束范式

一阶逻辑的推理理论

量词规则

1. US：全称引入规则（Universal Specification）$$\mathrm{\forall }xA(x)\Rightarrow A(c)$$
2. UG：全称推广规则（Universal Generalization）$$A(c)\Rightarrow \mathrm{\forall }xA(x)$$
3. ES：存在引入规则（Existential Specification）$$A(c)\Rightarrow \mathrm{\exists }xA(x)$$
4. EG：存在推广规则（Existential Generalization）$$\mathrm{\exists }xA(x)\Rightarrow A(c)$$

自然推理系统

定义5.3 自然推理系统 $N_{\mathcal{L}}$ 定义如下：

1. 字母表：同一阶语言 $\mathcal{L}$ 的字母表。
2. 合式公式：同 $\mathcal{L}$ 的合式公式。
3. 推理规则：基本等值式、量词规则。