5.18 제2 불완전성 정리의 증명 개요와 힐베르트-베르나이스 도출 가능성 조건

1. 제2 불완전성 정리의 증명 전략

제2 불완전성 정리의 증명은 제1 불완전성 정리의 증명을 형식 체계 $\mathcal{F}$ 내부에서 형식화(Formalize)하는 것에 기반한다. 제1 불완전성 정리의 증명에서 핵심 단계인 “만약 $\mathcal{F}$ 가 무모순이면, 괴델 문장 $G$ 는 $\mathcal{F}$ 에서 증명 불가능하다“를 $\mathcal{F}$ 내부의 산술적 문장으로 표현하고 증명하면, $\text{Con}(\mathcal{F}) \rightarrow G$ 가 $\mathcal{F}$ 에서 증명 가능해진다. $\mathcal{F} \nvdash G$ (제1 불완전성 정리)이므로, $\mathcal{F} \nvdash \text{Con}(\mathcal{F})$ 가 따른다.

이 형식화가 성공하려면, 증명 가능성 술어 $\text{Prov}$ 가 증명 가능성의 기본 성질을 $\mathcal{F}$ 내에서 올바르게 반영해야 한다. 이 요구사항을 정밀하게 기술한 것이 힐베르트-베르나이스 도출 가능성 조건이다.

2. 힐베르트-베르나이스 도출 가능성 조건(Derivability Conditions)

힐베르트(David Hilbert)와 베르나이스(Paul Bernays)가 “Grundlagen der Mathematik”(1939)에서 제시하고, 뢰브(Martin Löb)가 정리화한 세 조건이다.

2.1 조건 D1 ( $\Sigma_1$ -완전성)

$\text{if } \mathcal{F} \vdash \phi, \text{ then } \mathcal{F} \vdash \text{Prov}(\ulcorner \phi \urcorner)$

$\mathcal{F}$ 에서 증명 가능한 모든 문장 $\phi$ 에 대해, “ $\phi$ 가 증명 가능하다“는 사실이 $\mathcal{F}$ 내에서 증명 가능하다. 이 조건은 증명의 존재가 $\mathcal{F}$ 내부에서 확인 가능함을 보장한다.

검증: $\mathcal{F} \vdash \phi$ 이면, 실제 증명 $\pi$ 가 존재하고, 그 괴델 수 $m = \ulcorner \pi \urcorner$ 에 대해 $\text{Proof}(m, \ulcorner \phi \urcorner)$ 가 참이다. $\text{Prf}$ 가 원시 재귀적 관계를 표현하므로 $\mathcal{F} \vdash \text{Prf}(\overline{m}, \ulcorner \phi \urcorner)$ 이고, 존재 양화에 의해 $\mathcal{F} \vdash \exists x \, \text{Prf}(x, \ulcorner \phi \urcorner) = \text{Prov}(\ulcorner \phi \urcorner)$ .

조건 D2 (분배성, Distributivity)

$\mathcal{F} \vdash \text{Prov}(\ulcorner \phi \rightarrow \psi \urcorner) \rightarrow (\text{Prov}(\ulcorner \phi \urcorner) \rightarrow \text{Prov}(\ulcorner \psi \urcorner))$

조건문의 증명 가능성이, 전건의 증명 가능성으로부터 후건의 증명 가능성을 도출하는 것을 $\mathcal{F}$ 내부에서 증명할 수 있다. 이 조건은 전건 긍정(Modus Ponens)의 형식화가 $\mathcal{F}$ 내부에서 가능함을 보장한다.

직관적 의미: “ $\phi \rightarrow \psi$ 의 증명이 있고 $\phi$ 의 증명이 있으면, 이 두 증명을 결합하여 $\psi$ 의 증명을 구성할 수 있다“는 메타수학적 사실을 $\mathcal{F}$ 내부에서 형식적으로 증명할 수 있다.

2.2 조건 D3 (형식적 반영, Formal Reflection)

$\mathcal{F} \vdash \text{Prov}(\ulcorner \phi \urcorner) \rightarrow \text{Prov}(\ulcorner \text{Prov}(\ulcorner \phi \urcorner) \urcorner)$

증명 가능성의 증명 가능성을 $\mathcal{F}$ 내에서 증명할 수 있다. “만약 $\phi$ 가 증명 가능하면, ’ $\phi$ 가 증명 가능하다’도 증명 가능하다.”

이 조건은 D1의 형식화이다. D1은 메타수학적 진술(“ $\mathcal{F} \vdash \phi$ 이면 $\mathcal{F} \vdash \text{Prov}(\ulcorner \phi \urcorner)$ ”)이지만, D3는 이를 $\mathcal{F}$ 내부의 문장으로 표현한다.

검증의 기술적 어려움: D3의 검증은 D1, D2에 비해 기술적으로 가장 복잡하다. $\text{Prov}(\ulcorner \phi \urcorner)$ 의 증명이 존재할 때, 이 증명의 존재를 다시 증명하는 것을 $\mathcal{F}$ 내에서 수행해야 하며, 이는 $\Sigma_1$ -완전성의 형식화를 요구한다.

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

단계 1: 괴델 문장의 성질

대각화 보조 정리에 의해:

$\mathcal{F} \vdash G \leftrightarrow \neg\text{Prov}(\ulcorner G \urcorner) \quad \cdots (*)$

2.3 단계 2: $\text{Con}(\mathcal{F}) \rightarrow G$ 의 $\mathcal{F}$ 내 증명

$\text{Con}(\mathcal{F}) \equiv \neg\text{Prov}(\ulcorner \bot \urcorner)$ 이며, $\bot$ 은 $0 = S(0)$ 과 같은 거짓 문장이다.

제1 불완전성 정리의 부분 1 증명을 $\mathcal{F}$ 내부에서 형식화한다:

(a) $(*)$ 에 의해 $\mathcal{F} \vdash G \leftrightarrow \neg\text{Prov}(\ulcorner G \urcorner)$ .

(b) 대우: $\mathcal{F} \vdash \text{Prov}(\ulcorner G \urcorner) \rightarrow \neg G$ .

(d) D1을 형식화(D3 사용)하여: $\mathcal{F} \vdash \text{Prov}(\ulcorner G \urcorner) \rightarrow \text{Prov}(\ulcorner \text{Prov}(\ulcorner G \urcorner) \urcorner)$ .

(e) (b)에 D1 적용(D2 사용)하여: $\mathcal{F} \vdash \text{Prov}(\ulcorner G \urcorner) \rightarrow \text{Prov}(\ulcorner \neg G \urcorner)$ .

(f) (d)와 (e)를 결합: $\mathcal{F} \vdash \text{Prov}(\ulcorner G \urcorner) \rightarrow (\text{Prov}(\ulcorner G \urcorner) \wedge \text{Prov}(\ulcorner \neg G \urcorner))$ .

(g) $\text{Prov}(\ulcorner G \urcorner) \wedge \text{Prov}(\ulcorner \neg G \urcorner)$ 는 무모순성의 부정이므로:
$\mathcal{F} \vdash \text{Prov}(\ulcorner G \urcorner) \rightarrow \neg\text{Con}(\mathcal{F})$

(h) 대우: $\mathcal{F} \vdash \text{Con}(\mathcal{F}) \rightarrow \neg\text{Prov}(\ulcorner G \urcorner)$ .

(i) $(*)$ 에 의해 $\neg\text{Prov}(\ulcorner G \urcorner) \leftrightarrow G$ 이므로:
$\mathcal{F} \vdash \text{Con}(\mathcal{F}) \rightarrow G$

2.4 단계 3: 결론

$\mathcal{F}$ 가 무모순이면, 제1 불완전성 정리에 의해 $\mathcal{F} \nvdash G$ 이다. 단계 2에서 $\mathcal{F} \vdash \text{Con}(\mathcal{F}) \rightarrow G$ 이므로, 만약 $\mathcal{F} \vdash \text{Con}(\mathcal{F})$ 이면 전건 긍정에 의해 $\mathcal{F} \vdash G$ 가 되어 모순이다. 따라서:

$\mathcal{F} \nvdash \text{Con}(\mathcal{F}) \quad \blacksquare$

도출 가능성 조건의 사용 위치

조건	증명에서의 사용 위치
D1	단계 2(a)에서 구체적 증명 존재의 $\mathcal{F}$ 내 확인
D2	단계 2(e)에서 전건 긍정의 형식화
D3	단계 2(d)에서 증명 가능성 자체의 증명 가능성 형식화

D1만으로는 제1 불완전성 정리의 증명에 충분하지만, D2와 D3는 이 증명을 $\mathcal{F}$ 내부에서 형식화하는 데 필수적이다. 제2 불완전성 정리가 제1 불완전성 정리보다 기술적으로 더 어려운 이유가 여기에 있다.

뢰브의 정리(Löb’s Theorem)

도출 가능성 조건의 중요한 귀결이 뢰브의 정리(Löb’s Theorem, 1955)이다.

정리: $\mathcal{F} \vdash \text{Prov}(\ulcorner \phi \urcorner) \rightarrow \phi$ 이면 $\mathcal{F} \vdash \phi$ .

의미: “ $\phi$ 가 증명 가능하면 $\phi$ 가 참이다“가 $\mathcal{F}$ 에서 증명 가능하려면, $\phi$ 자체가 $\mathcal{F}$ 에서 증명 가능해야 한다. 이는 $\mathcal{F}$ 가 자기 자신의 건전성(Soundness)을 증명할 수 없음을 의미하며, 제2 불완전성 정리의 일반화이다.

$\phi$ 를 $\bot$ (모순)으로 설정하면: $\mathcal{F} \vdash \text{Prov}(\ulcorner \bot \urcorner) \rightarrow \bot$ 은 $\mathcal{F} \vdash \neg\text{Prov}(\ulcorner \bot \urcorner) = \text{Con}(\mathcal{F})$ 와 동치이다. 뢰브의 정리에 의해 $\mathcal{F} \vdash \bot$ 이어야 하는데, $\mathcal{F}$ 가 무모순이므로 $\mathcal{F} \nvdash \bot$ 이다. 따라서 $\mathcal{F} \nvdash \text{Con}(\mathcal{F})$ . 이는 제2 불완전성 정리의 재도출이다.

도출 가능성 조건의 충족 검증

PA에서 표준적으로 구성한 $\text{Prov}$ 술어가 D1–D3을 모두 만족하는 것의 완전한 검증은 괴델의 1931년 논문에서 수행되지 않았다. 힐베르트와 베르나이스가 1939년 “Grundlagen der Mathematik II“에서 상세한 검증을 수행하였으며, 이 검증은 수백 페이지에 달하는 기술적 작업이다.

현대에는 겐첸(Feferman, 1960)과 부로스(Boolos, 1993) 등이 도출 가능성 조건의 검증을 보다 간결하게 체계화하였다.

도출 가능성 조건의 추상적 관점: 증명 가능성 논리

도출 가능성 조건은 증명 가능성 논리(Provability Logic)의 기반이다. 증명 가능성 논리에서 $\text{Prov}$ 를 양상 연산자(Modal Operator) $\Box$ 로 해석하면:

D1: $\phi$ 이면 $\Box\phi$ (필연화 규칙, Necessitation Rule)
D2: $\Box(\phi \rightarrow \psi) \rightarrow (\Box\phi \rightarrow \Box\psi)$ (분배 공리, Distribution Axiom, K)
D3: $\Box\phi \rightarrow \Box\Box\phi$ (양상 공리 4)

D1–D3을 만족하는 양상 논리 체계는 정규 양상 논리 K4에 해당한다. 솔로비(Robert Solovay)의 산술적 완전성 정리(1976)는 PA의 증명 가능성이 정확히 양상 논리 GL(Gödel-Löb Logic)에 의해 포착됨을 증명하였다.