Mini wiki
切消定理
编辑
切消定理是确立
相继式演算
重要性的主要结果。它最初由
格哈德·根岑
在他的划时代论文《逻辑演绎研究》对分别形式化
直觉逻辑
和
经典逻辑
的系统LJ和LK做的证明。切削定理声称在相继式演算中,拥有利用了切规则的证明的任何判断,也拥有无切证明,就是说,不利用切规则的证明。
1