5.9 메타수학적 술어의 산술화: 증명 가능성의 형식적 표현

5.9 메타수학적 술어의 산술화: 증명 가능성의 형식적 표현

1. 메타수학과 대상 수학의 구분

괴델 증명의 핵심적 혁신은 메타수학적(Metamathematical) 개념을 대상 수학(Object Mathematics) 내에서 표현하는 것이다.

대상 수학: 형식 체계 \mathcal{F} 내에서 수행되는 수학. PA의 정리를 증명하는 것이 대상 수학의 활동이다.

메타수학: 형식 체계 \mathcal{F}에 관한 수학. “\phi는 PA의 정리이다”, “PA는 무모순하다” 등의 진술이 메타수학적 진술이다.

괴델 수 부여에 의해, 메타수학적 술어가 PA의 산술적 공식으로 변환된다. 이 변환에 의해 PA가 자기 자신에 관해 “말하는” 것이 가능해진다.

2. 핵심 메타수학적 술어의 산술화

2.1 증명 술어(Proof Predicate)

메타수학적 의미: “m은 공식 \phi(괴델 수 n)의 PA 증명이다.”

산술적 표현: 원시 재귀적 관계 \text{Proof}(m, n)

이 관계는 다음을 원시 재귀적으로 검사한다:

  1. m이 공식 열의 유효한 괴델 수인지
  2. 열의 각 원소가 PA의 공리이거나 앞선 원소들로부터 추론 규칙에 의해 올바르게 도출되었는지
  3. 열의 마지막 원소가 괴델 수 n을 가진 공식인지

\text{Proof}가 원시 재귀적이므로, PA 내에서 \Delta_0 공식 \text{Prf}(m, n)으로 표현(Represent) 가능하다:

\text{Proof}(a, b) \text{가 참} \iff \text{PA} \vdash \text{Prf}(\overline{a}, \overline{b})
\text{Proof}(a, b) \text{가 거짓} \iff \text{PA} \vdash \neg\text{Prf}(\overline{a}, \overline{b})

2.2 증명 가능성 술어(Provability Predicate)

메타수학적 의미: “괴델 수 n을 가진 공식이 PA에서 증명 가능하다.”

산술적 표현: \text{Prov}(n) \equiv \exists m \, \text{Prf}(m, n)

\text{Prov}는 존재 양화(\exists)를 포함하므로 \Sigma_1^0 공식이다. \text{Prov}는 원시 재귀적이 아니라 RE(Recursively Enumerable)이다.

2.3 핵심 성질

\text{Prov}는 다음의 성질을 만족한다:

  1. PA \vdash \phi이면 PA \vdash \text{Prov}(\ulcorner \phi \urcorner). (증명 가능한 공식의 증명 가능성이 PA 내에서 확인 가능)
  2. PA \nvdash \phi이라 하더라도 PA \nvdash \neg\text{Prov}(\ulcorner \phi \urcorner)일 수 있다. (증명 불가능한 공식의 증명 불가능성은 PA 내에서 확인되지 않을 수 있음)

성질 2는 \text{Prov}\Sigma_1^0이므로, 그 부정이 PA에서 증명 가능하지 않을 수 있기 때문이다.

3. 대입 함수의 산술화

3.1 대입 함수 \text{sub}

공식 \phi(x)의 변수 x에 항 t를 대입한 공식 \phi(t)의 괴델 수를 계산하는 함수:

\text{sub}(\ulcorner \phi(x) \urcorner, \ulcorner x \urcorner, \ulcorner t \urcorner) = \ulcorner \phi(t) \urcorner

\text{sub} 함수는 원시 재귀적이며, PA 내에서 표현 가능하다.

자기 대입 함수 \text{diag}

특히 중요한 것은 자기 대입(Self-Substitution) 또는 대각화(Diagonalization) 함수이다. 공식 \phi(x)의 변수 x에 공식 자체의 괴델 수 \ulcorner \phi(x) \urcorner를 대입하는 함수:

\text{diag}(\ulcorner \phi(x) \urcorner) = \text{sub}(\ulcorner \phi(x) \urcorner, \ulcorner x \urcorner, \overline{\ulcorner \phi(x) \urcorner})
= \ulcorner \phi(\overline{\ulcorner \phi(x) \urcorner}) \urcorner

\text{diag}은 원시 재귀적이며, 괴델 문장의 구성에서 핵심적 역할을 한다.

대각선 보조정리(Diagonal Lemma)

보조정리의 진술

PA의 자유 변수를 하나 가진 임의의 공식 \psi(x)에 대해, 다음을 만족하는 문장 G가 존재한다:

\text{PA} \vdash G \leftrightarrow \psi(\ulcorner G \urcorner)

즉, G는 “자기 자신의 괴델 수가 속성 \psi를 만족한다“와 동치인 문장이다.

3.2 증명의 개요

\psi(x)가 주어졌을 때, 보조 공식 \theta(x)를 다음과 같이 정의한다:

\theta(x) \equiv \psi(\text{diag}(x))

\theta(x)는 “x의 대각화 결과가 속성 \psi를 만족한다“를 표현한다.

이제 G\theta의 대각화로 정의한다:

G \equiv \theta(\overline{\ulcorner \theta(x) \urcorner})
= \psi(\text{diag}(\overline{\ulcorner \theta(x) \urcorner}))
= \psi(\overline{\ulcorner \theta(\overline{\ulcorner \theta(x) \urcorner}) \urcorner})
= \psi(\ulcorner G \urcorner)

따라서 G \leftrightarrow \psi(\ulcorner G \urcorner)이 PA에서 증명 가능하다. \blacksquare

괴델 문장의 구성

대각선 보조정리를 \psi(x) \equiv \neg\text{Prov}(x)에 적용하면, 다음을 만족하는 문장 G가 존재한다:

\text{PA} \vdash G \leftrightarrow \neg\text{Prov}(\ulcorner G \urcorner)

G는 “자기 자신의 괴델 수가 증명 가능하지 않다“와 동치이다. 즉:

G \text{는 "이 문장은 PA에서 증명 불가능하다"를 산술적으로 표현한 문장이다.}

G가 괴델 문장(Gödel Sentence)이며, 불완전성 정리의 핵심 구성물이다.

산술화의 정밀성 조건

괴델 증명이 올바르게 작동하려면 증명 가능성 술어 \text{Prov}가 특정 정밀성 조건을 만족해야 한다. 이 조건은 힐베르트-베르나이스-뢰브 도출 가능성 조건(Hilbert-Bernays-Löb Derivability Conditions)으로 알려져 있다:

D1: PA \vdash \phi이면 PA \vdash \text{Prov}(\ulcorner \phi \urcorner).
D2: PA \vdash \text{Prov}(\ulcorner \phi \rightarrow \psi \urcorner) \rightarrow (\text{Prov}(\ulcorner \phi \urcorner) \rightarrow \text{Prov}(\ulcorner \psi \urcorner)).
D3: PA \vdash \text{Prov}(\ulcorner \phi \urcorner) \rightarrow \text{Prov}(\ulcorner \text{Prov}(\ulcorner \phi \urcorner) \urcorner).

이 세 조건은 \text{Prov}가 증명 가능성의 핵심적 성질을 PA 내에서 올바르게 반영함을 보장한다. 조건 D1은 제1 불완전성 정리에, 조건 D1–D3 모두는 제2 불완전성 정리에 필요하다.

메타수학적 술어 산술화의 이론적 위상

메타수학적 술어의 산술화는 괴델 증명의 기술적 핵심이며, “형식 체계가 자기 자신에 관해 말한다“는 자기 참조의 형식적 실현이다. 이 산술화에 의해 구성되는 괴델 문장이 불완전성 정리의 증명을 완성하며, 형식 체계의 표현력과 한계 사이의 근본적 긴장을 드러낸다.