@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

@sno2wman とりあえず最小論理の自然演繹体系での証明を画像で上げます。ヒルベルト流はあまり詳しくないんですが、含意周りをS,Kでやるとたぶんいい感じになったと思います