驚くべき帰結2こと`(¬φ → φ) → φ`は排中律と同値らしいのだが全然解けなくて普通に怒りに満ちた帰結2になってる
フォロー
話をちゃんと整理しました ずっと解けないので誰か解いてみてください
https://scrapbox.io/sno2wman/2023.07.27#64c0dc0a13a15800006c8be4
@sno2wman@fedibird.com 二重否定の除去経由するのかなと思ったけど爆発律が無いせいで頭が爆発してしまった
@sno2wman p ∨ ¬p → ⊥ を仮定するとp → p ∨ ¬p, だから p → ⊥, よって p ∨ ¬pが証明できる（と思う）
https://scrapbox.io/kokuritsukouen/%E6%8E%92%E4%B8%AD%E5%BE%8B%E3%81%AFHPM_+_CM%E2%82%82%E3%81%A7%E8%A8%BC%E6%98%8E%E5%8F%AF%E8%83%BD
ありがとうございました！
https://mstdn.jp/@palalansouki/110780132085245415
https://bi.cbult.space/objects/245ba11d-0ea2-416b-96f7-d4e0ad0be0e2 [参照]