디아코네스쿠 정리

2024년 8월 5일 · 태그: mathematics, logic · 원문 · 한국어 번역(원문에서 변경됨)

1975년 라두 디아코네스쿠(Radu Diaconescu)가 발견한 디아코네스쿠 정리는 수학의 두 가지 근본 원리인 선택 공리와 배중률 사이에 흥미롭고도 놀라운 연관성이 있음을 보여 줍니다. 간단히 말해, 이 정리는 선택 공리를 받아들이면 배중률도 받아들여야 한다는 것을 말합니다. 이 정리는 1978년 굿맨(Goodman)과 마이힐(Myhill)이 독립적으로 발견하였으며, 디아코네스쿠-굿맨-마이힐 정리라고 불리기도 합니다. 흥미롭게도 에렛 비숍(Errett Bishop)은 디아코네스쿠의 발표 이전에 구성적 해석학에 관한 1967년 저서에서 이 결과를 연습 문제로 제시한 바 있습니다.

배경 지식으로, 배중률은 임의의 명제 $P$ 에 대해 $P$ 가 참이거나 $P$ 가 거짓이며 그 중간 상태는 없다는 원리입니다. 기호로 나타내면 $P \lor \neg P$ 입니다. 예를 들어, 어떤 수는 짝수이거나 짝수가 아닙니다. 직관적으로 보이지만, 모든 수학 체계가 이 원리를 받아들이는 것은 아닙니다!

선택 공리는 공집합이 아닌 집합들의 임의의 모임이 주어졌을 때, 각 집합에서 정확히 하나의 원소를 골라 새로운 집합을 만들 수 있다는 공리입니다. 이 역시 직관적으로 보이지만, 몇 가지 놀라운 결과를 낳습니다.

디아코네스쿠 정리는 다음을 보여 줍니다.

$Axiom of Choice ⟹ Law of Excluded Middle$

증명에 들어가기 전에 몇 가지 중요한 개념을 정리해 봅시다.

모든 원소에 대해 그 원소가 집합에 속하는지 아닌지를 판별할 수 있을 때, 그 집합을 **결정 가능(decidable)**하다고 합니다. 형식적으로는, 임의의 원소 $x$ 에 대해 $x \in S$ 이거나 $x \in / S$ 입니다.
어떤 집합 위로의 모든 전사 함수가 분할될 때(즉, 거꾸로 가는 사상이 존재하여 두 사상의 합성이 항등 사상이 될 때), 그 집합을 **선택 집합(choice set)**이라고 합니다.

증명은 다음 단계를 거쳐 진행됩니다.

참이거나 거짓이어야 함을 증명하고자 하는 임의의 명제 $P$ 에서 시작합니다
두 집합을 구성합니다.
- $U = x \in 0, 1 ∣ (x = 0) \lor P$
- $V = x \in 0, 1 ∣ (x = 1) \lor P$
두 집합 모두 공집합이 아님이 보장됩니다.
- $U$ 는 0을 포함합니다( $x = 0$ 일 때 $x = 0$ 이 참이기 때문입니다)
- $V$ 는 1을 포함합니다( $x = 1$ 일 때 $x = 1$ 이 참이기 때문입니다)
집합 $X = U, V$ 를 만듭니다. $U$ 와 $V$ 가 모두 공집합이 아니므로, 선택 공리에 의해 각 집합에서 원소를 하나씩 고를 수 있습니다.
$f$ 를 선택 함수라고 합시다. 선택 집합에서는 동등성이 결정 가능하므로(형식적 증명의 핵심 보조정리), $f (U)$ 와 $f (V)$ 를 분석할 수 있습니다.
- $f (U) = 0$ 이면 $P$ 는 거짓이어야 합니다( $\neg P$ )
- $f (U) = 1$ 이면 $P$ 는 참이어야 합니다
- $f (V)$ 에도 같은 분석이 적용됩니다
이 분석을 통해 $P \lor \neg P$ 가 성립해야 한다는 결론을 내릴 수 있습니다.

이 정리를 Lean으로 형식화할 수 있습니다. 이 증명은 선택과 함께 함수 외연성과 명제 외연성을 사용합니다. Lean 증명은 우리의 수학적 증명과 같은 논리 구조를 따르지만, 집합 대신 명제를 다룹니다. 술어의 동등성을 다루기 위해 함수 외연성과 명제 외연성을 사용하며, 선택 공리는 존재 명제에서 증인을 골라내는 choose 함수의 형태로 나타납니다.

먼저 정리를 em의 타입 선언으로 기술합니다:

theorem em (p : Prop) : p ∨ ¬p :=

이 형식 증명이 어떻게 동작하는지 하나씩 살펴봅시다:

먼저 명제 x를 받아 또 다른 명제를 반환하는 두 술어 U와 V를 정의합니다:
```
let U (x : Prop) : Prop := x = True ∨ p
let V (x : Prop) : Prop := x = False ∨ p
```
이들은 우리의 수학적 증명에 나오는 집합 U와 V에 대응하지만, {0,1} 대신 명제를 다룹니다.

U와 V가 모두 거주되어 있음(비어 있지 않음)을 증명합니다:

have exU : ∃ x, U x := ⟨True, Or.inl rfl⟩   -- True satisfies U because True = True
have exV : ∃ x, V x := ⟨False, Or.inl rfl⟩  -- False satisfies V because False = False

선택 공리를 사용하여(choose를 통해) U와 V에서 각각 증인 u와 v를 고릅니다:

let u : Prop := choose exU
let v : Prop := choose exV
have u_def : U u := choose_spec exU  -- u satisfies U
have v_def : V v := choose_spec exV  -- v satisfies V

핵심 통찰은 u ≠ v이거나 p가 참이어야 한다는 것입니다:

have not_uv_or_p : u ≠ v ∨ p :=
  match u_def, v_def with
  | Or.inr h, _ => Or.inr h        -- If U(u) because of p, then p is true
  | _, Or.inr h => Or.inr h        -- If V(v) because of p, then p is true
  | Or.inl hut, Or.inl hvf =>      -- Otherwise, u = True and v = False
    have hne : u ≠ v := by simp [hvf, hut, true_ne_false]
    Or.inl hne

다음으로 p가 참이면 u = v임을 증명합니다:

have p_implies_uv : p → u = v :=
  fun hp =>
  have hpred : U = V :=    -- If p is true, then U and V are the same predicate
    funext fun x =>        -- Using function extensionality
      have hl : (x = True ∨ p) → (x = False ∨ p) :=
        fun _ => Or.inr hp
      have hr : (x = False ∨ p) → (x = True ∨ p) :=
        fun _ => Or.inr hp
      show (x = True ∨ p) = (x = False ∨ p) from
        propext (Iff.intro hl hr)   -- Using propositional extensionality

마지막으로 경우 분석을 통해 p ∨ ¬p라는 결론을 내립니다:

match not_uv_or_p with
| Or.inl hne => Or.inr (mt p_implies_uv hne)  -- If u ≠ v, then ¬p
| Or.inr h   => Or.inl h                      -- If p, then p

디아코네스쿠 정리는 선택 원리와 고전 논리 사이의 깊은 연관성을 보여 줍니다. 이 결과는 중요한 메타수학적 함의를 지닙니다. 선택 원리는 본질적으로 비구성적이라는 사실을 드러내는데, 다른 면에서는 구성적인 환경에서도 고전적 추론을 강제하기 때문입니다. 기초론적 관점에서 보면, 이는 선택 원리가 논리적으로 중립적이지 않다는 것을 보여 줍니다. 선택 원리는 암묵적으로 우리를 고전 논리에 묶어 둡니다. 구성적 수학에서는 이 때문에 선택 원리를 신중하게 고려해야 합니다. 겉보기에 무해한 AC의 사용조차도 다른 면에서는 구성적인 전개를 자기도 모르게 고전화할 수 있기 때문입니다. 따라서 이 정리는 기초 공리가 수학 이론의 논리적 성격에 미묘하지만 광범위한 영향을 미칠 수 있음을 잘 보여 줍니다. 선택 공리와 배중률에 관한 한, 중간 지대를 선택할 여지는 없다고 말할 수 있겠습니다!

Keyboard shortcuts

Stephen Diehl 블로그 한국어 번역

디아코네스쿠 정리