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

相继式演算和自然演绎分别是使用推导规则描述逻辑的两种不同风格. 两者对于部分规则的处理是相同的, 比如蕴涵的如下规则:

$$\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}$$

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

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

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

•	在线性逻辑中, 使用相继式演算可以直接通过把 $\&$ 放在 $⊢$ 左边来得到 $⅋$ 连接词的效果, 但是在使用自然演绎的情况下需要单独定义它.