数理逻辑 (1) 命题逻辑

Abstract. 命题逻辑相关的内容，跳过了众所周知的内容，写一些以前没见过的。

第一节主要从语义角度讨论命题逻辑的等值和推理，第二节从语法角度讨论命题逻辑的公理系统，以完备性（和可靠性，但是这里没写）作为连接两者的桥梁。在开头简单阐释一下语义和语法的概念：语义意义下任何等值的变换都可以接受，语法意义下只有变换规则给出的变换可以接受。

参考资料是 thu 的数理逻辑与集合论教材。

• 命题逻辑的等值和推理
  • 命题公式与真值表的关系
    • 主析取范式
  • 联结词的完备集
  • 对偶式
  • 推理
    • 重言蕴含
    • 推理演算
    • 归结推理法（Resolution）
• 命题逻辑的公理化
  • 完备性证明
  • 自然演绎系统

命题逻辑的等值和推理

本章默认命题变项只有两种取值。

命题公式与真值表的关系

给定命题公式可以写出真值表，这是显然的。

给定 $P_1, …, P_n$ 到 $A$ 的真值表，可以写出一个和 $A$ 等价的命题公式，两种方法基于如下显然的操作：

取 $F_1(P_n)\wedge \cdots \wedge F_n(P_n)$，其中 $F_i(P)$ 为 $P$ 或者 $\neg P$，可以提取 $P_1, …, P_n$ 是否依次取 $T$（若 $F_i(P_i) = P_i$）和 $F$（若 $F_i(P_i) = \neg P_i$）。

那么将所有为 $T$ 的行用上述式子提取，然后析取起来即可得到和 $A$ 等价的命题公式；将所有为 $F$ 的行用上述式子提取，然后析取起来即可得到和 $\neg A$ 等价的命题公式。

主析取范式

事实上这个公式称为“主范式”，其中按 $T$ 列写得到的称为主析取范式，按 $F$ 列写的，取反用 De Morgan 将 $\neg$ 分配至每一项得到的称为主合取范式。接下来我们给出主析取范式的严格定义。

对于命题变项 $P_1, …, P_n$，定义 $Q_i = P_i \text{ 或 } \neg P_i$，称为文字。定义全部的 $n$ 个文字组成的合取式

$$
Q_1 \wedge \cdots \wedge Q_n
$$

为极小项。称仅有极小项构成的析取式为主析取范式。

我们将每个文字是否取 $\neg$ 记为 $0/1$，那么每个极小式可以表示成一个二进制数 $x$，这个极小式简记为 $m_x$，主析取范式可以简记为 $\vee_{i_1, …, i_k}$

Theorem. 任意公式有唯一主析取范式。

可以用真值表法来列写。

主范式的改写方法，以及简记方法 将 $P\rightarrow Q$ 改写为主范式。

Solution.

$$
\begin{aligned}
&P \rightarrow Q \\
=& \neg P \vee Q \\
=& (\neg P \wedge (Q \vee \neg Q)) \vee (Q \wedge (P \vee \neg P)) \\
=& (\neg P \wedge Q) \vee (\neg P \wedge \neg Q) \vee (P \wedge Q) \vee (\neg P \wedge Q) \\
=& (\neg P \wedge Q) \vee (\neg P \wedge \neg Q) \vee (P \wedge Q) \\
=& m_1 \vee m_0 \vee m_3 \\
=& \vee_{0, 1, 3}
\end{aligned}
$$

对于主合取范式，我们对称地定义极大项等，这里不多赘述。

主合取范式和主析取范式之间可以相互转化。从由真值表列写主范式的方法可以看出：

$$
\wedge_{i_1, …, i_k} = \vee_{\{0, …, 2^n - 1\} \setminus \{2^n - 1 - i_1, …, 2^n - 1 - i_k\}}
$$

联结词的完备集

Definition. 设 $C$ 为一联结词的集合，若任意命题公式都有一 $C$ 中联结词表示的公式与之等值，则称 $C$ 完备。

Theorem. $\{\neg, \wedge, \vee\}$ 完备。

Proof.

将逻辑公式写成真值表，然后给定真值表可以只用 $\{\neg, \wedge, \vee\}$ 写出逻辑公式（上一节结论）。$\square$

进一步根据摩根律 $P \vee Q = \neg (\neg P\wedge \neg Q)$ 等，$\{\neg, \wedge\}$ 和 $\{\neg, \vee\}$ 也完备。

对偶式

Definition 1. 设 $A$ 为一用 $\vee, \wedge, \neg$ 写成的命题公式，将 $A$ 中 $\vee$ 和 $\wedge$ 互换，$T, F$ 互换，得到的式子记为 $A^*$，称为对偶式。

Definition 2. 若 $A = A(P_1, …, P_n)$，那么记 $A^- = A(\neg P_1, …, \neg P_n)$。

Theorem 1. $\neg (A^*) = (\neg A)^*, \neg (A^-) = (\neg A)^-$.

Theorem 2. $(A^*)^* = A, (A^-)^- = (\neg A)^-$.

Theorem 3. $\neg A = A^{*-}$. 这个其实是 De Morgan 定理的通式。

Proof(Sketch).

对逻辑联结词个数归纳，因为众所周知逻辑公式是可以归纳构造的。

对于单变量显然成立，接下来以 Theorem 1，前半句为例

若 $A = \neg A_1$，那么

$$
\begin{aligned}
\neg (A^*) &= \neg (\neg A_1)^* \\
&= \neg \neg (A_1^*) & (\text{sym Theorem $1$}) \\
&= A_1^* \\
&= (\neg A)^*
\end{aligned}
$$

突然有一瞬间感觉这东西循环论证了，但是好像实际上没有。

若 $A = P\vee Q$，那么

$$
\begin{aligned}
\neg (A^*) &= \neg ((P \vee Q)^*) \\
&= \neg (P^* \wedge Q^*) \\
&= (\neg P^*) \vee (\neg Q^*) & (\text{De Morgan}) \\
&= (\neg P)^* \vee (\neg Q^*) & (\text{sym Theorem $1$}) \\
&= (\neg P \wedge \neg Q)^* \\
&= (\neg A)^* & (\text{De Morgan})
\end{aligned}
$$

$\wedge$ 和 $\vee$ 的证明是对称的。

Theorem 4. $A \leftrightarrow B$ 永真则 $A^* \leftrightarrow B^*$ 永真，i.e. $A = B$ 则 $A^* = B^*$。

Proof.

Lemma. $A \leftrightarrow B$ 永真则 $A^- \leftrightarrow B^-$ 永真。

相当于全部带入取反后的值。

$$
\begin{aligned}
&A\leftrightarrow B \\
\Rightarrow& \neg A \leftrightarrow \neg B \\
\Rightarrow& A^{*-} \leftrightarrow \neg B^{*-} \\
\Rightarrow& A^* = B^*
\end{aligned}
$$

Theorem 5. $A\rightarrow B$ 永真则 $B^* \rightarrow A^*$ 永真。

Proof.

$$
\begin{aligned}
&A \rightarrow B = T \\
\Rightarrow& \neg A \vee B = T \\
\Rightarrow& (\neg A \vee B)^* = (T)^* & (\text{Theorem $4$}) \\
\Rightarrow& (\neg A)^* \wedge B^* = F \\
\Rightarrow& \neg((\neg A)^* \wedge B^*) = \neg F \\
\Rightarrow& \neg B^* \vee A^* = T & (\text{De Morgan, Theorem $1$}) \\
\Rightarrow& B^* \rightarrow A^* = T
\end{aligned}
$$

上面的证明中出现了 $\Rightarrow$ 这个符号，现在我还不清楚它严格来说是什么意思，只是依照习惯用来简称“若…则…”。

Theorem 6. $A$ 和 $A^-$ 同永真，同可满足；$\neg A$ 和 $A^*$ 同永真，同可满足。

这个就非常显然了，所以不证明了。

推理

有两类推理关系（直接证明和归谬），用命题逻辑的语言表述如下

$$
\begin{aligned}
(P\rightarrow Q) \wedge P \rightarrow Q \\
(P\rightarrow Q) \wedge \neg Q \rightarrow \neg P
\end{aligned}
$$

注意 $(P\rightarrow Q) \wedge \neg P \rightarrow \neg Q$ 不正确。

重言蕴含

接下来正式解释上面的 $\Rightarrow$ 的含义（好像并没有用错）。

对于两个公式 $A, B$，若 $A$ 为真则 $B$ 必真，那么称 $A\Rightarrow B$（$A$ 重言蕴含 $B$）。注意这里和逻辑联结词 $\rightarrow$ 不同，$A\Rightarrow B$ 不是合式公式，只表示真值关系。

推理演算

有如下定理：

Theorem. $A\Rightarrow B$ 等价于 $A\rightarrow B$ 永真。

证明方法显然，这里不写。

可以用真值表法验证或者简要说明如下公式，书上列了 $16$ 条，并不想抄，因此每个等价类取一个代表元。

基本的推理公式.

1. $P\wedge Q \Rightarrow P, P \Rightarrow P\vee Q$。注意 $P\rightarrow Q = \neg P \vee Q$，所以说可以推出 $\neg P \Rightarrow P\rightarrow Q$，$\neg(P\rightarrow Q)\Rightarrow P$ 等。
2. $\neg P \wedge (P\vee Q) \Rightarrow Q$。
3. $(P\rightarrow Q)\wedge (Q\rightarrow R) \Rightarrow P \rightarrow R$，这个式子称为三段论。
4. $(P\rightarrow Q)\wedge (R\rightarrow S)\wedge (P\vee R) \Rightarrow Q \vee S$。
5. $(Q\rightarrow R)\Rightarrow (P \vee Q) \rightarrow (P \vee R)$，当然这里你取 $\neg P$ 的话可以把右边的 $\vee$ 换成 $\rightarrow$。

基本推理公式常配合如下推理规则使用：

1. 前提引入，可以随时引入前提；
2. 结论引用，可随时引用已经推出的结论；
3. 代入，可以对重言式的命题变项进行代入；
4. 置换，可以将命题公式任何部分替换为与其等价的公式；
5. 分离，$A \wedge A\rightarrow B\Rightarrow B$；
6. 条件证明 $A_1 \wedge A_2 \Rightarrow B$ 等价于 $A_1 \Rightarrow A_2 \rightarrow B$。

分离规则因为其重要性被列为推理规则而非基本推理公式。

做几个题。

Example. 证明 $(P\rightarrow Q)\wedge (R\rightarrow S)\wedge (P\vee R) \Rightarrow Q \vee S$。（基本推理公式 4）

Solution.

$$
\begin{aligned}
(1) & (P\vee R) & \text{前提引入} \\
(2) & \neg P \rightarrow R & \text{(1) 置换} \\
(3) & R \rightarrow S & \text{前提引入} \\
(4) & \neg P \rightarrow S & \text{(2) (3) 三段论} \\
(5) & \neg S \rightarrow P & \text{(4) 置换} \\
(6) & P \rightarrow Q & \text{前提引入} \\
(7) & \neg S \rightarrow Q & \text{(5) (6) 三段论} \\
(8) & Q \vee S & \text{(7) 置换} \\
\end{aligned}
$$

还有下面两个例题，自己做了一手感觉没啥难的，但是体现出了一些思路

Example.

1. 证明 $(P\rightarrow (Q\rightarrow S))\wedge (\neg R\vee P)\wedge Q \Rightarrow R\rightarrow S$。
2. 证明 $(\neg (P \rightarrow Q) \neg (R\vee S)) \wedge ((Q\rightarrow P)\vee \neg R) \wedge R \Rightarrow (P\leftrightarrow Q)$。

Hint.

1. 可以用条件规则，将 $R$ 放到左边去（称为附加条件引入），然后证明 $S$。当然也可以不用，开局先把 $(\neg R\vee P)$ 置换成 $R \rightarrow P$，可以直接三段论证明 $R\rightarrow S$。
2. 可以引入 $\neg (P\leftrightarrow Q)$，然后证明 $\bot$（$R\wedge \neg R$）。当然也可以不用，开局把 $((Q\rightarrow P)\vee \neg R)$ 置换成 $R\rightarrow (Q \rightarrow P)$，且 $R \Rightarrow (R \vee S)$，可以直接证明结论。

Remark. 做题的时候的一些可能的方向：

• $P\rightarrow Q$ 和 $\neg P \vee Q$ 之间的置换。
• 条件证明规则（引入 $\rightarrow$ 的第一个参数作为附加条件）。
• 反证（引入 $\Rightarrow$ 右边的逆命题作为附加条件，证明 $\bot$）。

感觉实际上第三条的本质是 $A\Rightarrow B$，因为 $B = \neg B\rightarrow B$，相当于证明 $A \Rightarrow \neg B\rightarrow B$，使用条件证明规则，只需证明 $A\wedge \neg B \Rightarrow B$。已知 $\bot \Rightarrow B$，如果我们证明了 $A \Rightarrow \neg B \Rightarrow \bot$，那么自然 $A \Rightarrow \neg B\rightarrow B$。

归结推理法（Resolution）

是一种粗暴的机械化方法。

Definition 若子句 $C_1 = L \vee C_1’, C_2 = \neg L \vee C_2’$，即其中含有互补对。定义其归结式（resolvent）为

$$
R(C_1, C_2) = C_1’ \vee C_2’
$$

Theorem(归结原理)

$$
(L \vee C_1) \wedge (\neg L \vee C_2) \Rightarrow C_1 \vee C_2
$$

Proof.

$$
\begin{aligned}
(1) & L \vee C_1 & \text{条件引入} \\
(2) & \neg L \rightarrow C_1 & \text{(1) 置换} \\
(3) & \neg L \vee C_2 & \text{条件引入} \\
(4) & L \rightarrow C_2 & \text{(3) 置换} \\
(5) & L \vee \neg L & \text{排中律} \\
(6) & C_1 \vee C_2 & \text{(2) (4) (5) 基本推理公式 4}
\end{aligned}
$$

上面的定理指出 $C_1 \wedge C_2 \vee R(C_1, C_2)$。

归结推理法是仅采用归结原理作为推理规则的一种方法，其流程大致如下：

• 将右边的命题取反，作为条件（引入附加条件）
• 将条件化为合取范式。
• 重复使用归结原理，推出 $\bot$。

这个算法在之前看的 CS50’s Introduction to Artificial Intelligence with Python 的课的时候，前面讲几个符号主义模型的时候有用 python 实现的 lab。然而这个算法写下来还是非常垃圾，中间结果最多可以有 $2^n$ 个，当然这个上界可能不紧，总之是个指数级的东西。

命题逻辑的公理化

在上一节中我们所做的推理均是基于对命题变项进行赋值来得到重言，这属于从语义角度来理解命题逻辑。在这一节中，我们从语法的角度来看待这件事情。

一个公理系统通常包括：

• 初始符号 可出现的全部符号。
• 形成规则 如何由初始符号构成一个合法的序列。在此形成规则的基础上你可以定义一些别的合法公式的简称。
• 公理 几条初始的语句。
• 变形规则 如何进行演算。可以从公理变形得到的式子称为定理。
• 建立定理 包括所有重言式及其证明。

其他教材对语义和语法做了如下区分：如果一个语句 $A$ 是重言式，则记为 $\vDash A$；如果 $A$ 可以证明，则称 $\vdash A$。一个公理系统可以被证明具有如下两类性质：

• 可靠性. 若 $\vdash A$ 那么 $\vDash A$。
• 完备性. 若 $\vDash A$ 那么 $\vdash A$。

当然出于效率考虑部分不完备的公理系统也是被允许的。

对于命题逻辑我们介绍如下有代表性的公理系统。

其实下面这个系统暂时相当不严谨。但是可以保证本节给出的所有定理都是对的，且用 Agda 写了形式化验证。但是下一节的完备性本人则暂时持怀疑态度。

初始符号 原子命题，$\neg, \vee$（联结词），$(, )$（括号），$\vdash$。$\vdash A$ 语义上表示 $A$ 是重言式，语法上表示 $A$ 可以证明。

形成规则 和普通合式公式的形成规则一样。

补充定义 $A\rightarrow B := \neg A \vee B, A \wedge B := \neg (\neg A \vee \neg B), A \leftrightarrow B := (A\rightarrow B) \wedge (B \rightarrow A)$，用于简写。

公理

$$
\begin{aligned}
\text{A1} \quad & \vdash ((P \vee P) \rightarrow P) \\
\text{A2} \quad & \vdash (P \rightarrow (P \vee Q)) \\
\text{A3} \quad & \vdash ((P \vee Q) \rightarrow (Q \vee P)) \\
\text{A4} \quad & \vdash ((Q \rightarrow R) \rightarrow ((P \vee Q) \rightarrow (P \vee R))) \\
\end{aligned}
$$

从语法的角度来看，应当还需要一条添加和去除括号的公理。下面我们默认可以随便添加和去除括号。

变形规则

• 代入 可以做整体代换。
• 分离 $\vdash A, \vdash A \rightarrow B$ 则 $\vdash B$。
• 置换 可以把补充定义内容的左右两边互相代换。

作为示例我们证明几个重要结论，顺便挖掘一下这个公理系统的性质。

Theorem.($\text{Syl}$)
$$
\vdash (Q \rightarrow R) \rightarrow ((P \rightarrow Q) \rightarrow (P \rightarrow R))
$$

Proof.

$$
\begin{aligned}
(1) & \vdash ((Q \rightarrow R) \rightarrow (\neg P \vee Q) \rightarrow (\neg P \vee R))) & \text{[A4 $\neg P$ $Q$ $R$]} \\
(2) & \vdash (Q \rightarrow R) \rightarrow ((P \rightarrow Q) \rightarrow (P \rightarrow R)) & \text{“$\rightarrow$” 定义置换}
\end{aligned}
$$

Lemma.($\text{Refl}$)

$$
\vdash P \rightarrow P
$$

Proof.

$$
\begin{aligned}
(1) & \vdash P \rightarrow (P \vee P) & [\text{A2 $P$ $P$}] \\
(2) & \vdash (P \vee P) \rightarrow P & [\text{A1}] \\
(3) & \vdash ((P \vee P) \rightarrow P) \rightarrow ((P \rightarrow (P \vee P)) \rightarrow (P \rightarrow P)) & [\text{Syl $P$ $P\vee P$ $P$}] \\
(4) & \vdash (P \rightarrow (P \vee P)) \rightarrow (P \rightarrow P) & \text{(2) (3) 分离} \\
(5) & \vdash (P \rightarrow P) & \text{(1) (4) 分离}
\end{aligned}
$$

Lemma.($\text{EM}$)

$$
P \vee \neg P
$$

Proof.

$$
\begin{aligned}
(1) & \vdash P \rightarrow P & [\text{Refl}] \\
(2) & \vdash \neg P \vee P & \text{“$\rightarrow$” 定义置换} \\
(3) & \vdash (\neg P \vee P) \rightarrow (P \vee \neg P) & [\text{A3 $\neg P$ $P$}] \\
(4) & \vdash P \vee \neg P & \text{(2) (3) 分离}
\end{aligned}
$$

Theorem.($\text{Elim}_r$)
$$
\vdash P \rightarrow \neg \neg P
$$

Proof.

$$
\begin{aligned}
(1) & \vdash \neg P \vee \neg \neg P & [\text{EM $\neg P$}] \\
(2) & \vdash P \rightarrow \neg \neg P & \text{“$\rightarrow$” 定义置换}
\end{aligned}
$$

Theorem.($\text{Elim}_l$)
$$
\vdash \neg \neg P \rightarrow P
$$

Proof.

$$
\begin{aligned}
(1) & \vdash \neg P \rightarrow \neg \neg \neg P & [\text{Idem$_r$ $\neg P$}] \\
(2) & \vdash \neg P \vee P & \text{EM} \\
(3) & \vdash (\neg P \rightarrow \neg \neg \neg P) \rightarrow ((\neg P \vee P)\rightarrow (P \vee \neg \neg \neg P)) & [\text{A4}] \\
(4) & \neg \neg P \rightarrow P & \text{分离两次，[A3], “$\rightarrow$” 定义}
\end{aligned}
$$

Theorem.($\text{Assoc}$)

$$
\vdash (A \vee (B \vee C)) \rightarrow ((A \vee B) \vee C)
$$

Proof.

$$
\begin{aligned}
(1) & \vdash B \rightarrow (A \vee B) & [\text{A2 $B$ $A$}] \\
(2) & \vdash(B \rightarrow (A \vee B)) \rightarrow ((B \vee C) \rightarrow ((A \vee B) \vee C)) & [\text{A4}] \\
(3) & \vdash(B \vee C) \rightarrow ((A \vee B) \vee C) & \text{(1) (2) 分离} \\
(4) & \vdash((B \vee C) \rightarrow ((A \vee B) \vee C)) \rightarrow ((A \vee (B \vee C)) \rightarrow (A \vee ((A \vee B) \vee C))) & [\text{A4}] \\
(5) & \vdash(A \vee (B \vee C)) \rightarrow (((A \vee B) \vee C) \vee A) & \text{(3) (4) 分离} \\
(6) & \vdash A \rightarrow ((A \vee B) \vee C) & [\text{A2}] \\
(7) & \vdash(A \rightarrow ((A \vee B) \vee C)) \\
& \rightarrow ((((A \vee B) \vee C) \vee A) \rightarrow (((A \vee B) \vee C) \vee ((A \vee B) \vee C))) & [\text{A4}] \\
(8) & \vdash(((A \vee B) \vee C) \vee A) \rightarrow (((A \vee B) \vee C) \vee ((A \vee B) \vee C)) & \text{(6) (7) 分离} \\
(9) & \vdash((((A \vee B) \vee C) \vee A) \rightarrow (((A \vee B) \vee C) \vee ((A \vee B) \vee C))) \\
& \rightarrow (((A \vee (B \vee C)) \rightarrow (((A \vee B) \vee C) \vee A)) \\
& \rightarrow ((A \vee (B \vee C)) \rightarrow (((A \vee B) \vee C) \vee ((A \vee B) \vee C)))) & [\text{Syl}] \\
(10)& \vdash(A \vee (B \vee C)) \rightarrow (((A \vee B) \vee C) \vee ((A \vee B) \vee C)) & \text{分离两次} \\
(11)& \vdash(((A \vee B) \vee C) \vee ((A \vee B) \vee C)) \rightarrow ((A \vee B) \vee C) & [\text{A1}] \\
(12)& \vdash((A \vee (B \vee C)) \rightarrow (((A \vee B) \vee C) \vee ((A \vee B) \vee C))) \\
& \rightarrow (((((A \vee B) \vee C) \vee ((A \vee B) \vee C)) \rightarrow ((A \vee B) \vee C)) \\
& \rightarrow ((A \vee (B \vee C)) \rightarrow ((A \vee B) \vee C))) & [\text{Syl}] \\
(13)& \vdash(A \vee (B \vee C)) \rightarrow ((A \vee B) \vee C) & \text{分离两次}
\end{aligned}
$$

这里核心思路是 $A \vee (B \vee C)$ 推成 $((A \vee B) \vee C) \vee ((A \vee B) \vee C)$，上面的过程可能不太是人看的，但经过肉编器编译并修改，多半是对的，故此提醒。

为了确认这个是对的，我们写了一个形式化验证。

做两次交换律，可以得到反方向的结合律，下面均称为 Assoc。

$$
\vdash ((A \vee B) \vee C) \rightarrow (A \vee (B \vee C))
$$

Theorem.($\text{AT}$)

$$
\vdash A \rightarrow (B \rightarrow (A \wedge B))
$$

Proof.

$$
\begin{aligned}
(1) & \vdash (\neg A \vee \neg B) \vee \neg (\neg A \vee \neg B) & [\text{EM}] \\
(2) & \vdash \neg A \vee (\neg B \vee \neg (\neg A \vee \neg B)) & [\text{Assoc}] \\
(3) & \vdash A \rightarrow (B \rightarrow (A \wedge B)) & \text{定义置换}
\end{aligned}
$$

完备性证明

上述公理系统的完备性可以简单地说明。对于任意一个重言式，它可以被写成若干个重言的合取子句的析取范式。即

$$
A = A_1 \wedge \cdots \wedge A_n
$$

其中一个合取子句必然形如（这里可以反证得到）

$$
A_i = \pi \vee \neg \pi \vee B
$$

因为结合律已经得证了，我们不再打括号。有

$$
\begin{aligned}
(1) & \vdash \pi \vee \neg \pi & [\text{EM}] \\
(2) & \vdash (\pi \vee \neg \pi) \vee B & [\text{A2}] \\
(2) & \vdash A_i & \text{定义置换}
\end{aligned}
$$

接下来

$$
\begin{aligned}
(1) & \vdash A_i \\
(2) & \vdash A_j \\
(3) & \vdash A_i \rightarrow (A_j \rightarrow (A_i \wedge A_j)) & [\text{AT}] \\
(4) & \vdash A_i \wedge A_j
\end{aligned}
$$

施归纳法于命题标号，可以得到 $\vdash A$，因此系统完备。

这里有些东西看起来有问题。比如我们使用了集合，反证法和 Peano 自然数导出的归纳法，这些东西并不是建立在当前公理系统上的。公理系统自证完备性疑似是困难的，因此在这里我们暂时接受上述的证明。

自然演绎系统

对上述公理系统做一些扩展，我们定义自然演绎系统。这是一个只有变换规则而没有公理的系统。

初始符号 在上述公理系统的基础上，新增

$$
\Gamma = \{A_1,。。。， A_n\}
$$

表示有限个命题公式的集合。

形成规则 命题公式的形成规则同上述公理系统，而一条完整的公式必须形如

$$
\Gamma \vdash A
$$

其中 $A$ 是命题公式，称为形式结论，$\Gamma$ 是命题公式的有限集，称为形式前提。整个式子表示 $\Gamma$ 和 $A$ 之间存在推理关系。

变形规则

• 肯定前提 $\Gamma \vdash A_i$；
• 转递 $\Gamma \vdash A, A\vdash B$ 则 $\Gamma \vdash B$；这里想说的应该是 $A$ 是一个集合。
• 反证 $\Gamma \cap \{\neg A\} \vdash B$ 且 $\Gamma \cap \{\neg A\} \vdash \neg B$，则 $\Gamma \vdash A$；
• 分离 $\{A \rightarrow B, A\} \vdash B$；
• 蕴含词引入 $\Gamma \cup \{A\}\vdash B$ 则 $\Gamma \vdash A\rightarrow B$。

我们证明三段论来演示这个系统的运作方式。

Theorem.

$$
A\rightarrow B, B\rightarrow C \vdash A \rightarrow C
$$

Proof.

$$
\begin{aligned}
(1) & A \rightarrow B, B\rightarrow C, A \vdash A & \text{肯定前件} \\
(2) & A \rightarrow B, B\rightarrow C, A \vdash A\rightarrow B & \text{肯定前件} \\
(3) & A \rightarrow B, A \vdash B & \text{分离} \\
(4) & A \rightarrow B, B\rightarrow C, A \vdash B & \text{传递} \\
\vdots & \\
(5) & A \rightarrow B, B\rightarrow C, A \vdash C & \text{(同理)} \\
(6) & A\rightarrow B, B\rightarrow C \vdash A \rightarrow C & \text{蕴含词引入}
\end{aligned}
$$

---

此外还有一种演绎系统称为 Hilbert 系统，可以参考这篇文章^[1]，看完之后会对这块内容有更深刻的理解。

---

剩下王浩算法和非标准逻辑，感觉重要度不高，故略去。

---

1. 1.命题逻辑演绎系统的可靠性与完备性, Ref: https://zhuanlan.zhihu.com/p/165188972 ↩