이 정리는 구성주의 논리만으로도 증명할 수 있습니다. 그 증명은 제 멘티들이 이 문제를 푼 뒤에 공개할게요.
참고 문헌
Avigad, Jeremy, Leonardo de Moura, Soonho Kong, and Sebastian Ullrich et al. “Propositions and Proofs.” Theorem Proving in Lean 4. Accessed November 28, 2024. Propositions and Proofs - Theorem Proving in Lean 4.
theorem em_of_dne (dne : ∀ {p : Prop}, ¬¬p → p) : ∀ {p : Prop}, p ∨ ¬p :=
fun {p : Prop} ↦ show p ∨ ¬p from
dne (show ¬¬(p ∨ ¬p) from
fun h : ¬(p ∨ ¬p) ↦
have hnp : ¬p := fun hp : p ↦ show False from
h (show p ∨ ¬p from Or.inl hp)
show False from h (show p ∨ ¬p from Or.inr hnp))
p가 명제라고 가정하겠습니다. 이중 부정 제거 규칙 dne에 따라, p ∨ ¬p을 증명하는 데는 ¬¬(p ∨ ¬p)임을 보이는 것으로 충분합니다.
1.1. h가 ¬(p ∨ ¬p)의 증명이라고 가정하겠습니다. 이를 바탕으로 ¬p임을 증명할 수 있습니다.
1.1.1. hp가 p의 증명이라고 가정하겠습니다. 이 증명과 선언(논리합) 왼쪽 도입 규칙에 따라 p ∨ ¬p입니다. 이는 증명 h : ¬(p ∨ ¬p)과 모순됩니다. 이 단계에서의 논증에 따라, ¬p의 증명 hnp를 구성할 수 있습니다.
1.2. 증명 hnp : ¬p와 선언 오른쪽 도입 규칙에 따라 p ∨ ¬p입니다. 이는 증명 h : ¬(p ∨ ¬p)과 모순됩니다.