相继式演算

在逻辑学中, 相继式演算是一种使用相继式的逻辑.

相继式演算的推导规则具有左右对称、恰好一种可逆的规律.

1推导规则

此处假设结构性规则都成立.

直觉主义相继式演算

一个直觉主义相继式是指 $⊢$ 右边只有一个命题的相继式.

•	恒同规则和切规则: $$\frac{}{\Gamma ,A⊢A}\frac{\Gamma ⊢A\Gamma ,A⊢C}{\Gamma ⊢C}$$

•	蕴涵: $$\frac{\Gamma ,A⊢B}{\Gamma ⊢A\to B}\frac{\Gamma ,A\to B⊢A\Gamma ,A\to B,B⊢C}{\Gamma ,A\to B⊢C}$$

•	与的规则: $$\frac{\Gamma ⊢A\Gamma ⊢B}{\Gamma ⊢A\wedge B}\frac{\Gamma ,A\wedge B,A,B⊢C}{\Gamma ,A\wedge B⊢C}$$其单位元的规则: $$\frac{}{\Gamma ⊢1}\frac{\Gamma ⊢C}{\Gamma ,1⊢C}$$

•	或: $$\frac{\Gamma ⊢A}{\Gamma ⊢A\vee B}\frac{\Gamma ⊢B}{\Gamma ⊢A\vee B}\frac{\Gamma ,A\vee B,A⊢C\Gamma ,A\vee B,B⊢C}{\Gamma ,A\vee B⊢C}$$

经典相继式演算

未来可以移动到单独的词条

在经典相继式演算中, 有如下额外特性:

•	$⊢$ 右边可以有多个命题. $\Gamma ⊢\Delta$ 的意思是说, 在 $\Gamma$ 中全部命题成立的情况下, $\Delta$ 中至少有一个命题成立.

•	或的右规则 (关于右规则的定义, 参见后文) 可以借助这一特性重新定义: $$\frac{\Gamma ⊢A,B,\Delta }{\Gamma ⊢A\vee B,\Delta }$$其单位元的定义也可以变得很简单: $$\frac{}{\Gamma ,0⊢\Delta }\frac{\Gamma ⊢\Delta }{\Gamma ⊢0,\Delta }$$

•	命题的否定 $\neg A:=A\to 0$ 类似于 “移动位置”, 换言之如下定理写成规则的形式是可导出规则: $$\Gamma ,A⊢\Delta ⟺\Gamma ⊢\neg A,\Delta$$从左到右可以这样证明: $$\frac{\Gamma ,A⊢\Delta }{\frac{\Gamma ,A⊢0,\Delta }{\Gamma ⊢A\to 0,\Delta }}$$

•	许多经典逻辑中和排中律相关的公理在经典相继式演算中都可以证明. 例如, 排中律可以这样证明: $$\frac{A⊢A}{\frac{⊢\neg A,A}{⊢\neg A\vee A}}$$

2性质

相继式演算满足切消除定理, 即切规则是可容许规则.

没有切规则的经典相继式演算具有子公式性质.

对称性

相继式演算的每个逻辑连接词都有左规则和右规则之分: 对于规则导出的相继式 $\Psi ⊢A$, 若某规则对 $\Psi$ 中的连接词进行消除, 那么称之为左规则, 反之则称之为右规则.

定义 2.1. 某规则可逆大致是说它上下颠倒的版本是可导出规则或者可容许规则.

一般来说, 不可逆的那些规则在证明中包含非平凡的信息.

若某连接词的左规则可逆 (又叫左可逆), 那么认为该连接词的极性为正, 否则为负.

3相关概念

•	自然演绎, 参见自然演绎–相继式演算类比.

•

极性.

•	聚焦是相继式演算特有的 “大步证明” 手段.

术语翻译

相继式演算 • 英文 sequent calculus

直觉主义相继式 • 英文 intuitionistic sequent