相继式演算–自然演绎类比

相继式演算和自然演绎拥有相同的逻辑连接词, 都使用推导规则描述逻辑, 并且在证明能力上是等价的, 但两者仍有许多不同之处, 本文给出一组对比.

对于部分规则, 是相同的, 比如蕴涵的如下规则:

$$\frac{\Gamma ,A⊢B}{\Gamma ⊢A\to B}$$

它的另一条规则, 在相继式演算中定义如下, 大致是说 “若 $⊢$ 左边有蕴涵符号, 那么要如何演绎才能推出这个结论”:

$$\frac{\Gamma ⊢A\Gamma ,B⊢C}{\Gamma ,A\to B⊢C}$$

在自然演绎中定义如下, 也就是肯定前件:

$$\frac{\Gamma ⊢A\to B\Gamma ⊢A}{\Gamma ⊢B}$$

这里可以看出如下几个区别:

•	相继式演算会处理 $⊢$ 左边的命题, 但自然演绎总是处理 $⊢$ 右边的命题. 这也是为什么相继式演算会有 “左规则” 和 “右规则” 的概念, 但同样的事情在自然演绎中则对应了 “该逻辑连接词到底是在横线上面还是下面” 这一事实, 更加接近类型论中的构造规则和消去规则.

•	若要给定一个相继式, 去机械地搜索一个演绎, 在相继式演算中这总是不断地从结论到前提、一路追踪到那些没有前提的推导规则, 但在自然演绎中, 我们可能还需要一些从前提推出结论的步骤. 这也是为什么聚焦只能在相继式演算里面研究.