수학에는 참이지만
증명할 수 없는
사실이 있을까?

증명을 숫자로 검사하기

구체적인 증명과 증명 전체를 구분합니다.

4. 정답을 찾는 일과 이미 적힌 증명을 검사하는 일부터 구별합시다

한 연구자가 아주 긴 산술 증명을 제출했다고 생각해 봅시다. 검토자는 각 줄이 공리이거나, 앞의 몇 줄에서 허용된 규칙에 따라 나왔는지 확인할 수 있습니다. 이론과 증명의 표기법이 충분히 명확하면 검사 절차 자체를 수학적으로 정의할 수 있습니다. 어떤 증명이 유한하게 제시되었을 때 그 증명서의 합법성을 확인하는 문제입니다.

이제 연구자가 “이 식의 증명은 존재하나요?”라고 질문했다고 합시다. 길이 1인 후보, 길이 2인 후보, 길이 3인 후보를 차례로 열거하면서 각 후보를 검사할 수 있습니다. 증명이 존재한다면 적절히 설계된 탐색에서는 언젠가 그 증명을 발견합니다. 그러나 증명이 존재하지 않을 때, 후보를 계속 검사하는 절차는 언제 중단해야 할지 알기 어려울 수 있습니다. 증명 하나를 발견하는 일과 가능한 모든 유한한 증명이 없음을 판단하는 일은 서로 다른 문제입니다.

괴델이 사용하는 부호화는 이 검사를 산술 문제로 옮깁니다. 증명은 문자로 쓰여 있지만, 문자의 배열을 자연수로 나타내면 “번호가 붙은 이 배열이 올바른 증명인가”를 자연수들의 관계로 표현할 수 있습니다. 여기서 숫자로 바뀌는 것은 증명의 내용과 구조를 기록한 기호 배열입니다. 자연수를 표현하는 힘이 있는 이론에서는 그런 기록을 다루는 규칙까지 산술식으로 나타낼 수 있습니다.

5. 글자를 숫자로 바꾸어도 증명의 규칙이 남을까요?

간단한 부호화 하나를 직접 만들어 보겠습니다. 기호 0에는 코드 1을, 기호 S에는 코드 2를 붙입니다. 여기서 S는 다음 자연수를 만드는 연산 기호입니다. 따라서 S0는 자연수 1을 나타내는 짧은 표현이고, 0S는 이 표기법에서 올바른 산술항이 아니지만 문자 두 개를 거꾸로 나열한 배열로 생각할 수 있습니다. 이 예시에서는 문자 배열을 구분하는 기능만 검사합니다.

배열의 첫째 자리 코드를 a, 둘째 자리 코드를 b라고 합시다. 첫 번째 소수 2의 지수에 a+1을, 두 번째 소수 3의 지수에 b+1을 넣어 번호를 정합니다. 그러면 두 글자 배열에는 N(a,b) = 2^(a+1) × 3^(b+1)이라는 번호가 붙습니다. 지수에 1을 더하는 이유는 코드가 0인 경우가 생겨도 자리의 정보를 안정적으로 남기는 일반화된 규칙을 생각하기 쉽도록 하기 위해서입니다. 이번 두 기호의 코드는 이미 1과 2이므로 이 설명은 부호화 방식의 원리를 밝혀 줍니다.

S0의 코드는 (2,1)이므로 번호는 2³ × 3² = 8 × 9 = 72입니다. 0S의 코드는 (1,2)이므로 번호는 2² × 3³ = 4 × 27 = 108입니다. 배열에 들어간 기호 두 개는 같아도 순서가 다르면 번호가 달라집니다. 소인수분해의 유일성 덕분에 72에서 2의 지수는 3, 3의 지수는 2라는 정보를 다시 찾을 수 있습니다. 그래서 주어진 부호화 규칙을 알고 있으면 원래 배열을 복원할 수 있습니다.

기호가 셋 이상일 때는 세 번째 자리에 5, 네 번째 자리에 7처럼 차례로 다른 소수를 쓰면 됩니다. 더 복잡한 기호와 괄호, 변수, 공리, 증명 줄 전체를 다루려면 그에 맞는 코딩을 세밀하게 정의해야 합니다. 핵심은 유한한 기호 배열을 자연수로 구별하여 기록하고, 그 배열을 다시 읽어 원래의 추론 규칙에 맞는지 검사할 수 있다는 사실입니다. 임의로 큰 수를 실제 종이에 적어야 정리가 성립하는 것은 아닙니다. 부호화와 검사 절차의 존재를 수학적으로 보여 주면 충분합니다.

증명 가능성을 산술로 나타내기

증명의 번호와 문장의 번호를 연결합니다.

6. 이제 자연수에 대해 ‘이것은 증명 번호다’라고 물을 수 있습니다

형식 이론 T의 문장 A에도 번호가 붙었다고 합시다. 그 번호를 ⌜A⌝라고 씁니다. 증명 전체에도 번호 p를 붙입니다. 그러면 Proof_T(p,⌜A⌝)는 “자연수 p가 T의 규칙에 맞게 쓰인 A의 증명 번호다”라는 관계를 나타냅니다. 왼쪽의 p는 증명에 붙은 번호이고, 오른쪽의 ⌜A⌝는 그 증명이 마지막에 얻어야 할 문장 A의 번호입니다. 두 번호의 역할을 바꾸면 뜻도 달라집니다.

Prov_T(⌜A⌝)의 앞부분 Prov는 프로버빌리티(provability, 증명 가능성)를 나타냅니다. 이 관계는 “T에서 A를 증명하는 유한한 기호 기록이 존재한다”라는 뜻입니다. 자연수에 관한 공리와 계산을 충분히 표현하는 이론에서는 증명의 구문적 성질이 산술 안에 구현되도록 부호화할 수 있습니다. 이 과정은 단순히 숫자로 바꾸는 것에서 끝나지 않습니다. T가 내부에서 필요한 계산을 표현하고 검증할 수 있도록 증명 관계를 정확히 구성해야 합니다.

여기서 주의할 점이 있습니다. “A가 표준 자연수에서 참이다”라는 판정과 “A의 증명 번호가 존재한다”라는 관계는 다른 것입니다. 괴델의 구성은 참 자체를 숫자로 나타내는 만능 판정표를 먼저 가정하지 않습니다. 계산 가능한 증명의 규칙과 그 기록을 수로 나타냅니다. 그래서 산술 안에서 증명 가능성에 관해 언급하는 일이 가능해집니다.

7. 문장이 자기 자신의 번호를 다룰 수 있다는 것은 무슨 뜻일까요?

이제 가장 중요한 기술을 소개하겠습니다. 산술식 Φ(x)가 하나 있고, x 자리에 문장의 번호를 넣을 수 있다고 합시다. x는 특정한 자연수가 아직 정해지지 않은 자리입니다. 예를 들어 Φ(x)가 “번호 x를 가진 문장은 T에서 증명되지 않는다”라는 성질을 표현한다고 생각할 수 있습니다. 괴델이 다룬 논리적 과제는 어떤 문장 G를 만들어 Φ(⌜G⌝)와 같은 내용을 표현하도록 할 수 있는가였습니다.

이것은 단순한 언어 유희가 아닙니다. 문장의 기호 배열을 자연수로 바꾸는 규칙, 어떤 수를 식의 빈자리에 집어넣는 절차, 그 결과로 얻어진 식의 번호를 계산하는 절차를 산술 안에서 표현할 수 있어야 합니다. 이 작업이 가능한 체계에서 사용하는 정리가 대각화 보조정리(diagonalization lemma, 자기 번호를 대입하는 문장 구성 정리)입니다. 적절한 조건의 산술 이론 T와 한 변수 공식 Φ(x)가 주어지면 다음과 같은 문장 G를 구성할 수 있습니다.

G는 자기 이름을 일상 언어로 적어 넣은 문장이 아닙니다. G의 번호를 이용해 조립한 산술식입니다. 기호의 순서와 대입 규칙이 명확하면 그 조립을 실제 계산 대상으로 만들 수 있습니다. 이 점이 고대의 자기언급 역설과 괴델의 엄밀한 논리적 구성을 가르는 핵심입니다.

이제 Φ(x)를 ¬Prov_T(x)로 정합니다. 그러면 어떤 문장 G_T에 대해 T ⊢ G_T ↔ ¬Prov_T(⌜G_T⌝)를 얻습니다. 오른쪽은 “G_T라는 문장의 증명이 T 안에 존재하지 않는다”라는 뜻입니다. 왼쪽은 그것과 동치인 산술 문장 G_T입니다. 우리가 흔히 “괴델 문장”이라고 부르는 대상이 이와 같은 방식으로 만들어집니다.

괴델 문장의 두 방향을 따지기

무모순성과 오메가 무모순성의 역할을 구분합니다.

8. T가 G_T를 증명했다고 가정하면 무엇이 생길까요?

불완전성을 보여 주려면 실제로 추론을 전개해야 합니다. T가 무모순적이라고 가정하고, 반대로 T 안에 G_T의 증명이 하나 존재한다고 해 보겠습니다. 그 증명에는 어떤 자연수 번호 p가 있습니다. 우리가 정한 검증 절차는 p가 정말 G_T의 증명 번호라는 것을 확인합니다. 필요한 기초 산술을 표현하는 T는 이 사실을 내부에서도 확인할 수 있도록 설계되었습니다. 따라서 T에서는 Prov_T(⌜G_T⌝)도 증명할 수 있습니다.

그런데 앞 단계에서 T ⊢ G_T ↔ ¬Prov_T(⌜G_T⌝)라는 관계를 이미 얻었습니다. T에서 G_T를 증명했다는 가정을 넣으면 T에서는 ¬Prov_T(⌜G_T⌝)도 증명할 수 있습니다. 결국 같은 이론 T에서 Prov_T(⌜G_T⌝)와 그 부정을 모두 얻게 됩니다. 이는 무모순성 가정과 충돌합니다.

따라서 무모순적인 T에서는 T ⊬ G_T입니다. 이 결론은 “우리에게 지금 증명이 발견되지 않았다”라는 경험적 보고보다 강합니다. 이론의 공리와 규칙을 제대로 지키는 유한한 증명이 존재할 수 없다는 일반적인 논증입니다. 다만 여기까지의 추론으로는 아직 T ⊬ ¬G_T를 얻었다고 말할 수 없습니다. 어떤 문장을 증명할 수 없다는 사실만으로 그 부정도 증명할 수 없다는 결론이 자동으로 따라오지는 않기 때문입니다.

9. G_T의 부정도 증명할 수 없을까요? 원래 증명의 중요한 조건

¬G_T의 뜻을 앞의 동치식을 이용해 풀어 보면, 이론 T에 G_T의 증명 번호가 적어도 하나 존재한다는 주장과 연결됩니다. 앞 단계에서는 T가 무모순이라면 실제의 유한한 G_T 증명이 존재하지 않는다고 보았습니다. 외부에서 각 자연수 p를 하나씩 살펴보면 어느 p도 G_T의 올바른 증명 번호가 될 수 없습니다. T는 개별 표준 자연수 번호에 관한 그런 계산 사실을 확인할 수 있습니다.

그러나 여기에는 한 가지 구별이 있습니다. 모든 구체적인 자연수 p마다 ‘p는 증명 번호가 아니다’라는 식을 따로 증명하는 일과, ‘어떤 p는 증명 번호다’라는 존재문을 이론 안에서 반박하는 일은 서로 다른 논리적 작업입니다. 무한한 개수의 개별 검산을 모두 모아 놓았다고 해서, 그 결과를 한 줄의 전칭 명제로 얻는 방법이 자동으로 주어지는 것은 아닙니다.

괴델의 1931년 원래 형태는 G_T와 그 부정의 증명 불가능성을 얻기 위해 오메가 무모순성(ω-consistency)이라는 더 강한 성질을 사용했습니다. 대략 한 공식 P(x)에 대하여 각 표준 자연수 n마다 ¬P(n)을 증명해 놓고 동시에 ∃xP(x)도 증명하는 상황을 배제하는 조건입니다. 이는 보통의 무모순성보다 강합니다. 개별 자연수에 관한 모든 검증과 존재문 사이에 예상 밖의 충돌을 허용하지 않는다는 요구이기 때문입니다.

1931년의 논증과 1936년 이후의 개선을 한 가지 가정으로 뭉뚱그리면 원전의 중요한 조건을 놓칩니다. 현대 교과서에서는 첫 번째 불완전성 정리를 단지 무모순성만 가정한 형태로 제시하는 일이 많은데, 거기에는 후속 연구의 성과가 포함되어 있습니다.

로서의 개선과 자기 무모순성

1936년 개선과 제2불완전성 정리의 조건을 읽습니다.

10. 1936년 로서는 무엇을 바꾸었을까요?

존 바클리 로서(J. Barkley Rosser, 1907–1989, 논리학자·수학자, 미국)는 1936년 논문에서 괴델의 방법을 개선했습니다. 문장의 증명이 있는지만 묻는 대신, 그 문장을 증명하는 번호와 그 부정을 증명하는 번호 가운데 어느 쪽이 먼저 나타나는지를 비교하는 특별한 증명 가능성 관계를 사용했습니다. 이 비교에서 ‘먼저’는 역사 속에 누가 먼저 발표했는지가 아니라, 정해진 부호화에서 증명 번호의 자연수 크기를 가리킵니다.

쉽게 이해하기 위해 두 증명 후보의 검증표를 상상해 봅시다. 어떤 명제 A의 증명 후보와 ¬A의 증명 후보를 번호 순서로 검사합니다. 한쪽의 증명이라고 인정할 때, 그보다 번호가 작은 반대쪽 증명이 있는지도 확인합니다. 이 과정은 규칙에 따라 검산할 수 있는 유한한 번호들에 대한 비교를 사용합니다. 로서는 이 비교 성질을 산술화하고 대각화를 적용해 특별한 문장 R_T를 만듭니다.

이 정리는 “무모순이면 아무 문장이나 결정할 수 없다”는 뜻은 아닙니다. 자연수 7 + 5 = 12 같은 많은 식은 여전히 증명할 수 있습니다. 정확한 결론은 해당 조건을 갖춘 모든 무모순적인 이론 T마다, 그 이론에서 결정할 수 없는 문장 적어도 하나가 존재한다는 것입니다. 그 문장이 매번 똑같을 필요도 없습니다. 이론의 공리를 바꾸면 증명 가능성과 자기언급을 구성하는 문장도 함께 달라집니다.

11. 두 번째 불완전성 정리는 ‘무모순성 증명’을 어디까지 제한할까요?

제10회에서는 힐베르트가 산술과 수학의 무모순성을 밝히려 했던 과정을 살펴보았습니다. 이제 괴델의 제2불완전성 정리를 그 질문에 연결해 보겠습니다. T의 무모순성을 표현하기 위해 0 = 1과 같은 분명한 모순식을 ⊥라고 정합니다. 그리고 Con(T)를 “T에서 ⊥를 증명하는 번호는 존재하지 않는다”라는 산술 문장으로 정의합니다. ⊥를 어떻게 선택하고 무모순성을 어떻게 형식화하는지도 정확히 규정해야 합니다.

여기서 중요한 추가 요건이 있습니다. “어떤 증명 번호가 있다”라는 술어는 마음대로 정의한 아무 식이면 되는 것이 아닙니다. 제2정리의 표준 증명에는 증명 가능성 술어가 증명된 정리를 다시 ‘증명 가능하다’고 표현하고, 그런 표현에 대해 내부에서 추론할 수 있다는 도출 가능성 조건들이 필요합니다. 후대에 정리된 뢰프의 조건(Löb's derivability conditions, 형식화된 증명 가능성을 다루는 조건)이 널리 사용됩니다. 다음 식은 그 조건을 충족하는 표준적인 구성에서 얻는 핵심 관계입니다.

따라서 위 조건을 갖춘 무모순적인 T에는 T ⊬ Con(T)가 성립합니다. 여기서 부정되는 것은 T가 자신의 표준적인 무모순성 문장을 T 자신의 공리와 규칙만으로 증명할 수 있다는 주장입니다. 더 강한 이론 U에서 T의 무모순성을 증명하는 일까지 금지하는 정리가 아닙니다. 예를 들어 어떤 더 강한 이론에서 약한 산술 체계의 무모순성을 증명할 수 있는 경우들이 있습니다. 다만 그 증명은 사용한 강한 이론의 근거가 무엇인지 다시 묻게 합니다.

제2정리는 1931년의 괴델 연구에 포함되어 있지만, 오늘날 쓰는 정교한 증명 가능성 조건과 표준 교과서의 전개는 후대에 다듬어졌습니다. 따라서 지금 적은 두 식은 원전의 문장을 그대로 옮긴 인용이 아니라, 역사적 성과를 현대적 형식으로 설명한 것입니다.

이 정리는 어디에 적용할까?

작은 체계와 충분한 산술을 표현하는 이론을 구별합니다.

12. 작은 체계에서는 무모순성을 증명했는데, 왜 여기서는 어려울까요?

제10회의 작은 체계에는 p, p→q, q→r 같은 몇 개의 공리와 전건 긍정이라는 규칙 하나만 있었습니다. 모든 공리를 참으로 만드는 해석을 찾고 그 규칙이 참을 보존한다는 것을 보이면 무모순성을 설명할 수 있었습니다. 이 작은 체계는 자기 자신의 증명 관계와 대각화 구성에 필요한 산술을 충분히 표현하지 못합니다. 그러므로 제2불완전성 정리의 적용 조건을 갖춘 체계와 같은 것으로 취급하면 안 됩니다.

산술을 충분히 표현하는 큰 이론에 대해서도 외부에서 모형을 만들거나 더 강한 원리를 사용해 무모순성을 논의할 수 있습니다. 그러나 외부의 논증을 그대로 해당 이론 안의 증명으로 옮길 수 있는지는 따로 검사해야 합니다. ‘어떤 수학적 이유로 T가 무모순임을 안다’와 ‘T ⊢ Con(T)’의 차이가 여기서 드러납니다.

역사적으로 겐첸은 1936년에 산술의 무모순성과 관련된 증명을 제시하면서 특별한 초한귀납법을 활용했습니다. 그 논증의 강도와 힐베르트의 원래 유한주의 요구 사이의 관계는 중요한 연구 주제입니다. 괴델의 제2정리는 이 같은 후속 연구를 쓸모없게 만든 것이 아니라 증명에 동원된 원리의 강도를 따져 보도록 요구합니다. 제10회가 무모순성 계획 자체를 중심으로 설명했다면, 이번에는 왜 이 구분이 논리적으로 필요해지는지를 자기언급의 구조에서 확인한 것입니다.