📐 Lean 4를 활용한 명제 논리 증명: 실전 가이드 🔗

이 글은 Lean 4 프로그래밍 언어이자 정리 증명기(theorem prover)를 사용하여 기초적인 명제 논리 개념과 그 형식적 구현(formal implementation)을 단계별로 살펴보는 기술 가이드입니다.

증명을 형식화하려는 수학자든 타입 이론(type theory)에 뛰어든 프로그래머든, 이 가이드를 통해 제1원리(first principles)로부터 논리를 재구성해 볼 수 있습니다. 기본적인 논리 상수부터 시작하여, 명제는 타입이고 증명은 프로그램이다라는 원리인 **커리-하워드 동형사상(Curry-Howard Isomorphism)**을 통해 Lean 4가 어떻게 논리 구조를 우아하게 모델링하는지 탐구해 보겠습니다.

📑 목차 🔗

⚙️ 도입부(Preamble): 환경 설정하기 🔗

논리 결합자(logical connectives)를 정의하기 전에 먼저 기초 환경을 설정해야 합니다. Lean 4에서는 일반적으로 범위(scope)와 계산 동작을 제어하는 두 가지 특정 명령어를 사용하여 이를 수행합니다.

namespace Basic

noncomputable section

• namespace Basic: 이 명령어는 우리의 정의들을 하나로 묶어 Lean의 내장 라이브러리(Prelude)와 이름이 충돌하는 것을 방지합니다. 이를 통해 교육 목적으로 True, False, And와 같은 근본적인 구조들을 처음부터 직접 재정의할 수 있습니다.
• noncomputable section: Lean 4는 정리 증명기인 동시에 함수형 프로그래밍 언어입니다. 기본적으로 Lean은 모든 정의에 대해 실행 가능한 바이트코드를 생성하려고 시도합니다. 섹션을 noncomputable로 표시하면 컴파일러에 이 단계를 건너뛰도록 지시하는데, 이는 런타임 실행보다 수학적 성질에 관심이 있는 형식 논리에서 흔히 사용되는 방식입니다.

🧩 핵심 논리 결합자 (Core Logical Connectives) 🔗

이 섹션에서는 표준 수학 표기법을 Lean 4 코드에 매핑하면서 논리의 기초 요소들을 정의해 보겠습니다.

✅ 1. 참 (True, ⊤) 🔗

가장 단순한 명제는 보편적으로 논리적 타당성을 지니는 명제입니다. 프로그래밍 관점에서 $\top$은 정확히 하나의 상태만 가지며 추가 데이터를 담지 않는 **유닛 타입(Unit type)**처럼 동작합니다.

정의:

inductive True : Prop where
  | intro : True

단 하나의 생성자(intro)로 정의되어 있기 때문에, True를 “증명"하는 유일한 방법은 바로 이 생성자를 제공하는 것입니다.

예시:

-- 조건 없이 True 증명하기
example : True := True.intro

-- 임의의 명제 'a'는 자명하게 True를 함의함
example {a : Prop} : a → True := fun _ => True.intro

❌ 2. 거짓 (False, ⊥) 🔗

True가 증명의 자명한 존재로 정의된다면, False는 증명의 완전한 부재로 정의됩니다. 이는 빈 타입(Empty type)(또는 Void 타입)입니다.

정의:

inductive False : Prop

False에는 생성자가 전혀 없기 때문에 무(無)에서 이를 인스턴스화할 수 있는 방법은 절대 없습니다. 이는 논리적 모순을 나타냅니다.

폭발 원리 (Ex Falso Quodlibet): 만약 어쩌다 False의 증명을 손에 넣게 된다면, 논리 체계가 무너지면서 무엇이든 증명할 수 있게 됩니다. Lean은 재귀자(recursor)인 False.elim을 사용하여 이를 처리합니다.

-- 거짓으로부터는 임의의 명제 'a'가 모두 도출됨 (⊥ → a)
def False.elim {a : Prop} (false_proof : False) : a := 
  false_proof.rec

🔄 3. 부정 (Negation, ¬) 🔗

Lean 4에서 부정은 원시적인 내장 개념이 아닙니다. 대신 함의(implication)와 False를 사용하여 함수적으로 정의됩니다. 명제 $a$가 거짓임($\neg a$로 표기)을 증명하려면, $a$를 가정했을 때 곧바로 모순($\bot$)으로 이어진다는 함수를 보여주어야 합니다.

정의:

def Not (a : Prop) : Prop := a → False

주요 정리:

-- 부정 증명하기: 'a'를 가정하여 False가 증명되면, Not 'a'가 참임.
theorem Not.intro {a : Prop} (h : a → False) : Not a := 
  fun ha => h ha

-- 이중 부정 도입 (a → ¬¬a)
theorem not_not_intro {a : Prop} (ha : a) : Not (Not a) := 
  fun na => na ha  -- 'na'는 (a → False) 타입이므로 'ha'를 전달하면 False가 반환됨.

-- 부정논법 (Modus Tollens): (a → b)이고 (¬b)이면 (¬a)임
theorem Not.imp {a b : Prop} (nb : Not b) (ab : a → b) : Not a := 
  fun ha => 
    have hb : b := ab ha
    nb hb

➡️ 4. 함의 (Implication, →) 🔗

Lean은 타입 이론에 기반하므로 논리적 함의($a \to b$)는 문자 그대로 **함수(function)**로 취급됩니다. $a$가 $b$를 함의함을 증명하려면, $a$에 대한 임의의 증명을 받아 $b$에 대한 증명을 반환하는 함수를 작성해야 합니다.

연쇄 함의 예시: $c$를 $a$로 바꿀 수 있고 $b$를 $d$로 바꿀 수 있다면, $a \to b$ 함수를 $c \to d$ 함수로 변환할 수 있습니다.

theorem imp_imp_imp {a b c d : Prop} 
  (ca : c → a) (bd : b → d) : (a → b) → (c → d) := 
  fun ab => fun hc => 
    have ha : a := ca hc
    have hb : b := ab ha
    bd hb

🔗 5. 논리곱 (Conjunction, ∧) 🔗

$a$와 $b$가 모두 참이어야 하는 논리곱(And)은 구조체(structure)로 모델링됩니다. 프로그래밍 용어로 이는 두 개의 개별적인 증거를 함께 담고 있는 곱 타입(Product type)(구조체 또는 튜플)입니다.

정의:

structure And (a b : Prop) : Prop where
  intro ::
  left : a
  right : b

주요 증명 패턴:

-- 도입(Introduction): And 생성하기
example {a b : Prop} (ha : a) (hb : b) : And a b := 
  And.intro ha hb

-- 대칭성(Symmetry): a ∧ b → b ∧ a
theorem And.symm {a b : Prop} (h : And a b) : And b a := 
  And.intro h.right h.left

🔀 6. 논리합 (Disjunction, ∨) 🔗

논리합(Or)은 명제 중 적어도 하나가 참일 것을 요구합니다. And와 달리 Or는 증명을 구성하는 두 가지 구별되는 대안적 방법이 존재하기 때문에 귀납적 합 타입(Sum type)(태그된 유니온)입니다.

정의:

inductive Or (a b : Prop) : Prop where
  | inl (h : a) : Or a b
  | inr (h : b) : Or a b

$a \lor b$를 증명하려면 $a$의 증명을 inl(왼쪽 주입, inject-left) 생성자로 감싸거나, $b$의 증명을 inr(오른쪽 주입, inject-right) 생성자로 감싸면 됩니다.

예시:

-- 대칭성(Symmetry): a ∨ b → b ∨ a
theorem Or.symm {a b : Prop} (h : Or a b) : Or b a :=
  match h with
  | Or.inl ha => Or.inr ha
  | Or.inr hb => Or.inl hb

↔️ 7. 논리적 동치 (Logical Equivalence, ↔) 🔗

쌍조건문(Bi-implication) 또는 필요충분조건(Iff, “if and only if”)은 두 명제가 논리적으로 동치임을 나타냅니다. 이는 양방향의 함의를 모두 담고 있는 구조체로 정의됩니다.

정의:

structure Iff (a b : Prop) : Prop where
  intro ::
  mp : a → b
  mpr : b → a

반사성(Reflexivity) 예시:

-- 모든 명제는 자기 자신과 동치임 (a ↔ a)
theorem Iff.refl {a : Prop} : Iff a a :=
  Iff.intro (fun ha => ha) (fun ha => ha)

🎯 결론 및 핵심 요약 🔗

Lean 4에서 명제 논리를 처음부터 다시 구축해 봄으로써 우리는 형식 체계가 지닌 기계적 아름다움을 확인할 수 있습니다.

1. 기본적으로 구성적(Constructive)임: 단순히 무언가가 참이라고 선언하는 대신, 참에 대한 증거를 보유한다는 것이 무슨 의미인지 정의합니다.
2. 타입으로서의 명제: 커리-하워드 매핑을 통해 논리 결합자는 표준 프로그래밍 구조와 일대일로 대응됩니다. 함의는 함수, And는 구조체(struct), Or는 열거형(enum), True는 유닛(unit), False는 보이드(void)입니다.
3. 프로그램으로서의 증명: Lean에서 수학적 증명을 작성하는 것은 특정 시그니처를 만족하는 타입 안전한(type-safe) 함수를 작성하는 것과 정확히 같습니다.

이러한 기초 구성 요소들을 마스터하면 더 복잡한 수학 정리, 술어 논리(predicate logic), 그리고 복잡한 소프트웨어 시스템의 정형 검증(formal verification)을 다루는 데 필요한 핵심 디딤돌을 얻게 됩니다.