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

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

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

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

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

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

참고 문헌

다음은 린 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. hpp의 증명이라고 가정하겠습니다. 이 증명과 선언(논리합) 왼쪽 도입 규칙에 따라 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입니다.