論理学の授業で自然演繹を習うとき、最小論理にボトムの除去則、ないしは公理図式"￢A→(A→B)"を加えるとを加えると直観主義になると教わる。しかし、これは保存拡大にならない。まぁ、ボトムには導入則がないのだから、除去則を導入則によって正当化する、みたいな話にもなりようがないのかな。
ところで、シークエント計算では最小論理という名前はなぜか聞かない。しかし、直観主義LJでEFQを導出するには右の弱化規則を本質的に使うので、右の弱化規則を制限すれば、最小論理になるんじゃないかと予想してみる。もしそうだとすると、最小論理は部分構造論理ということになる。
例えば、一般に知られているEFQの導出方法は、C.I.ルイスの独立性論証で、これは選言の導入則と選言的三段論法を本質的に使っている。シークエント計算で選言的三段論法を導出すると
A:A
----
A, not-A:
-------
A, not-A: B B:B
-------------------
AvB, not-A:B
という風になるから、やはり右の弱化規則が本質的か。
あと、EFQと右の弱化規則は犠牲にしてもいいけど、選言的三段論法は犠牲にしたくない、という場合には、まだ最終手段としてカット規則を捨てるという手もありそうである。というのも、
A:A
------
A:AvB AvB, not-A:B
---------------
A, not-A:B
独立性論証では、EFQの導出にカット規則が関わるから…。
