이중 부정 제거 규칙에서 배중률 도출하기

[chabulhwi]

이중 부정 제거 규칙에서 배중률 도출하기

다음은 "린 4로 하는 정리 증명"의 3장 본문 중 이중 부정 제거 규칙에 관한 내용입니다. 저자들은 이중 부정 제거 규칙(dne)에서 배중률(em)을 도출할 수 있음을 독자에게 연습 문제로 남겼습니다.

Double-negation elimination allows one to prove any proposition, p, by assuming ¬p and deriving False, because that amounts to proving ¬¬p. In other words, double-negation elimination allows one to carry out a proof by contradiction, something which is not generally possible in constructive logic. As an exercise, you might try proving the converse, that is, showing that em can be proved from dne.

린 4 코드로는 이를 다음과 같이 진술할 수 있습니다.

theorem em_of_dne (dne : ∀ {p : Prop}, ¬¬p → p) : ∀ {p : Prop}, p ∨ ¬p :=
  sorry

이 정리는 구성주의 논리만으로도 증명할 수 있습니다. 그 증명은 제 멘티들이 이 문제를 푼 뒤에 공개할게요.

참고 문헌

• 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.

[chabulhwi]

다음은 린 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))

1. 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)과 모순됩니다.
2. 위의 1.1~1.2단계에서의 논증에 따라 ¬¬(p ∨ ¬p)입니다.
3. 위의 1~2단계에서의 논증에 따라 ∀ {p : Prop}, p ∨ ¬p입니다.