괴델의 불완전성 정리

3. 정의

다비트 힐베르트는 러셀의 역설 등에서 나타나는 역설이 의미론적인 요소에 기인한다고 보았다. 그는 무의미한 형식 체계를 정의하고 그 안에서 수학적 진술의 참/거짓을 논하고자 했다. 이 체계에서 모든 식은 의미 없는 부호와 기호열로 간주되며, 공리에서 정리를 유도하는 것은 기호열 집합 간의 변환으로 이해된다. 이러한 형식화는 체계의 모든 정리들을 공리로부터 유도하고, 모순되는 두 공식이 동시에 유도될 수 없음을 보여 무모순성을 증명하는 것을 목표로 한다.

형식화 과정은 다음과 같다.

# 사용할 부호 목록 정의 (어휘)

# 문장으로 허용되는 구성 규칙 설정 (문법)

# 공식 간 변환을 위한 추론 규칙 정의

# 체계의 기초가 되는 공리(원시공식) 선택

체계의 '정리'는 변형 규칙을 통해 공리로부터 도출 가능한 공식을, '증명'은 추론 규칙에 따른 공식의 나열을 의미한다.

주세페 페아노 등에 의해 산술화된 유클리드 기하학을 비롯한 일반적인 수학 체계에 대하여, 고틀로프 프레게, 버트런드 러셀 등 논리주의자들은 산술 체계를 논리학 명제로 표현할 수 있다고 보았다. 따라서 수학의 무모순성 문제는 형식논리학의 무모순성 문제로 귀결되었으며, 앨프리드 노스 화이트헤드와 버트런드 러셀은 《수학 원리》에서 순수 수학(산술)의 모든 진술을 형식화하는 방법을 제시했다. 이 표기 체계에 따라 모든 수학 명제를 표준적인 방법으로 코드화할 수 있다.

귀납적으로 공리화 가능한 이론이 자연수론을 포함하면, 해당 이론에서의 증명 가능성은 원시 귀납적 술어로 표현될 수 있다. 이 술어를 이용해 "'''는 증명할 수 없다'''"와 동치인 증명 불가능 명제 ('''괴델 문장''')을 구성할 수 있다. 이를 위해 괴델 수와 자기 지칭에 사용되는 대각화 보조 정리가 필요하다.

자연수를 변수로 하는 술어 "는…이다"의 '''대각화'''는, 술어의 에 "는…이다" 자체의 괴델 수를 대입한 명제이다. 즉, "「는…이다」는…이다"를 의미한다.

괴델 문장 는 다음과 같이 표현된다.

: "「「로 표현되는 술어의 대각화는 증명할 수 없다」로 표현되는 술어의 대각화는 증명할 수 없다」"

"「로 표현되는 술어의 대각화는 증명할 수 없다」"의 대각화는 자신과 동치가 된다.

3. 1. 제1 불완전성 정리

• (유효 생성성) $T$의 공리계와 추론 규칙들은 재귀 열거 집합을 이룬다. 즉, 공리계가 유한하거나, 아니면 튜링 기계로 공리꼴로부터 생성되는 공리들을 열거할 수 있다.
• (일관성) $T$의 공리계로부터 거짓 $\backslash bot$을 증명할 수 없다.
• (산술의 표현 가능성) $T$의 공리계로부터, 페아노 공리계와 동치인 공리들을 증명할 수 있다.
• (산술에 대한 완전성) 자연수에 대한 모든 참인 명제는 $T$로부터 증명할 수 있다.

3. 2. 제2 불완전성 정리

• 『수학 원리』의 체계나 공리적 집합론 중에는 "증명도 반증도 할 수 없는 "자연수론의 명제"가 존재한다.
• 또한, 이들 체계에 공리를 추가해도 공리가 유한 개라면, 앞서 언급한 명제의 존재를 해소할 수 없다.

4. 증명

괴델의 제1 불완전성 정리는 1931년 논문 "프린키피아 마테마티카와 관련된 시스템의 형식적으로 결정 불가능한 명제에 관하여 I"에서 "정리 VI"로 처음 등장했다.^[2] 이 정리의 가정은 이후 로저의 트릭을 사용하여 개선되었다.

제1 불완전성 정리는 어느 정도의 기본 산술을 수행할 수 있는 모든 일관적인 형식적 시스템 F는 불완전하다는 것을 보여준다. 즉, F의 언어에는 F에서 증명하거나 반증할 수 없는 명제가 존재한다. 이러한 증명 불가능한 명제를 "괴델 문장"이라고 부른다. 괴델 문장은 간접적으로 자기 자신을 지칭하도록 설계되었으며, 특정 단계를 거쳐 구성된 문장이 F 내에서 증명될 수 없다고 말한다. 괴델은 시스템 내의 증명 가능성 개념이 괴델 수에 작용하는 산술적 함수를 통해 표현될 수 있음을 증명했다.

괴델은 자신의 논문 서론에서 리처드의 역설과 거짓말쟁이의 역설을 언급한다. 거짓말쟁이의 역설은 "이 문장은 거짓이다"라는 문장으로, 참일 수도 거짓일 수도 없다. 괴델 문장 G는 이와 유사하지만, 진실 대신 증명 가능성으로 대체하여 "G는 시스템 F에서 증명할 수 없다"라고 말한다.

괴델의 불완전성 정리의 원래 증명에는 시스템이 일관적일 뿐만 아니라 ''ω-일관성''이 있다는 가정이 필요했다. 그러나 J. Barkley Rosser^영어는 로저의 트릭을 통해 일관성 가정만으로도 충분하도록 정리를 강화했다.

제2 불완전성 정리는 형식적 시스템 F의 무모순성을 F의 언어 내 공식으로 표현하는 방법에 있어 여러 방식이 존재하며, 모든 방식이 동일한 결과를 가져오지는 않는다는 미묘함을 갖는다. 제2 불완전성 정리의 공식 Cons(F)는 무모순성의 특정한 표현이다.

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

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

• (유효 생성성) $T$의 공리계와 추론 규칙들은 재귀 열거 집합을 이룬다. 즉, 공리계가 유한하거나, 아니면 튜링 기계로 공리꼴로부터 생성되는 공리들을 열거할 수 있다.
• (무모순성) $T$의 공리계로부터 거짓 $\backslash bot$을 증명할 수 없다.
• (산술의 표현 가능성) $T$의 공리계로부터, 페아노 공리계와 동치인 공리들을 증명할 수 있다.
• (제1 정리의 표현 가능성) $T$는 제1 불완전성 정리의 증명을 형식화할 수 있다.
• (무모순성의 증명 가능성) $T$ 속에서, $T$가 무모순적이라는 사실을 증명할 수 있다.

5. 상세

불완전성 정리는 자연수의 기본적인 산술을 표현할 수 있을 만큼 충분히 복잡하고, 일관적이며, 효과적으로 공리화된 형식적 체계에 적용된다. 형식적 체계는 완전성, 일관성, 효과적인 공리화 등의 속성을 가질 수 있는데, 불완전성 정리는 충분한 양의 산술을 포함하는 체계가 이 세 가지 속성을 모두 가질 수 없음을 보여준다.^[5]

괴델의 불완전성 정리 증명 개요도 참고

'''괴델의 제1 불완전성 정리'''는 다음과 같다.

가 어느 정도의 기본 산술을 수행할 수 있는 모든 일관적인 형식적 시스템이라면, 의 언어에는 에서 증명하거나 반증할 수 없는 명제가 존재한다.

증명 불가능한 명제 는 시스템 에 대한 "괴델 문장"이라고 불린다. 시스템 에 대한 특정 괴델 문장을 구성하지만, 괴델 문장과 모든 논리적 타당성 문장의 결합과 같이 동일한 속성을 공유하는 시스템 언어에는 무한히 많은 명제가 있다.

각 효과적으로 생성된 시스템에는 자체 괴델 문장이 있다. 전체에 를 추가 공리로 포함하는 더 큰 시스템 를 정의할 수 있다. 이것은 완전한 시스템을 만들지 못하는데, 괴델의 정리가 에도 적용되기 때문이다. 는 에서 증명할 수 없다고만 말하기 때문에 내에서 증명 가능하다고 해서 모순이 나타나지 않는다. 그러나 불완전성 정리가 에 적용되기 때문에, 에 대한 새로운 괴델 명제 가 있을 것이다. 는 와 달리 가 아닌 를 참조할 것이다.

괴델 문장은 간접적으로 자기 자신을 지칭하도록 설계되었다. 이 문장은 특정 일련의 단계를 사용하여 다른 문장을 구성할 때, 구성된 문장이 내에서 증명될 수 없다고 말한다. 그러나 일련의 단계는 구성된 문장이 자신이 되도록 한다. 이런 식으로 괴델 문장 는 내에서의 자신의 무증명성을 간접적으로 진술한다.

괴델은 "프린키피아 마테마티카와 관련된 시스템 I에서 형식적으로 결정 불가능한 명제에 관하여"의 서론에서 리처드의 역설과 거짓말쟁이의 역설을 언급한다. 거짓말쟁이의 역설은 "이 문장은 거짓이다."라는 문장이다. 거짓말쟁이 문장을 분석하면, 이 문장은 참일 수 없고, 또한 거짓일 수도 없다. 시스템 에 대한 괴델 문장 는 거짓말쟁이 문장과 유사한 주장을 하지만, 진실 대신 증명 가능성으로 대체한다. 는 "는 시스템 에서 증명할 수 없다."라고 말한다.

괴델 문장에서 "증명할 수 없음"을 "거짓"으로 대체하는 것은 불가능하다. "는 거짓 공식의 괴델 수이다"라는 술어는 산술의 공식으로 표현될 수 없기 때문이다. 이 결과는 타르스키의 정의 불가능성 정리로 알려져 있다.

괴델의 불완전성 정리의 원래 진술과 증명에는 시스템이 일관적일 뿐만 아니라 ''ω-일관성''이 있다는 가정이 필요하다. 는 ω-일관성 대신 시스템이 일관적이기만 하면 되는 증명의 변형(로저의 트릭)을 찾아 불완전성 정리를 강화했다. ω-일관성 대신 일관성만을 가정하는 불완전성 정리의 더 강력한 버전은 현재 괴델의 불완전성 정리와 괴델-로저 정리로 일반적으로 알려져 있다.

'''괴델의 제2 불완전성 정리'''는 일반적인 가정 하에서 무모순성 명제 Cons()는 내에서 증명할 수 없음을 보여준다.^[2] 이 정리는 일정한 양의 초등 산술을 수행할 수 있는 모든 무모순적인 시스템 ''F''에 대해 ''F''의 무모순성은 ''F'' 자체 내에서 증명될 수 없다고 말한다.

제2 불완전성 정리에는 의 무모순성을 의 언어 내 공식으로 표현하는 방법에 대한 기술적인 미묘함이 존재한다. 시스템의 무모순성을 표현하는 방법은 많으며, 모든 방법이 동일한 결과를 가져오지는 않는다. 두 번째 불완전성 정리의 공식 Cons()는 무모순성의 특정한 표현이다.

5. 1. 효과적인 공리화

5. 2. 완전성

5. 3. 일관성

5. 4. 산술을 포함하는 체계

6. 결정 불가능 명제의 예

쿠르트 괴델과 폴 코헨의 연구를 통해 결정 불가능한 명제의 예시들이 제시되었다. 연속체 가설은 ZFC(집합론의 표준 공리계)에서 증명하거나 반증할 수 없다.^[1] 또한, 선택 공리는 ZF(ZFC에서 선택 공리를 제외한 공리계)에서 증명하거나 반증할 수 없다.^[1] 1940년 괴델은 이 명제들이 ZF나 ZFC 집합론에서 반증될 수 없음을 보였고, 1960년대 코헨은 이들이 ZF에서 증명될 수 없으며, 연속체 가설은 ZFC에서 증명될 수 없음을 증명했다.^[1]

유리 마차세비치가 힐베르트의 제10문제를 해결하면서 또 다른 결정 불가능한 명제의 예시가 발견되었다.^[1] 이 예시는 디오판토스 방정식의 해의 존재 여부에 관한 것으로, 특정 형식 체계에서는 증명도 반증도 불가능하다.^[1]

1973년에는 군론의 Whitehead problem|화이트헤드 문제^영어가 표준 집합론에서 결정 불가능하다는 것이 밝혀졌다.^[1]

1977년, 파리스와 해링턴은 램지 정리의 일종인 파리스-해링턴 정리가 페아노 산술에서는 결정 불가능하지만, 이차 산술에서는 증명 가능함을 보였다.^[1] 굿스타인 정리는 페아노 산술에서 결정 불가능한 또 다른 예시이다.^[1]

컴퓨터 과학에 응용되는 Kruskal's tree theorem|크루스칼의 트리 정리^영어는 페아노 산술에서 결정 불가능하지만, 집합론에서는 증명 가능하다.^[1] graph minor theorem|그래프 마이너 정리^영어는 계산 복잡도 이론에 영향을 미치는 또 다른 예시이다.^[1]

그레고리 차이틴은 알고리즘 정보 이론에서 결정 불가능한 명제를 발견하고, 차이틴의 불완전성 정리를 제시했다.^[1] 이 정리에 따르면, 충분한 산술을 표현할 수 있는 이론에서는 어떤 수가 특정 값보다 큰 콜모고로프 복잡성을 갖는다는 것을 증명할 수 없다.^[1]

7. 계산 가능성과의 관계

불완전성 정리는 계산 가능성 이론의 몇 가지 결정 불가능 집합에 대한 결과와 밀접하게 관련되어 있다. 어떤 문제를 모든 입력에 대해 올바르게 답하는 알고리즘이 존재하지 않을 때 (즉, 특성 함수가 계산 가능 함수가 아닐 때), 그러한 문제는 결정 불가능하다고 한다.

정지 문제는 결정 불가능하다. 즉, 어떤 프로그램 P가 주어졌을 때, 특정 입력을 사용하여 실행될 때 P가 결국 정지하는지 여부를 정확하게 결정할 수 있는 컴퓨터 프로그램은 없다.

유리 마차세비치에 의해 해결된 힐베르트의 제10문제는 결정 불가능한 명제의 한 예시이다. MRDP 정리에 따르면, 괴델 문장은 정수를 변수로 대입했을 때 정수 계수를 갖는 여러 변수의 특정 다항식이 0의 값을 갖지 않는다는 명제로 다시 작성될 수 있다. 이는 마티야세비치의 정리로 이어지는데, 이 정리에 따르면 정수 계수를 갖는 다변수 다항식 p(x1, x2,...,xk)가 주어졌을 때, 방정식 p = 0에 정수 해가 있는지 여부를 결정하는 알고리즘은 없다.

8. 힐베르트 프로그램의 발전

다비트 힐베르트는 수학의 무모순성을 "유한한 입장"에서 증명하려 했다. 즉, 수학을 형식화된 공식체계로 만든 후, 그 체계의 무모순성을 '유한한 초수학적 방법'으로 증명하고자 했다.^[6] 그러나 괴델의 불완전성 정리는 이러한 힐베르트 프로그램이 실현 불가능함을 보였다.

하지만 괴델 자신은 "새로운 공리나 추론 규칙에 의한 수학의 확장이 무한정 계속되는 가운데 어떤 산술 문제도 언젠가 어디선가 결정될 가능성"을 믿었다. 괴델은 현대 수학을 확장하는 수단으로 "거대 기수 공리"를 제안했다.

불완전성 정리는 힐베르트의 목적(수학의 "무모순성 증명")을 실현하기 위해서는 수단(힐베르트 프로그램)을 확장할 필요가 있다는 것을 보여주었다. 실제로 괴델의 정리 발견 이후 겐첸의 무모순성 증명 등 무모순성 증명을 위한 다양한 방법론이 개발되었다.

9. 오해 (철학 등에 의한 오해/오용)

토르켈 프란센에 따르면, 불완전성 정리의 영향력과 중요성에 대해 과장된 주장이 반복되어 왔다.^[4] 불완전성 정리가 가장 큰 충격을 주었다고 생각되는 수학에서조차 "혁명"과 같은 일은 일어나지 않았다.^[4] 불완전성 정리는 수리논리학에서 항상 사용되지만, 일반적인 수학자들의 일에는 거의 도움이 되지 않는다.^[4]

괴델의 정리에 대한 오해는 일반 대중 사이에서도 발생하고 있다.^[4] 예를 들어, "어떤 종류의 사실은 논리나 수학으로 제대로 증명할 수 없다", "어떤 것도 확실하게 전부 알 수는 없다", "인간의 마음은 계산기(컴퓨터)가 할 수 없는 일도 할 수 있다" 등이 있다.^[4]

유명한 물리학자조차 실수를 범하는 경우가 있다.^[4] 프리먼 다이슨과 스티븐 호킹의 논설은 만물 이론의 가능성을 부정하기 위해 괴델의 정리를 사용했지만, 이는 잘못된 적용이다.^[4] 괴델의 정리는 "산술을 포함하는 체계가 그 산술 부분에서 불완전하다"는 주장이므로, 그 산술의 바깥 부분이 완전한지 불완전한지에 대해서는 이 정리가 아무것도 말하지 않는다.^[4]

참조

_[1] 문서 independent
_[2] 문서
_[3] 서적 Subsystems of Second-Order Arithmetic Perspectives in Logic
_[4] 웹사이트 数理論理学 II (不完全性定理) https://www.kurims.k[...] 2023-04-06
_[5] 저널 History of the parallel postulate https://archive.org/[...] 1920-01
_[6] 저널 Über das Unendliche https://archive.org/[...] 1926
_[7] 저널 Über formal unentscheidbare Sätze der ''Principia Mathematica'' und verwandter Systeme I 1931
_[8] 저널 Recursive predicates and quantifiers 1943
_[9] 저널 Information-theoretic limitations of formal systems https://web.archive.[...] 2014-11-20
_[10] 서적 Gödel’s theorem: an incomplete guide to its use and abuse A.K. Peters 2005