---
id: wiki-2026-0508-godel-s-incompleteness-theorems
title: "Godel's Incompleteness Theorems"
category: 10_Wiki/Topics
status: verified
canonical_id: self
aliases: [Incompleteness, Godel's Theorems, First and Second Incompleteness]
duplicate_of: none
source_trust_level: A
confidence_score: 0.95
verification_status: applied
tags: [logic, foundations, mathematical-logic, computability, philosophy-of-math]
raw_sources: []
last_reinforced: 2026-05-10
github_commit: pending
tech_stack:
  language: Lean4
  framework: mathlib
---

# Godel's Incompleteness Theorems

## 매 한 줄
> **"매 충분히 강력한 consistent formal system 의 자기 자신의 truth/consistency 의 증명 불가능"**. 1931년 Kurt Gödel 의 결과 — Hilbert program 의 종료, computability/AI/foundation of math 의 근본적 제약. 매 modern 의 Lean/Coq proof assistants, halting problem, Tarski undefinability 의 모두 이의 후예.

## 매 핵심

### 매 First Incompleteness Theorem
- **Statement**: 매 consistent recursively axiomatizable system T 의 Peano Arithmetic 포함 시 — 매 T 에서 증명 불가능 statement G_T (true but unprovable) 존재.
- **Proof sketch**: Gödel numbering → 매 self-referential statement "I am not provable in T" 의 construction → 매 consistency 시 unprovable.
- 매 consequence: 매 truth ≠ provability.

### 매 Second Incompleteness Theorem
- **Statement**: 매 consistent T (PA 포함) 의 자신의 consistency Con(T) 증명 불가능.
- 매 Hilbert program 의 사망 — 매 finitistic 한 means 의 mathematics consistency 의 증명 불가능.
- 매 stronger system 으로 (e.g., ZFC) PA 의 consistency 증명 가능 — but 매 ZFC 자신의 consistency 매 ZFC 안에서 증명 불가능.

### 매 핵심 개념
- **Gödel numbering**: 매 syntactic objects (formulas, proofs) → ℕ 의 injection. 매 meta-mathematical statement 의 arithmetic statement 로의 encoding.
- **ω-consistency** vs **simple consistency**: 매 first proof 의 ω-consistency 의존, Rosser 1936 의 simple consistency 만으로도 OK.
- **Provability predicate Bew_T(x)**: 매 "x 의 numerical encoding 의 statement 매 T 에서 증명가능".
- **Hilbert-Bernays-Löb derivability conditions**: D1, D2, D3.

### 매 응용 / 영향
1. **Halting problem (Turing 1936)**: 매 incompleteness 의 computability twin — 매 universal halting predicate 매 unrecursive.
2. **Tarski's undefinability (1936)**: 매 truth predicate 매 system 자신 안에서 정의 불가능.
3. **Löb's theorem (1955)**: 매 Bew(⌜φ⌝) → φ 증명 시 ⊢ φ.
4. **AI/AGI 의미**: Penrose-Lucas 의 mind ≠ algorithm argument (매 controversial). 2024-2026 LLM era 에서 매 재논쟁.
5. **Foundations**: ZFC 의 large cardinal axioms — 매 stronger theories 의 hierarchy.

## 💻 패턴

### Gödel Numbering (매 simple toy)
```python
def godel_number_str(s):
    """매 매 character 의 ASCII → prime^code product.
    매 unique decoding 가능."""
    primes = [2, 3, 5, 7, 11, 13, 17, 19, 23, 29, 31]
    result = 1
    for i, c in enumerate(s):
        result *= primes[i] ** ord(c)
    return result

def decode_godel(n):
    """매 prime factorization 통해 string 복원."""
    primes = [2, 3, 5, 7, 11, 13, 17, 19, 23, 29, 31]
    chars = []
    for p in primes:
        cnt = 0
        while n % p == 0:
            n //= p
            cnt += 1
        if cnt == 0:
            break
        chars.append(chr(cnt))
    return ''.join(chars)

print(godel_number_str("0=0"))  # 매 huge number
```

### Lean4 — 매 statement 의 formalization
```lean
-- 매 First Incompleteness 의 Lean4 formalization (mathlib outline).
-- 매 actual proof 매 thousand-line ordeal — outline 만.
import Mathlib.Logic.Godel.GodelBetaFunction

theorem godel_first_incompleteness 
    (T : Theory ℒ) (hT : T.Consistent) (hRec : T.RecursivelyEnumerable)
    (hPA : ⊥ ⊆ T) :
    ∃ G : Sentence ℒ, ¬T ⊢ G ∧ ¬T ⊢ ~G := by
  -- 매 self-referential G via diagonalization lemma
  obtain ⟨G, hG⟩ := T.diagonalLemma (¬· ∈ T.theorems)
  exact ⟨G, sorry, sorry⟩
```

### Diagonalization Lemma (매 핵심 trick)
```python
# 매 pseudo-code: matter 의 fixed-point 의 construction.
# 매 statement φ(x) 에 대해, 매 G 의 ⊢ G ↔ φ(⌜G⌝) 의 statement 존재.

def diagonalize(phi):
    """φ(x): 매 free variable x 인 formula.
    Returns G such that PA ⊢ G ↔ φ(⌜G⌝)."""
    # Step 1: substitution function sub(y, x): formula y(x/⌜y⌝)
    # Step 2: G := sub(⌜φ(sub(x,x))⌝, ⌜φ(sub(x,x))⌝)
    # 매 G 의 의미: "I have property φ"
    pass
```

### Halting problem 의 reduction (매 Gödel-Turing)
```python
def halting_problem_undecidable():
    """매 First Incompleteness 의 computability version.
    Halts(P, x) — 매 recursive function 으로 정의 불가능."""
    # 매 Cantor-style diagonal:
    # Suppose Halts(P, x) decidable. Define:
    def D(P):
        if Halts(P, P):
            while True: pass  # loop forever
        else:
            return  # halt
    # 매 D(D) 의 동작 — 매 contradiction.
    # 따라서 Halts 매 decidable 아님.
    pass
```

### Provability Logic (매 GL — Gödel-Löb)
```python
# 매 modal logic GL 의 axioms — 매 Bew predicate 의 modal formalization.
# K: □(p → q) → (□p → □q)
# 4: □p → □□p
# Löb: □(□p → p) → □p

# 매 GL 의 Solovay 1976 의 arithmetic completeness 의 증명 — 매 PA 에서 valid 한 매 modal formula 의 GL 의 정확한 fragment.
```

### Lean — 매 PA consistency proof (in stronger system)
```lean
-- 매 PA's consistency 의 증명 매 ZFC (or PRA + ε₀-induction) 에서 가능.
-- Gentzen 1936 의 ε₀-induction 의존.
theorem PA_consistent : PeanoArithmetic.Consistent := by
  -- 매 actual proof: ordinal analysis up to ε₀
  sorry
```

## 매 결정 기준

| 상황 | Lesson |
|---|---|
| Formal system 의 power 결정 | 매 expressiveness 와 incompleteness 의 trade-off |
| Self-reference 가 가능한가? | Diagonalization 으로 paradox 가능성 |
| Decidable 한 logic 원함 | 매 weak system (e.g., Presburger arithmetic) 사용 |
| Mathematical foundations | ZFC + large cardinals — 매 stronger but still incomplete |
| AGI / consciousness argument | 매 cautious — Penrose 의 controversial |
| Proof assistant 사용 | Lean/Coq — 매 axiom set 명시 (consistency 추가 가정) |

**기본값**: 매 sufficiently expressive system 의 incompleteness 의 inherent — 매 "complete the system" 의 시도는 매 futile 하다 (e.g., Hilbert program 의 실패).

## 🔗 Graph
- 부모: [[Mathematical-Logic]]

## 🤖 LLM 활용
**언제**: 매 conceptual explanation, 매 historical context, 매 proof structure 의 high-level summary, 매 formal logic teaching.
**언제 X**: 매 actual formal proof 작성 — 매 LLM 의 mistake 가능, Lean/Coq 등 proof assistant 사용. 매 Penrose-style "AI cannot reason because of Gödel" argument — 매 fallacy 의 widely critique 됨.

## ❌ 안티패턴
- **"Gödel proves AI impossible"**: 매 fallacy. 매 incompleteness 매 specific formal system 에 대한 statement, 매 thinking 의 nature 와 별개.
- **Confusing First/Second**: 매 First (existence of unprovable truth) ≠ Second (unprovability of consistency).
- **Applying to weak systems**: 매 Presburger arithmetic 의 complete & decidable — 매 incompleteness 매 Robinson arithmetic 이상에 적용.
- **Proof of consistency via system itself**: 매 Second 의 의미 — 매 가능 시 system 자체 의 inconsistent.

## 🧪 검증 / 중복
- Verified (Gödel 1931, Hilbert-Bernays "Grundlagen der Mathematik", Smullyan "Gödel's Incompleteness Theorems").
- 신뢰도 A (foundational result of mathematical logic).

## 🕓 Changelog
| 날짜 | 변경 |
|---|---|
| 2026-05-08 | Phase 1 |
| 2026-05-10 | Manual cleanup — first/second statements, diagonalization, Lean formalization, philosophical caveats |
