驚くべき帰結2こと`(¬φ → φ) → φ`は排中律と同値らしいのだが全然解けなくて普通に怒りに満ちた帰結2になってる

φ∨¬φ からは (¬φ→φ)→φ が、 (¬(φ∨¬φ)→(φ∨¬φ))→(φ∨¬φ) からは φ∨¬φ が成り立つ、ということから示せると思います......

話をちゃんと整理しました ずっと解けないので誰か解いてみてください

scrapbox.io/sno2wman/2023.07.2

とりあえず最小論理の自然演繹体系での証明を画像で上げます。ヒルベルト流はあまり詳しくないんですが、含意周りをS,Kでやるとたぶんいい感じになったと思います
SKIバージョン: CM_2 (S (K inr) (S (S (K S) (S (KK) I)) (K inl)))
ログインして会話に参加
Fedibird

様々な目的に使える、日本の汎用マストドンサーバーです。安定した利用環境と、多数の独自機能を提供しています。