5.17 제2 불완전성 정리의 정식화: 무모순성의 내적 증명 불가능성

1. 제2 불��전성 정리의 진술

1.1 형식적 진술

효과적으로 공리화되고, 충분히 강력하며(페아노 산술을 포함), 무모순한 형식 체계 $\mathcal{F}$ 에 대해, “ $\mathcal{F}$ 는 무모순하다“를 표현하는 $\mathcal{F}$ 의 문장 $\text{Con}(\mathcal{F})$ 는 $\mathcal{F}$ 내에서 증명 불가능하다:

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

무모순성 문장 $\text{Con}(\mathcal{F})$ 의 정의

$\text{Con}(\mathcal{F})$ 는 “ $\mathcal{F}$ 에서 모순이 도출되지 않는다“를 $\mathcal{F}$ 의 언어로 표현한 문장이다. 형식적으로:

$\text{Con}(\mathcal{F}) \equiv \neg\text{Prov}(\ulcorner 0 = S(0) \urcorner)$

또는 동등하게:

$\text{Con}(\mathcal{F}) \equiv \neg\exists x \, \text{Prf}(x, \ulcorner 0 = 1 \urcorner)$

“ $0 = 1$ 이 $\mathcal{F}$ 에서 증명 불가능하다.” $0 = 1$ 은 거짓인 문장이므로, 이 문장이 증명 불가능하다는 것은 $\mathcal{F}$ 가 무모순하다는 것과 동치이다.

(대안적으로, 임의의 거짓 문장 $\bot$ 에 대해 $\text{Con}(\mathcal{F}) \equiv \neg\text{Prov}(\ulcorner \bot \urcorner)$ 로 정의해도 동등하다.)

제1 불완전성 정리로부터의 도출

도출의 핵심 아이디어

제2 불완전성 정리는 제1 불완전성 정리의 증명을 $\mathcal{F}$ 내부에서 형식화함으로써 도출된다.

제1 불완전성 정리의 증명 중 부분 1(“ $\mathcal{F}$ 가 무모순이면 $\mathcal{F} \nvdash G$ ”)을 $\mathcal{F}$ 내부에서 형식화하면, 다음이 $\mathcal{F}$ 에서 증명 가능하다:

$\mathcal{F} \vdash \text{Con}(\mathcal{F}) \rightarrow \neg\text{Prov}(\ulcorner G \urcorner)$

괴델 문장의 정의에 의해 $G \leftrightarrow \neg\text{Prov}(\ulcorner G \urcorner)$ 이므로:

$\mathcal{F} \vdash \text{Con}(\mathcal{F}) \rightarrow G$

만약 $\mathcal{F} \vdash \text{Con}(\mathcal{F})$ 이면, 전건 긍정에 의해 $\mathcal{F} \vdash G$ 이다. 그러나 제1 불완전성 정리에 의해 $\mathcal{F} \nvdash G$ 이다. 따라서 $\mathcal{F} \nvdash \text{Con}(\mathcal{F})$ 이다.

형식화의 요구사항

위 도출이 성립하려면, 제1 불완전성 정리의 증명이 $\mathcal{F}$ 내부에서 형식화 가능해야 한다. 이를 위해 증명 가능성 술어 $\text{Prov}$ 가 특정 조건을 만족해야 한다.

힐베르트-베르나이스-뢰브 도출 가능성 조건

증명 가능성 술어 $\text{Prov}$ 가 만족해야 하는 세 가지 조건:

D1 (Σ₁-완전성): $\mathcal{F} \vdash \phi$ 이면 $\mathcal{F} \vdash \text{Prov}(\ulcorner \phi \urcorner)$ .

$\mathcal{F}$ 에서 증명 가능한 문장에 대해, 그 증명 가능성이 $\mathcal{F}$ 내에서 확인 가능하다.

D2 (분배성): $\mathcal{F} \vdash \text{Prov}(\ulcorner \phi \rightarrow \psi \urcorner) \rightarrow (\text{Prov}(\ulcorner \phi \urcorner) \rightarrow \text{Prov}(\ulcorner \psi \urcorner))$ .

$\mathcal{F}$ 에서 조건문의 증명 가능성이 전건과 후건의 증명 가능성에 대한 분배를 $\mathcal{F}$ 내부에서 증명할 수 있다.

D3 (반복 가능성): $\mathcal{F} \vdash \text{Prov}(\ulcorner \phi \urcorner) \rightarrow \text{Prov}(\ulcorner \text{Prov}(\ulcorner \phi \urcorner) \urcorner)$ .

증명 가능성의 증명 가능성이 $\mathcal{F}$ 내부에서 증명될 수 있다.

이 세 조건은 $\text{Prov}$ 가 증명 가능성의 핵심적 성질을 $\mathcal{F}$ 내부에서 반영함을 보장하며, 제2 불완전성 정리의 증명에서 필수적으로 사용된다.

제2 불완전성 정리의 상세 증명

전제: $\mathcal{F}$ 는 효과적으로 공리화되고, PA를 포함하며, 무모순하다. $\text{Prov}$ 는 D1–D3을 만족한다.

단계 1: 괴델 문장 $G$ 에 대해 $\mathcal{F} \vdash G \leftrightarrow \neg\text{Prov}(\ulcorner G \urcorner)$ .

단계 2: 대우(Contrapositive)에 의해:
$\mathcal{F} \vdash \text{Prov}(\ulcorner G \urcorner) \rightarrow \neg G$

단계 3: $G \rightarrow \neg\text{Prov}(\ulcorner G \urcorner)$ 이므로, 대우:
$\mathcal{F} \vdash \text{Prov}(\ulcorner G \urcorner) \rightarrow \neg G$

한편 $\neg G \rightarrow \text{Prov}(\ulcorner G \urcorner)$ 이므로:
$\mathcal{F} \vdash \text{Prov}(\ulcorner G \urcorner) \leftrightarrow \neg G$

단계 4: $\mathcal{F}$ 내부에서 다음을 증명한다:

“ $\text{Prov}(\ulcorner G \urcorner)$ 이면 $\text{Prov}(\ulcorner \neg G \urcorner)$ 이다”

이는 단계 2와 D1에서 도출된다.

“ $\text{Prov}(\ulcorner G \urcorner)$ 이면 $\text{Prov}(\ulcorner G \urcorner) \wedge \text{Prov}(\ulcorner \neg G \urcorner)$ 이다”

단계 5: $\text{Con}(\mathcal{F}) \equiv \neg(\text{Prov}(\ulcorner G \urcorner) \wedge \text{Prov}(\ulcorner \neg G \urcorner))$ 이므로:
$\mathcal{F} \vdash \text{Con}(\mathcal{F}) \rightarrow \neg\text{Prov}(\ulcorner G \urcorner)$
$\mathcal{F} \vdash \text{Con}(\mathcal{F}) \rightarrow G$

단계 6: $\mathcal{F}$ 가 무모순이므로 $\mathcal{F} \nvdash G$ (제1 불완전성 정리). 따라서 $\mathcal{F} \nvdash \text{Con}(\mathcal{F})$ . $\blacksquare$

2. 제2 불완전성 정리의 함의

2.1 무모순성 증명의 본질적 한계

체계 $\mathcal{F}$ 의 무모순성을 증명하려면 $\mathcal{F}$ 보다 강력한(더 많은 공리를 가진) 체계 $\mathcal{F}'$ 가 필요하다. 그러나 $\mathcal{F}'$ 의 무모순성도 $\mathcal{F}'$ 자체로는 증명 불가능하므로, 더 강력한 $\mathcal{F}''$ 가 필요하다. 이 무한 후퇴(Infinite Regress)는 형식 체계의 무모순성에 대한 절대적 확신이 형식적 방법만으로는 달성 불가능함을 의미한다.

2.2 힐베르트 프로그램에 대한 최종적 타격

힐베르트는 무한수학(예: 집합론)의 무모순성을 유한수학(유한적 방법)으로 증명하고자 하였다. 제2 불완전성 정리에 의해, 유한적 방법이 PA보다 약한(또는 동등한) 체계에 의해 형식화 가능하다면, PA의 무모순성을 유한적 방법으로 증명하는 것은 불가능하다.

2.3 겐첸의 무모순성 증명

겐첸(Gerhard Gentzen)은 1936년 초한 귀납법(Transfinite Induction up to $\epsilon_0$ )을 사용하여 PA의 무모순성을 증명하였다. 이 증명은 PA 자체보다 강력한 원리(초한 귀납법)를 사용하므로, 제2 불완전성 정리에 모순되지 않는다.

겐첸의 결과는 PA의 무모순성이 “증명 불가능“이 아니라 “PA 내에서 증명 불가능“이라는 정밀한 구분을 예시한다.

3. 인공지능에 대한 함의

제2 불완전성 정리에 의해, 인공지능 체계가 자기 자신의 정확성(무모순성)을 검증하는 것에 원리적 한계가 존재한다. 충분히 강력한 인공지능 체계는 자기 자신이 “올바르게 작동한다“는 것을 자기 자신의 추론 능력만으로 증명할 수 없다. 이는 AI 안전성(AI Safety)과 AI 정렬(AI Alignment)에 관한 이론적 도전을 제기한다.