切规则

在逻辑学中, 切规则是指如下规则:$$\frac{{\Gamma }_1⊢AA,{\Gamma }_2⊢{\Gamma }_3}{{\Gamma }_1,{\Gamma }_2⊢{\Gamma }_3}$$其中, 带下标的 $\Gamma$ 代表一组命题, 或者说一个语境, 而 $A$ 是任意单个命题, 这个命题叫做 “被切掉” 的命题.

切消除定理大致是指对切规则的使用可以被 “消除”, 即该规则可容许.

切规则往往被视为结构性规则.

1范畴语义

参见: 恒同规则

在范畴论中解释逻辑的时候, 一般将整个逻辑解释为某个范畴, 命题解释为其对象、证明 (即一整套推理的过程, 比如从一个没有前提的推理规则一直走到想要的相继式) 解释为其态射, 此时切规则对应的则是复合.

切规则在 ${\Gamma }_2=\varnothing$ 的特殊情况中, “复合” 这一直觉更加明显:

$$\frac{{\Gamma }_1⊢AA⊢{\Gamma }_3}{{\Gamma }_1⊢{\Gamma }_3}$$

2切消除

切消除定理, 或称 Gentzen 主要定理, 是指切规则是可容许规则. 这句话有一些等价的叙述方式以便理解:

•	任何使用切规则的证明都可以改写为不使用切规则的证明.

•	若存在一不使用切规则的 ${\Gamma }_1⊢A$ 的证明, 和一不使用切规则的 ${\Gamma }_2,A⊢{\Gamma }_3$ 的证明, 那么能给出一不使用切规则的 ${\Gamma }_1,{\Gamma }_2⊢{\Gamma }_3$ 的证明.

切消除和恒同规则都可容许这一性质叫做逻辑和谐.

这一定理在大部分相继式演算或者说逻辑中都成立, 并且在设计新的逻辑系统时, 往往会希望它满足这一定理. 但也有一些有用的逻辑中是没有切消除定理的, 这种情况下要么该逻辑不需要切消除, 要么需要切消除作为定义的一部分出现.

后者的一个例子是半公理化逻辑.

3其它形式

顺序逻辑

在顺序逻辑中, 由于交换规则不成立, 因此需要将它改写为如下形式, 允许 $A$ 左右两边都有命题:

$$\frac{\Omega ⊢A{\Omega }_L,A,{\Omega }_R⊢C}{{\Omega }_L,\Omega ,{\Omega }_R⊢C}$$

半公理化逻辑

在半公理化逻辑中, 有一种受限的切规则, 叫做 “剪规则”.

术语翻译

切规则 • 英文 cut rule

切消除 • 英文 cut elimination

Gentzen 主要定理 • 英文 Gentzen’s Hauptsatz