驚くべき帰結2こと`(¬φ → φ) → φ`は排中律と同値らしいのだが全然解けなくて普通に怒りに満ちた帰結2になってる
@sno2wman φ∨¬φ からは (¬φ→φ)→φ が、 (¬(φ∨¬φ)→(φ∨¬φ))→(φ∨¬φ) からは φ∨¬φ が成り立つ、ということから示せると思います......
話をちゃんと整理しました ずっと解けないので誰か解いてみてください
https://scrapbox.io/sno2wman/2023.07.27#64c0dc0a13a15800006c8be4
@sno2wman とりあえず最小論理の自然演繹体系での証明を画像で上げます。ヒルベルト流はあまり詳しくないんですが、含意周りをS,Kでやるとたぶんいい感じになったと思います
@sno2wman SKIバージョン: CM_2 (S (K inr) (S (S (K S) (S (KK) I)) (K inl)))
