证明论学习笔记4：直觉主义逻辑和相继式演算

在讨论直觉主义逻辑之前，我们先看一下用相继式演算（sequent calculus）表示的经典逻辑的自然演绎规则：

相继式式的经典逻辑（ $\mathcal{C}$ ）自然演绎规则

合取引入： $\frac{\Gamma \vdash A \phantom{two} \Delta \vdash B}{ \Gamma, \Delta \vdash A\wedge B}\wedge i$
合取消除： $\frac{\Gamma \vdash A\wedge B}{\Gamma \vdash A}\wedge e_1,\frac{\Gamma \vdash A\wedge B}{\Gamma \vdash B}\wedge e_2$
析取引入： $\frac{\Gamma \vdash A}{\Gamma \vdash A\vee B}\vee i_1,\frac{\Gamma \vdash B}{\Gamma \vdash A\vee B}\vee i_2$
析取消除： $\frac{\Gamma \vdash A\vee B\phantom{tw} \Delta,A\vdash C\phantom{tw} \Theta,B\vdash C }{\Gamma,\Delta,\Theta \vdash C}\vee e$
箭头引入： $\frac{\Gamma,A \vdash B}{\Gamma \vdash A\to B}\to i$
箭头消除： $\frac{\Gamma \vdash A\phantom{tw}\Delta\vdash A\to B}{\Gamma,\Delta\vdash B}\to e$
否定引入： $\frac{\Gamma,A\vdash B}{\Gamma\vdash A\to B}\neg i$
否定消除： $\frac{\Gamma\vdash A\phantom{tw}\Delta \vdash \neg A}{\Gamma,\Delta\vdash \bot}\neg e$
谬误没有引入规则
谬误消除： $\frac{\Gamma \vdash \bot}{\Gamma \vdash A}\bot e$
全称引入： $\frac{\Gamma \vdash A(y)}{\Gamma \vdash \forall x.A(x)}\forall i$
全称消除： $\frac{\Gamma \vdash \forall x.A(x)}{\Gamma \vdash A(t)}\forall e$
存在引入： $\frac{\Gamma \vdash A(t)}{\Gamma \vdash \exists x.A(x)}\exists i$
存在消除： $\frac{\Gamma \vdash \exists x.A(x)\phantom{tw} \Delta,A(y)\vdash B }{\Gamma,\Delta \vdash B}\exists e$
双重否定： $\frac{\Gamma \vdash \neg\neg A}{\Gamma \vdash A}\neg\neg$

在全称引入中， $y$ 不能在 $\Gamma$ 或 $A(x)$ 中自由出现；在存在消除中， $y$ 不能在 $\Gamma$ ， $A(x)$ 或者 $B$ 中自由出现。

除了“双重否定”之外，其余的规则要么是引入规则，要么是消除规则，具有很好的对称性。将“双重否定”这一规则删去，我们就得到了直觉主义逻辑 $\mathcal{I}$ .

但值得注意的是，直觉主义逻辑否定的只是经典逻辑中 $A\Leftrightarrow \neg\neg A$ 的一个方向。由于证明必须具有构造性，我们无法证明 $\neg \neg A\Rightarrow A$ ，但是却可以证明 $A\Rightarrow \neg\neg A$ 。先对 $A\vdash A$ 和 $\neg A\vdash \neg A$ 应用否定消除，得到 $A,\neg A\vdash \bot$ ，再应用否定引入规则，得到 $A\vdash \neg A\to \bot$ ，而 $\neg A\to \bot$ 恰恰是 $\neg\neg A$ 的一未归约式。

从实际证明的角度来讲，有些自然演绎规则是很有用的，例如合取引入规则 $\frac{\Gamma \vdash A \phantom{two} \Delta \vdash B}{ \Gamma, \Delta \vdash A\wedge B}\wedge i$ 。如果我们要找到 $\Gamma,\Delta \vdash A\wedge B$ 的证明，只需要分别找到 $\Gamma\vdash A$ 和 $\Delta\vdash B$ 的证明就好了。但是，有些规则对于寻找证明来说帮助不大，例如合取消除规则。如果要证明“张三是老师”，沿着合取消除规则，我们可以证明“张三和李四是老师”。但“张三和李四是老师”的证明其实比“张三是老师”的证明更难。此外，我们也无法运用否定消除规则来证明 $\Gamma\vdash \bot$ 。

为此，根岑提出了一种新的子逻辑式概念（参见：证明论学习笔记1：预备知识）：

根岑子逻辑式（Gentzen subformula）：

$\bot$ 是所有逻辑式的子逻辑式
$A$ 是 $A$ 和 $\neg A$ 的子逻辑式
$A$ 和 $B$ 是 $B\vee C, B\wedge C$ 和 $B\to C$ 的子逻辑式
如果 $\forall x.B$ 或 $\exists x. B$ 是 $A$ 的子逻辑式，那么 $B[x:=t]$ 也是 $A$ 的子逻辑式。其中 $t$ 是所有不包含 $x$ 的项。

定义（子逻辑式特性，subformula property）：

证明法则 $\frac{\Gamma\vdash A}{\Gamma' \vdash A'}$ 拥有子逻辑式特性，如果 $\Gamma\cup\{A\}$ 中的每一个逻辑式都是 $\Gamma'\cup\{A'\}$ 中一个逻辑式的子逻辑式。

子逻辑式特性可以用来逆推证明。自然演绎规则里的引入规则都具备子逻辑式特性。但它的消去规则都不具备子逻辑式特性。为了确保子逻辑式特性，我们可以将消去规则删除，增加新的一组引入规则，即在语境中引入逻辑运算符的规则，我们称之为“左引入规则”，与之前介绍的引入规则（“右引入规则”）相对应。

简而言之，如果引入的运算符出现在 $\vdash$ 左侧，则为左引入规则，如果引入的运算符出现在 $\vdash$ 右侧，则为右引入规则。根岑的 $\mathcal{I}$ 规则罗列如下：

结构规则（structural rules）：

$\Gamma,A\vdash A$ （包含）
$\frac{\Gamma\vdash C\phantom{tw}\Delta,C\vdash A}{\Delta,\Gamma \vdash A} cut$ （切）
$\frac{\Gamma\vdash\bot}{\Gamma\vdash A}mono_r$ （右单调）
$\frac{\Gamma\vdash A}{\Gamma, B\vdash A}mono_l$ （左单调）

逻辑规则（logical rules）：

右合取： $\frac{\Gamma \vdash A \phantom{two} \Delta \vdash B}{ \Gamma, \Delta \vdash A\wedge B}\wedge r$
左合取： $\frac{\Gamma, A, B \vdash C}{\Gamma, A\wedge B \vdash C}\wedge l$
右析取： $\frac{\Gamma \vdash A}{\Gamma \vdash A\vee B}\vee r _1,\frac{\Gamma \vdash B}{\Gamma \vdash A\vee B}\vee r_2$
左析取： $\frac{\Gamma, A \vdash C\phantom{tw} \Delta, B\vdash C}{\Gamma,\Delta, A\vee B \vdash C}\vee l$
右箭头： $\frac{\Gamma,A \vdash B}{\Gamma \vdash A\to B}\to r$
左箭头： $\frac{\Gamma \vdash A\phantom{tw}\Delta,B\vdash C}{\Gamma,\Delta, A\to B\vdash C}\to l$
右否定： $\frac{\Gamma,A\vdash B}{\Gamma\vdash A\to B}\neg r$
左否定： $\frac{\Gamma\vdash A}{\Gamma,\neg A\vdash \bot}\neg l$
右全称： $\frac{\Gamma \vdash A(y)}{\Gamma \vdash \forall x.A(x)}\forall r$
左全称： $\frac{\Gamma, A(t)\vdash C}{\Gamma,\forall x.A(x)\vdash C}\forall l$
右存在： $\frac{\Gamma \vdash A(t)}{\Gamma \vdash \exists x.A(x)}\exists r$
左存在： $\frac{\Gamma, A(y) \vdash C}{\Gamma,\exists x.A(x) \vdash C}\exists l$