음주자 역설

논리학
1

수리 논리학자 레이먼드 스멀리언(Raymond_Smullyan)이 사람들에게 알린 음주자 역설[drinker paradox]은 고전 술어 논리의 정리이고, 그 진술은 다음과 같습니다.

사람이 적어도 한 명 있는 모든 선술집에 대해, 다음 요건을 갖추는 사람 x가 그 선술집에 존재한다.

x가 술을 마시고 있으면, 그 선술집에 있는 모든 사람이 술을 마시고 있다.

린 정리 증명기로 이 정리의 증명을 작성했는데, 그 증명은 잠시 후에 공유하겠습니다. 위의 요건을 충족하는 사람의 보기를 들 때, 그 사람이 술을 마시고 있지 않아도 된다는 점이 실마리입니다.

한국어 증명은 다음과 같습니다.

  1. 그 선술집에 있는 모든 사람이 술을 마시고 있거나, 그 선술집에 있으면서 술을 마시고 있지 않은 사람이 존재합니다. (배중률, 보편 명제의 부정)
  2. 선언 (1)을 이루는 첫째 명제가 참이라고 가정하겠습니다. (가정)
    2.1. 그 선술집에는 사람이 적어도 한 명 있으므로, 그런 어느 한 사람을 a로 나타낼 수 있습니다. (존재 정량어 제거)
    2.2. a가 술을 마시고 있으면, 그 선술집에 있는 모든 사람이 술을 마시고 있습니다. 이 조건문이 참인 이유는 그 결론이 참이기 때문입니다. 이 조건문의 결론은 (2)의 가정입니다. (조건문 도입)
    2.3. 따라서 위에서 언급된 요건을 갖추는 사람 x가 그 선술집에 존재합니다. (존재 정량어 도입)
  3. 선언 (1)을 이루는 둘째 명제가 참이라고 가정하겠습니다. (가정)
    3.1. (3)의 가정에 따라, 그 선술집에 있으면서 술을 마시고 있지 않은 어느 한 사람을 a로 나타낼 수 있습니다. (존재 정량어 제거)
    3.2. a가 술을 마시고 있으면, 그 선술집에 있는 모든 사람이 술을 마시고 있습니다. 이 조건문이 참인 이유는 그 가정이 거짓이기 때문입니다. 이 조건문의 가정이 거짓인 이유는 (3.1) 때문입니다. (조건문 도입, 부정 제거, 거짓 제거)
    3.3. 따라서 위에서 언급된 요건을 갖추는 사람 x가 그 선술집에 존재합니다. (존재 정량어 도입)
  4. (1)-(3)에 따라, 위에서 언급된 요건을 갖추는 사람 x가 그 선술집에 존재합니다. (선언 제거)

린 4 증명은 다음 링크의 메시지에 있습니다. https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/Stuck.20on.20lean.20book.20example/near/482918164

20241118_11h49m28s_drinker-paradox
20241118_11h49m28s_drinker-paradox1161×1570 115 KB

2개의 좋아요
3

이 정리가 역설처럼 보이는 이유는 아무래도 우리가 형식 논리학 밖의 맥락에서 이해하는 함의가 형식 논리학의 내용적 함의와 다르기 때문이지 않을까요? 음주자 역설은 다음과 같이 서술할 수도 있는데, 내용적 함의를 배운 적이 없는 분들도 과연 원래의 진술과 다음 진술이 내용상 동등하다고 생각할까요?

사람이 적어도 한 명 있는 모든 선술집에 대해, 술을 마시고 있지 않은 사람이 그 선술집에 존재하거나, 그 선술집에 있는 모든 사람이 술을 마시고 있다.

두 진술이 동등하다는 증명은 아래의 보기에 있습니다.

theorem funext_propext {α : Sort u} {p q : α → Prop} (h : ∀ {x}, p x ↔ q x) :
    (fun x : α ↦ p x) = (fun x : α ↦ q x) :=
  funext (fun _ ↦ propext h)

theorem exists_or_right {α : Sort u} {p : α → Prop} {r : Prop} [Inhabited α] :
    (∃ x, (p x ∨ r)) ↔ (∃ x, p x) ∨ r :=
  Iff.intro
    (fun h ↦ let ⟨a, ha⟩ := h; Or.elim ha (fun hp ↦ Or.inl ⟨a, hp⟩) Or.inr)
    (fun h ↦ Or.elim h
      (fun hexp ↦ let ⟨a, hp⟩ := hexp; ⟨a, Or.inl hp⟩)
      (fun hr ↦ ⟨default, Or.inr hr⟩))

open Classical

example {Pub : Sort u} {IsDrinking : Pub → Prop} [Inhabited Pub] :
    (∃ x, (IsDrinking x → ∀ y, IsDrinking y)) ↔ (∃ x, ¬IsDrinking x) ∨ ∀ y, IsDrinking y := by
  rw [funext_propext Decidable.imp_iff_not_or, exists_or_right]
4

술어논리 표기에 좀 더 익숙하신 분들을 위해..

증명하고자 하는 명제 : (∃x)(Dx→(y)Dy)
('Dx' : x가 술을 마신다, 논의영역 U : 선술집에 있는 사람들)

  1. (x)Dx v ~(x)Dx (논리적 참)
  2. (x)Dx [조건증명을 위한 가정]
  3. Dy (2, 보편양화사 제거)
  4. (y)Dy (3, 보편양화사 도입)
  5. (y)Dy v ~Dt (4, 선언지 추가)
  6. ~Dt v (y)Dy (5, 교환법칙)
  7. Dt→(y)Dy (6, 동치)
  8. (∃x)(Dx→(y)Dy) (7, 존재양화사 도입)
  9. (x)Dx→(∃x)(Dx→(y)Dy) [조건증명 종료]
  10. ~(x)Dx [조건증명을 위한 가정]
  11. (∃x)~Dx (10, 양화사 동치규칙)
  12. ~Dt (11, 존재양화사 제거)
  13. ~Dt v (y)Dy (12, 선언지 추가)
  14. Dt→(y)Dy (13, 동치)
  15. (∃x)(Dx→(y)Dy) (14, 존재양화사 도입)
  16. ~(x)Dx→(∃x)(Dx→(y)Dy) [조건증명 종료]
  17. (∃x)(Dx→(y)Dy) (1, 9, 16 구성적 삼단논법 & 동어반복 선언지 제거)
    ■증명 끝!

스멀리안의 재능도 참 철학사에서 귀한 재능인 것 같네요 ㅋㄷ

7개의 좋아요