5.15 ω-무모순성(ω-consistency) 조건과 로서의 강화

1. ω-무모순성의 정의

1.1 형식적 정의

형식 체계 \mathcal{F}\omega-무모순(\omega-Consistent)하다 함은, 어떤 공식 \phi(x)에 대해서도 다음의 상황이 발생하지 않음을 의미한다:

\mathcal{F} \vdash \phi(\overline{0}), \quad \mathcal{F} \vdash \phi(\overline{1}), \quad \mathcal{F} \vdash \phi(\overline{2}), \quad \ldots

이면서 동시에

\mathcal{F} \vdash \exists x \, \neg\phi(x)

형식적으로:

\omega\text{-Con}(\mathcal{F}) \equiv \neg\exists \phi \, [\forall n \in \mathbb{N} \, (\mathcal{F} \vdash \phi(\overline{n})) \wedge \mathcal{F} \vdash \exists x \, \neg\phi(x)]

직관적 의미

\omega-무모순성은 \mathcal{F}가 자연수에 관해 “합리적“으로 행동함을 보장한다. \phi(x)가 모든 구체적 자연수에 대해 증명 가능하면, \mathcal{F}는 “\phi를 만족하지 않는 수가 존재한다“를 증명하지 않는다.

무모순성과의 관계

\omega\text{-무모순성} \implies \text{무모순성}

증명: \mathcal{F}가 무모순하지 않다면, 모든 문장이 증명 가능하므로 \forall n (\mathcal{F} \vdash \phi(\overline{n}))\mathcal{F} \vdash \exists x \neg\phi(x)가 동시에 성립한다. 따라서 \omega-무모순하지도 않다.

역은 성립하지 않는다. 무모순하지만 \omega-무모순하지 않은 체계가 존재한다.

1.2 \omega-무모순하지 않지만 무모순한 체계의 예

PA가 무모순이라고 가정하면, PA + \neg G (PA에 괴델 문장의 부정을 추가한 체계)는 무모순하다(G가 PA에서 결정 불가능하므로). 그러나 이 체계는 \omega-무모순하지 않다.

PA + \neg G에서:

  • \neg G \equiv \text{Prov}(\ulcorner G \urcorner) \equiv \exists x \, \text{Prf}(x, \ulcorner G \urcorner)가 공리이므로 증명 가능.
  • 그러나 PA \nvdash G이므로 실제 증명이 존재하지 않아, 모든 구체적 자연수 m에 대해 \text{Prf}(\overline{m}, \ulcorner G \urcorner)가 거짓이고, 따라서 \mathcal{F} \vdash \neg\text{Prf}(\overline{m}, \ulcorner G \urcorner).

이 상황은 정확히 \omega-무모순성의 위반이다.

2. 괴델 원래 증명에서 ω-무모순성의 역할

괴델의 1931년 원래 증명에서, \neg G의 증명 불가능성(\mathcal{F} \nvdash \neg G)을 보이는 부분(부분 2)에서 \omega-무모순성이 사용된다.

핵심 추론: \mathcal{F} \nvdash G로부터 모든 m에 대해 \mathcal{F} \vdash \neg\text{Prf}(\overline{m}, \ulcorner G \urcorner)가 도출된다. 만약 \mathcal{F} \vdash \neg G이면 \mathcal{F} \vdash \exists x \, \text{Prf}(x, \ulcorner G \urcorner)이 도출된다. 이 두 결과의 공존이 \omega-무모순성에 모순된다.

3. 로서의 강화(Rosser’s Improvement, 1936)

3.1 동기

\omega-무모순성은 단순 무모순성보다 강한 조건이며, 직접 검증하기 어렵다. 로서(J. Barkley Rosser)는 1936년 “Extensions of Some Theorems of Gödel and Church“에서 괴델 문장을 변형하여 단순 무모순성만으로도 결정 불가능 문장의 존재를 증명하였다.

3.2 로서 문장(Rosser Sentence)의 구성

로서는 괴델 문장 G \leftrightarrow \neg\text{Prov}(\ulcorner G \urcorner)를 다음과 같이 변형하였다.

대각화 보조 정리를 다음의 속성 \rho(x)에 적용한다:

\rho(x) \equiv \forall y \, (\text{Prf}(y, x) \rightarrow \exists z \leq y \, \text{Prf}(z, \text{neg}(x)))

여기서 \text{neg}(x)는 괴델 수 x를 가진 공식의 부정의 괴델 수를 반환하는 함수이다.

대각화에 의해 로서 문장 R을 구성한다:

\mathcal{F} \vdash R \leftrightarrow \forall y \, (\text{Prf}(y, \ulcorner R \urcorner) \rightarrow \exists z \leq y \, \text{Prf}(z, \ulcorner \neg R \urcorner))

3.3 로서 문장의 의미

R은 다음을 말한다: “만약 R의 증명이 존재한다면, 그 증명보다 작거나 같은 괴델 수를 가진 \neg R의 증명이 존재한다.”

더 직관적으로: “R이 증명 가능하다면, \neg R이 먼저(또는 동시에) 증명 가능하다.” 이는 “R이 먼저 증명되는 것은 불가능하다“는 내용으로, “R은 증명 불가능하다“의 정교화이다.

3.4 로서 정리의 증명 개요

\mathcal{F} \nvdash R의 증명:

\mathcal{F} \vdash R이라 가정. R의 증명 \pi의 괴델 수 m에 대해 \mathcal{F} \vdash \text{Prf}(\overline{m}, \ulcorner R \urcorner). R의 정의에 의해 \mathcal{F} \vdash \exists z \leq \overline{m} \, \text{Prf}(z, \ulcorner \neg R \urcorner). 한편, \mathcal{F}가 무모순이므로 \neg R의 증명이 존재하지 않아, 모든 z \leq m에 대해 \mathcal{F} \vdash \neg\text{Prf}(\overline{z}, \ulcorner \neg R \urcorner). z \leq m이 유한 범위이므로 \mathcal{F} \vdash \neg\exists z \leq \overline{m} \, \text{Prf}(z, \ulcorner \neg R \urcorner). 모순. 따라서 \mathcal{F} \nvdash R.

\mathcal{F} \nvdash \neg R의 증명:

\mathcal{F} \vdash \neg R이라 가정. 유사한 논증에 의해 모순이 도출된다. \neg R의 증명의 괴델 수 m'에 대해, R의 정의의 대우를 사용하면 m'보다 작은 R의 증명의 부재로부터 모순이 도출된다.

3.5 로서 강화의 의의

로서의 강화에 의해 제1 불완전성 정리의 전제 조건이 \omega-무모순성에서 단순 무모순성으로 약화된다. 이는 정리의 적용 범위를 확장하며, 무모순한 모든 충분히 강력한 형식 체계에서 결정 불가능 문장이 존재함을 보장한다.

4. ω-무모순성의 현대적 위상

현대 수리논리학에서 \omega-무모순성은 괴델의 원래 증명의 역사적 조건으로서의 의의를 갖지만, 로서의 강화 이후 제1 불완전성 정리의 표준 진술에서는 단순 무모순성이 사용된다. \omega-무모순성은 제2 불완전성 정리, 뢰브의 정리(Löb’s Theorem), 산술 계층의 분석 등에서 여전히 중요한 개념적 역할을 수행한다.