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

目录:类型论驿站写作计划

上一篇:证明论学习笔记3:自然演绎

下一篇:证明论学习笔记5:赋值系统

在讨论直觉主义逻辑之前,我们先看一下用相继式演算(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 不能在 \GammaA(x) 中自由出现;在存在消除中, y 不能在 \GammaA(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 是所有逻辑式的子逻辑式
  • AA\neg A 的子逻辑式
  • ABB\vee C, B\wedge CB\to C 的子逻辑式
  • 如果 \forall x.B\exists x. BA 的子逻辑式,那么 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

除了“切”之外,上述规则均满足子逻辑式特性。根岑于是又提出了著名的“切消定理”,即所有用到切的证明均可用没有用到切的证明来代替。

目录:类型论驿站写作计划

上一篇:证明论学习笔记3:自然演绎

下一篇:证明论学习笔记5:赋值系统

参考文献:

Basic proof theory

Handbook of Logic in Computer Science

来源:知乎 www.zhihu.com

作者:Arjuna

【知乎日报】千万用户的选择,做朋友圈里的新鲜事分享大牛。
点击下载