개념
산술을 표현할 만큼 강한 효과적으로 공리화된 일관된 형식체계에는 그 체계 안에서 증명할 수 없는 문장이 존재한다. 정리의 조건 아래 그 체계는 자기 무모순성도 증명할 수 없다.
한 호흡으로 이해하기
산술을 표현할 만큼 강한 효과적으로 공리화된 일관된 형식체계에는 그 체계 안에서 증명할 수 없는 문장이 존재한다. 정리의 조건 아래 그 체계는 자기 무모순성도 증명할 수 없다. 24세의 괴델은 1930년 첫 결과를 알렸고, 1931년 논문에서 두 정리를 제시했다.
한눈에 보기
시스템 | 강도 | 괴델 정리 적용? | 귀결 |
|---|---|---|---|
프레스부르거 산술 (덧셈만) | 약함 | ✗ — 완전 + 결정 가능 | 계산 가능, 모든 진실 증명 |
튜링 기계 정지 문제 | 계산 모델 | 별도 정리 | 튜링 1936 결정 불가능성 |
페아노 산술 (PA) | 강함 | ✓ 1차 정리 | PA 안에서 증명 불가한 PA의 진실 |
ZFC 집합론 | 매우 강함 | ✓ (일관성 가정) | CH 독립성은 Gödel·Cohen의 별도 결과 |
단순 명제논리 | 약함 | ✗ — 결정 가능 | SAT 풀이 알고리즘 |
효과적으로 공리화되고 산술을 표현할 만큼 강한 일관된 형식체계에는 그 체계 안에서 증명할 수 없는 문장이 존재한다. 정지 문제와 CH 독립성은 관련 있지만 각각 별도의 정리다.
핵심 식
체계는 자신의 무모순성을 증명할 수 없다
핵심 순간
힐베르트 프로그램 — 형식화와 무모순성
1920년대 초 고전 수학을 공리적으로 형식화하고 유한주의적 방법으로 그 무모순성을 정당화하려는 프로그램을 제시.
괴델 — 24세, 두 정리의 논문
1930년 쾨니히스베르크에서 첫 결과를 알린 뒤, 1931년 논문에서 두 불완전성 정리를 제시해 힐베르트 프로그램 목표의 한계를 드러냈다.
튜링 — 정지 문제
튜링이 모든 프로그램의 정지 여부를 판정하는 일반 알고리즘은 없음을 보였다. 형식 체계와는 다른 계산 가능성의 한계 결과.
굿스타인 정리 — 첫 자연스러운 불완전성 예
평범해 보이는 자연수 정리가 페아노 산술 안에서 증명 불가함이 밝혀짐. 괴델 정리의 추상이 아닌 구체적 사례.
오늘날의 응용
컴퓨터 과학의 정지 문제(undecidability), AI의 한계 논의, 형식 검증의 한계, 자기 참조 시스템 분석.
MathVoyage 너머로
불러오는 중…