Chapter 5. 쿠르트 괴델의 불완전성 정리 증명 과정

1. 불완전성 정리의 역사적 맥락

쿠르트 프리드리히 괴델(Kurt Friedrich Gödel, 1906–1978)은 1931년 “Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I(수학 원리와 관련 체계의 형식적으로 결정 불가능한 명제에 관하여)“를 발표하여 수학 기초론 역사상 가장 심원한 결과 중 하나인 불완전성 정리(Incompleteness Theorems)를 증명하였다. 이 결과는 힐베르트 프로그램(Hilbert’s Program)의 핵심 목표—수학의 완전한 형식화와 무모순성 증명—가 원리적으로 달성 불가능함을 확정하였다.

2. 불완전성 정리의 진술

2.1 제1 불완전성 정리

페아노 산술(Peano Arithmetic)을 포함하는 충분히 강력한 무모순(Consistent) 형식 체계 $\mathcal{F}$ 에 대해, $\mathcal{F}$ 의 언어로 표현 가능하지만 $\mathcal{F}$ 내에서 증명도 반증도 불가능한 참인 문장이 존재한다.

형식적으로, $\mathcal{F}$ 가 무모순이면, 문장 $G_\mathcal{F}$ 가 존재하여:

$G_\mathcal{F}$ 는 참이다(표준 해석에서).
$\mathcal{F} \nvdash G_\mathcal{F}$ ( $G_\mathcal{F}$ 는 $\mathcal{F}$ 에서 증명 불가능).
$\mathcal{F} \nvdash \neg G_\mathcal{F}$ ( $\neg G_\mathcal{F}$ 도 $\mathcal{F}$ 에서 증명 불가능).

2.2 제2 불완전성 정리

페아노 산술을 포함하는 충분히 강력한 무모순 형식 체계 $\mathcal{F}$ 는 자기 자신의 무모순성을 증명할 수 없다.

형식적으로, $\text{Con}(\mathcal{F})$ 가 “ $\mathcal{F}$ 는 무모순하다“를 산술적으로 표현한 문장이면:

$\mathcal{F}$ 가 무모순이면 $\mathcal{F} \nvdash \text{Con}(\mathcal{F})$ .

3. 증명의 핵심 기법: 산술화(Arithmetization)

3.1 괴델 수(Gödel Numbering)

괴델 증명의 핵심 기법은 형식 체계의 모든 구문론적 대상—기호, 공식, 증명—을 자연수로 체계적으로 부호화하는 것이다. 이 부호화에 의해 형식 체계에 관한 메타수학적(Metamathematical) 명제가 산술적 명제로 변환된다.

기호, 항, 공식, 증명열에 고유한 자연수(괴델 수)를 대응시키되, 이 부호화가 효과적(Effective)이고 해독 가능(Decodable)해야 한다. 소수의 거듭제곱에 의한 부호화가 표준적으로 사용된다.

3.2 원시 재귀적 관계의 산술적 표현

괴델은 형식 체계의 핵심 구문론적 관계들이 원시 재귀적(Primitive Recursive)임을 보였다:

“ $x$ 는 변수의 괴델 수이다”
“ $x$ 는 공식의 괴델 수이다”
“ $x$ 는 공리의 괴델 수이다”
“ $x$ 는 $y$ 의 증명의 괴델 수이다” ( $\text{Proof}(x, y)$ )

이 관계들이 원시 재귀적이므로, 페아노 산술 내에서 표현(Represent) 가능하다.

3.3 자기 참조적 문장의 구성

대각선 보조정리(Diagonal Lemma, 또는 고정점 보조정리)에 의해, 형식 체계의 언어로 표현된 임의의 속성 $\phi(x)$ 에 대해, “ $G$ 는 $\phi(\ulcorner G \urcorner)$ 과 동치이다“를 만족하는 문장 $G$ 를 구성할 수 있다. 여기서 $\ulcorner G \urcorner$ 는 $G$ 의 괴델 수이다.

괴델 문장 $G_\mathcal{F}$ 는 이 기법을 증명 불가능성 속성 $\neg \text{Provable}(x)$ 에 적용하여 구성된다:

$G_\mathcal{F} \leftrightarrow \neg \text{Provable}(\ulcorner G_\mathcal{F} \urcorner)$

$G_\mathcal{F}$ 는 “이 문장은 $\mathcal{F}$ 내에서 증명 불가능하다“를 산술적으로 표현한 문장이다.

제1 불완전성 정리의 증명 개요

$G_\mathcal{F}$ 의 증명 불가능성

$\mathcal{F} \vdash G_\mathcal{F}$ 라고 가정한다. 그러면 $G_\mathcal{F}$ 의 증명이 존재하므로 $\text{Provable}(\ulcorner G_\mathcal{F} \urcorner)$ 이 참이다. 그런데 $G_\mathcal{F} \leftrightarrow \neg \text{Provable}(\ulcorner G_\mathcal{F} \urcorner)$ 이므로 $G_\mathcal{F}$ 가 거짓이다. 무모순 체계에서 거짓인 문장이 증명되었으므로 모순이다. 따라서 $\mathcal{F} \nvdash G_\mathcal{F}$ .

$\neg G_\mathcal{F}$ 의 증명 불가능성

$\mathcal{F} \vdash \neg G_\mathcal{F}$ 라고 가정한다. $\neg G_\mathcal{F} \leftrightarrow \text{Provable}(\ulcorner G_\mathcal{F} \urcorner)$ 이므로, $G_\mathcal{F}$ 의 증명이 존재해야 한다. 그러나 방금 $\mathcal{F} \nvdash G_\mathcal{F}$ 를 보았으므로 모순이다(ω-무모순성 가정 하). 따라서 $\mathcal{F} \nvdash \neg G_\mathcal{F}$ .

$G_\mathcal{F}$ 의 진리값

$G_\mathcal{F}$ 가 $\mathcal{F}$ 에서 증명 불가능하므로, $G_\mathcal{F}$ 의 내용—“이 문장은 증명 불가능하다”—이 참이다. 따라서 $G_\mathcal{F}$ 는 참이지만 증명 불가능한 문장이다.

제2 불완전성 정리의 개요

제1 불완전성 정리의 증명을 $\mathcal{F}$ 내부에서 형식화하면, “ $\text{Con}(\mathcal{F}) \rightarrow G_\mathcal{F}$ “가 $\mathcal{F}$ 내에서 증명 가능함을 보일 수 있다. $G_\mathcal{F}$ 가 $\mathcal{F}$ 에서 증명 불가능하므로, $\text{Con}(\mathcal{F})$ 도 $\mathcal{F}$ 에서 증명 불가능하다(대우에 의해).

불완전성 정리의 학문사적 의의

힐베르트 프로그램에의 영향

제1 불완전성 정리는 힐베르트 프로그램의 완전성(Completeness) 목표가 달성 불가능함을 확정하였다. 제2 불완전성 정리는 무모순성(Consistency) 증명 목표가 체계 내부적으로 달성 불가능함을 확정하였다.

수학의 본질에 관한 통찰

불완전성 정리는 수학적 진리(Mathematical Truth)가 형식적 증명 가능성(Formal Provability)을 초과함을 보여준다. 참이지만 증명 불가능한 문장의 존재는 수학적 실재가 형식 체계에 의해 완전히 포착될 수 없음을 의미하며, 이는 수학의 본질에 관한 가장 심원한 메타수학적 통찰이다.

계산 이론과 인공지능에의 영향

불완전성 정리는 튜링의 정지 문제 결정 불가능성 증명에 직접적 영감을 제공하였으며, 인공지능의 이론적 한계에 관한 논쟁에서 핵심적 참조점으로 기능한다. 본 Chapter에서는 불완전성 정리의 증명 과정을 상세히 추적하고, 이 결과가 계산 이론과 인공지능에 미치는 함의를 분석한다.