괴델의 불완전성 정리

괴델의 불완전성 정리는 형식적 공리 이론에서 증명 가능성의 한계와 관련된 수학 논리의 두 가지 정리입니다. 1931년 쿠르트 괴델(Kurt Gödel)이 발표한 이 결과는 수학 논리학과 수학 철학 모두에서 중요합니다. 그 정리들은 광범위하지만 보편적이지는 않지만, 모든 수학에 대한 완전하고 일관된 일련의 공리를 찾기 위한 힐베르트의 프로그램이 불가능하다는 것을 보여주는 것으로 해석됩니다.

첫 번째 불완전성 정리는 효과적인 절차(즉, 알고리즘)로 정리를 나열할 수 있는 일관된 공리 체계가 자연수의 산술에 대한 모든 진리를 증명할 수 없다고 말합니다. 그러한 일관된 형식 체계의 경우, 항상 참이지만 체계 내에서 증명할 수 없는 자연수에 대한 진술이 있을 것입니다.

첫 번째의 확장인 두 번째 불완전성 정리는 시스템이 자체 일관성을 입증할 수 없음을 보여줍니다.

대각 논법을 사용한 괴델의 불완전성 정리는 형식적 체계의 한계에 대해 밀접하게 관련된 여러 정리 중 첫 번째 정리였습니다. 그들은 진리의 형식적 불확정성에 대한 타르스키의 불확정성 정리, 힐베르트의 엔체이둥 문제는 풀 수 없다는 교회의 증명, 정지 문제를 해결할 알고리즘이 없다는 튜링의 정리가 뒤따랐습니다.

형식적 체계: 완전성, 일관성, 효과적 공리화

불완전성 정리는 자연수의 기본 산술을 표현하기에 충분한 복잡성을 가지고 일관되고 효과적으로 공리화된 형식적 체계에 적용됩니다. 특히 1차 논리의 맥락에서 형식 체계는 형식 이론이라고도 불립니다. 일반적으로 형식 체계는 공리로부터 새로운 정리를 유도할 수 있는 상징적 조작 규칙(또는 추론 규칙)과 함께 특정한 일련의 공리로 구성된 연역적 장치입니다. 그러한 시스템의 한 예는 모든 변수가 자연수를 나타내도록 의도된 시스템인 1차 페아노 산술입니다. 집합론과 같은 다른 체계에서는 형식 체계의 일부 문장만이 자연수에 대한 문장을 표현합니다. 불완전성 정리는 비공식적인 의미의 "증명 가능성"이 아니라 이러한 시스템 내의 공식적인 증명 가능성에 관한 것입니다.

형식적 체계가 가질 수 있는 특성은 완전성, 일관성, 효과적인 공리화의 존재 등 여러 가지가 있습니다. 불완전성 정리는 충분한 양의 산술을 포함하는 시스템이 이 세 가지 속성을 모두 가질 수 없음을 보여줍니다.

효율적 공리화

형식적 체계는 그 정리들의 집합이 재귀적으로 열거될 수 있는 경우 효과적으로 공리화(유효 생성이라고도 함)된다고 합니다. 이것은 원칙적으로 정리가 아닌 문장을 나열하지 않고 시스템의 모든 정리를 열거할 수 있는 컴퓨터 프로그램이 있다는 것을 의미합니다. 효과적으로 생성된 이론의 예로는 페아노 산술과 제르멜로-프렝켈 집합 이론(ZFC)이 있습니다.^[1]

참 산술이라고 알려진 이론은 페아노 산술의 언어로 표준 정수에 대한 모든 참 진술로 구성됩니다. 이 이론은 일관되고 완전하며 충분한 양의 산술을 포함하고 있습니다. 그러나 재귀적으로 열거 가능한 공리 집합이 없으므로 불완전성 정리의 가설을 만족시키지 못합니다.

완성도

공리의 언어로 된 어떤 진술에 대해, 그 진술 또는 그 부정이 공리로부터 증명될 수 있다면 공리의 집합은 완전합니다.^[2] 이것은 괴델의 첫 번째 불완전성 정리와 관련된 개념입니다. 의미론적 완성도와 혼동하지 말라는 것인데, 이는 일련의 공리가 주어진 언어의 모든 의미론적 신조를 증명한다는 것을 의미합니다. 괴델은 그의 완전성 정리(여기에 설명된 불완전성 정리와 혼동하지 않기 위해)에서 1차 논리가 의미론적으로 완전하다는 것을 증명했습니다. 그러나 논리의 공리만으로는 증명할 수도 반증할 수도 없는 1차 논리의 언어로 표현할 수 있는 문장이 있기 때문에 구문론적으로 완전하지 않습니다.

수학의 체계에서, 힐베르트와 같은 사상가들은 모든 수학 공식을 증명하거나 (그 부정을 증명함으로써) 반증할 수 있는 그러한 공리화를 찾는 것은 단지 시간 문제라고 믿었습니다.

형식적인 시스템은 일반적으로 논리학과 마찬가지로 설계에 의해 구문론적으로 불완전할 수 있습니다. 아니면 단순히 필요한 모든 공리가 발견되거나 포함되지 않았기 때문에 불완전할 수 있습니다. 예를 들어, 평행 공준이 없는 유클리드 기하학은 언어의 일부 문장(예: 평행 공준 자체)이 나머지 공리로부터 증명될 수 없기 때문에 불완전합니다. 마찬가지로, 조밀한 선형 순서 이론은 완전하지 않지만 순서에 끝점이 없다는 추가 공리로 완전해집니다. 연속체 가설은 ZFC 내에서 증명할 수 없는 ZFC 언어로 된 진술이므로 ZFC는 완전하지 않습니다. 이 경우 문제를 해결하는 새로운 공리에 대한 명확한 후보는 없습니다.

1차 페아노 산술 이론은 일관된 것으로 보입니다. 실제로 그렇다면 무한하지만 재귀적으로 열거할 수 있는 공리 집합을 가지며 불완전성 정리의 가설에 대한 충분한 산술을 인코딩할 수 있다는 점에 유의하십시오. 따라서 첫 번째 불완전성 정리에 의해 페아노 산술은 완전하지 않습니다. 이 정리는 페아노의 산술에서 증명할 수도 반증할 수도 없는 산술 진술의 명시적인 예를 제공합니다. 게다가, 이 진술은 일반적인 모델에서 사실입니다. 또한 페아노 산술의 효과적으로 공리화되고 일관된 확장은 완전할 수 없습니다.

일관성.

일련의 공리는 진술과 그 부정이 모두 공리로부터 증명될 수 있는 진술이 없으면 (단순히) 일관되고 그렇지 않으면 일관되지 않습니다. 즉, 일관된 공리 체계는 모순이 없는 체계입니다.

페아노 산술은 ZFC에서 일관성을 입증할 수 있지만 그 자체에서는 일관성이 없습니다. 마찬가지로 ZFC는 그 자체에서 일관성을 입증할 수는 없지만, ZFC + "접근할 수 없는 추기경이 존재한다"는 것은 κ이 그러한 최소한의 추기경이라면 폰 노이만 우주 안에 앉아 있는 V는 ZFC의 모델이며, 어떤 이론은 모델이 있어야만 일관성이 있기 때문입니다.

페아노 산술의 언어로 된 모든 진술을 공리로 삼는다면 이 이론은 완전하고 재귀적으로 열거 가능한 공리 집합을 가지며 덧셈과 곱셈을 설명할 수 있습니다. 하지만, 일관성이 없습니다.

일관되지 않은 이론의 추가적인 예는 집합 이론에서 무제한 이해의 공리 스키마를 가정할 때 발생하는 역설에서 발생합니다.

산술을 포함하는 시스템

불완전성 정리는 자연수에 대한 충분한 사실 집합을 증명할 수 있는 형식적 체계에만 적용됩니다. 로빈슨 산술 Q의 정리들은 충분한 모음 중 하나입니다. 페아노 산술과 같은 일부 시스템은 자연수에 대한 문장을 직접 표현할 수 있습니다. ZFC 집합론과 같은 다른 것들은 자연수에 대한 진술을 그들의 언어로 해석할 수 있습니다. 이러한 옵션 중 하나는 불완전성 정리에 적합합니다.

주어진 특성의 대수적으로 닫힌 장에 대한 이론은 완전하고 일관되며 무한하지만 재귀적으로 열거할 수 있는 공리 집합을 가지고 있습니다. 그러나 정수를 이 이론으로 부호화하는 것은 불가능하며, 이론은 정수의 산술을 설명할 수 없습니다. 유사한 예는 유클리드 기하학에 대한 타르스키의 공리와 본질적으로 동등한 실제 닫힌장 이론입니다. 그래서 (타르스키의 공식에서) 유클리드 기하학 자체는 완전하고 일관적이며 효과적으로 공리화된 이론의 한 예입니다.

Presburger 산술의 체계는 덧셈 연산만으로 자연수에 대한 일련의 공리로 구성됩니다(곱셈은 생략). 프레스버거 산술은 완전하고 일관적이며 재귀적으로 셀 수 있으며 자연수의 곱셈은 인코딩할 수 없지만 덧셈을 인코딩할 수 있으며 괴델의 정리에 대해 이론이 덧셈뿐만 아니라 곱셈도 인코딩해야 한다는 것을 보여줍니다.

Dan Willard(2001)는 괴델 수를 공식화하기 위해 관계로서 충분한 산술을 허용하지만 함수로서의 곱셈을 가질 만큼 충분히 강하지 않으므로 두 번째 불완전성 정리를 증명하지 못하는 약한 산술 시스템 계열을 연구했습니다. 이러한 시스템은 일관성이 있으며 자체 일관성을 입증할 수 있습니다(자체 verifying 이론 참조).

상충되는 목표

일련의 공리를 선택할 때 한 가지 목표는 잘못된 결과를 증명하지 않고 가능한 한 많은 올바른 결과를 증명하는 것입니다. 예를 들어, 우리는 자연수에 대한 모든 참된 산술 주장을 증명할 수 있는 일련의 참된 공리를 상상할 수 있습니다(Smith 2007, p. 2). 1차 논리의 표준 체계에서, 일관되지 않은 일련의 공리는 그 언어로 된 모든 진술을 증명할 것이고(이것은 때때로 폭발의 원리라고 불린다), 따라서 자동적으로 완성됩니다. 그러나 완전하고 일관된 일련의 공리는 모순되지 않는 최대의 정리를 증명합니다.^{[citation needed]}

Peano 산술, ZFC 및 ZFC + "접근할 수 없는 카디널이 있습니다"를 사용하는 이전 섹션에서 설명한 패턴은 일반적으로 깨질 수 없습니다. 여기서 ZFC + "접근할 수 없는 추기경이 존재합니다"는 그 자체로 일관성을 입증할 수 없습니다. 또한 ZFC + "접근할 수 없는 추기경이 존재한다"에서 해결할^[3] 수 없는 연속체 가설에서 알 수 있듯이 완전하지 않습니다.

첫 번째 불완전성 정리는 기본적인 산술을 표현할 수 있는 공식적인 체계에서는 완전하고 일관된 유한한 공리 목록이 결코 만들어질 수 없다는 것을 보여줍니다. 공리로 추가적이고 일관된 진술이 추가될 때마다 새로운 공리를 사용하더라도 여전히 증명할 수 없는 다른 참된 진술이 있습니다. 시스템을 완전하게 만드는 공리가 추가되면 시스템을 일관되지 않게 만드는 대가를 치르게 됩니다. 무한한 공리의 목록이 완전하고 일관적이며 효과적으로 공리화되는 것은 불가능합니다.

첫 번째 불완전성 정리

괴델의 첫 번째 불완전성 정리는 1931년 괴델의 논문 《수학 원리와 관련 체계 I의 형식적으로 결정할 수 없는 명제에 관하여》에서 처음으로 등장했습니다. 정리의 가설은 얼마 지나지 않아 J. Barkley Rosser(1936)에 의해 Rosser의 트릭을 사용하여 개선되었습니다. 결과 정리(Rosser의 개선 사항 포함)는 영어로 다음과 같이 번역될 수 있으며, 여기서 "formal system"은 시스템이 효과적으로 생성된다는 가정을 포함합니다.

첫 번째 불완전성 정리: "일정한 양의 기본 연산을 수행할 수 있는 일관된 형식 체계 F는 불완전합니다. 즉, F에서 증명할 수도 반증할 수도 없는 F의 언어에 대한 진술이 있습니다."(Raatikainen 2020)

정리에 의해 언급되는 증명 불가능한 문장 G는_F 종종 시스템 F에 대해 "괴델 문장"이라고 불립니다. 증명은 시스템 F에 대한 특정 괴델 문장을 구성하지만, 시스템 언어에는 괴델 문장의 결합과 논리적으로 유효한 문장과 같이 동일한 속성을 공유하는 문장이 무한히 많이 있습니다.

효과적으로 생성된 각 시스템에는 고유한 괴델 문장이 있습니다. F + G의_F 전체를 포함하는 더 큰 시스템 F'를 추가 공리로 정의할 수 있습니다. 괴델의 정리는 F'에도 적용되므로 F' 역시 완전할 수 없기 때문에 이는 완전한 체계로 이어지지는 않을 것입니다. 이 경우, G는_F 공리이기 때문에 실제로 F'의 정리입니다. G는_F F'에서 증명할 수 없다고만 진술하기 때문에 F' 내에서 증명 가능성에 의해 모순이 나타나지 않습니다. 그러나 불완전성 정리는 F'에 적용되기 때문에 F'에 대한 새로운 괴델 문장 G가_F' 존재할 것이며, 이는 F'도 불완전하다는 것을 보여줍니다. G는_F'F' F가 아닌 F'를 지칭한다는 점에서 G와_F 다를 것입니다.

괴델 문장의 통사적 형태

괴델 문장은 간접적으로 그 자체를 지칭하도록 설계되었습니다. 문장은 특정 단계 시퀀스를 사용하여 다른 문장을 구성할 때 그 구성된 문장을 F에서 증명할 수 없다고 말합니다. 그러나 단계의 순서는 구성된 문장이_F G 자체로 밝혀질 정도입니다. 이와 같이, 괴델 문장 G는_F F 내에서 자신의 증명 불가능성을 간접적으로 언급합니다(Smith 2007, p. 135).

첫 번째 불완전성 정리를 증명하기 위해 괴델은 시스템 내 증명 가능성의 개념이 시스템의 괴델 문장 수에 따라 작동하는 산술 함수로 순수하게 표현될 수 있음을 증명했습니다. 따라서 수에 관한 일정한 사실을 증명할 수 있는 시스템은 효과적으로 생성되는 것이라면 자신의 진술에 관한 사실을 간접적으로 증명할 수도 있습니다. 시스템 내에서 문장의 증명 가능성에 대한 질문은 숫자 자체의 산술적 속성에 대한 질문으로 표현되며, 이는 완전한 경우 시스템에 의해 결정됩니다.

따라서, 괴델 문장은 시스템 F의 문장을 간접적으로 언급하지만, 산술 문장으로 읽을 때 괴델 문장은 자연수만을 직접적으로 언급합니다. 어떤 자연수도 특정한 성질을 갖지 않으며, 여기서 그 성질은 원시 재귀적 관계에 의해 주어진다(Smith 2007, p. 141). 이처럼 괴델 문장은 간단한 구문 형식으로 산술의 언어로 작성할 수 있습니다. 특히 산술 언어의 공식으로 표현할 수 있으며, 이 공식은 다수의 선행 범용 양자화자와 양자화자가 없는 본체로 구성됩니다(이 공식은 산술 계층 구조의$$π $10$ {\$displaystyle \Pi$_{1}^{0} 수준입니다). MRDP 정리를 통해 괴델 문장은 정수 계수가 있는 많은 변수에서 정수가 변수를 대체할 때 특정 다항식이 값 0을 취하지 않는다는 진술로 다시 작성될 수 있습니다(Franzén 2005, p. 71).

괴델 문장의 진실

첫 번째 불완전성 정리는 적절한 형식 이론 F의 괴델 문장 G가_F F에서 증명될 수 없음을 보여줍니다. 왜냐하면 이 증명 불가능성은 산술에 관한 진술로 해석될 때 괴델 문장이 사실은 사실이라고 주장하는 문장이 정확히 일치하기 때문입니다(Smory ń스키 1977, p. 825; Franzén 2005, pp. 28-33 참조). 이러한 이유로, G라는_F 문장은 종종 "참이지만 증명할 수 없다"고 말합니다(Raatikainen 2020). 그러나 괴델 문장 자체가 공식적으로 의도된 해석을 명시할 수 없기 때문에, G_F 문장의 진실은 시스템 외부에서 메타 분석을 통해서만 도달할 수 있습니다. 일반적으로 이 메타 분석은 원시 재귀 산술로 알려진 약한 형식 체계 내에서 수행될 수 있으며, 이는 Con(F)→G라는 함의를 증명하며, 여기서 Con(F)은 F의 일관성을 주장하는 표준 문장입니다(Smory ński 1977, p. 840, Kikuchi & Tanaka 1994, p. 403).

일관된 이론의 괴델 문장은 산술의 의도된 해석에 대한 진술로서 사실이지만, 괴델의 완전성 정리의 결과로서 일부 비표준 산술 모델에서 괴델 문장은 거짓일 것입니다(Franzén 2005, p. 135). 그 정리는 문장이 이론과 독립적일 때 이론은 문장이 참인 모델과 문장이 거짓인 모델을 갖게 된다는 것을 보여줍니다. 앞에서 설명했듯이, 계 F의 괴델 문장은 특정 성질을 가진 수가 존재하지 않는다고 주장하는 산술적인 문장입니다. 불완전성 정리는 이 주장이 시스템 F와 독립적일 것이라는 것을 보여주며, 괴델 문장의 진리는 어떤 표준 자연수도 문제의 속성을 갖지 않는다는 사실에서 비롯됩니다. 괴델 문장이 거짓인 모형은 해당 모형 내의 속성을 만족시키는 요소를 포함해야 합니다. 이러한 모델은 "비표준"이어야 하며, 표준 자연수에 해당하지 않는 요소를 포함해야 합니다(Raatikainen 2020, Franzén 2005, p. 135).

거짓말쟁이 역설과의 관계

괴델은 《수학 원리와 관련 체계 I의 형식적으로 결정할 수 없는 명제에 관하여》의 서론 부분에서 리처드의 역설과 거짓말쟁이의 역설을 그의 구문론적 불완전성 결과에 대한 의미론적 유사점으로 구체적으로 인용합니다. 거짓말쟁이 역설은 "이 문장은 거짓이다"라는 문장입니다. 거짓말쟁이 문장을 분석한 결과, 거짓말은 참일 수 없으며(주장하는 대로 거짓일 수 있으며) 거짓일 수도 없습니다(그러면 참일 수 있습니다). 시스템 F에 대한 괴델 문장 G는 거짓말쟁이 문장과 유사한 주장을 하지만, 진리가 증명 가능성으로 대체됩니다. G는 "G는 시스템 F에서 증명 가능하지 않다"고 말합니다. G의 진실성과 증명 가능성에 대한 분석은 거짓말쟁이 문장의 진실성에 대한 분석을 공식화한 것입니다.

"Q는 거짓 공식의 괴델 수"라는 술어를 산술 공식으로 표현할 수 없기 때문에 괴델 문장에서 "증명할 수 없음"을 "거짓"으로 대체할 수 없습니다. 타르스키의 불확정성 정리로 알려진 이 결과는 괴델이 불완전성 정리의 증명을 연구할 때와 이 정리의 이름을 딴 알프레드 타르스키에 의해 독립적으로 발견되었습니다.

괴델의 원래 결과의 확장

1931년 괴델의 논문에서 언급된 정리와 비교할 때, 불완전성 정리에 대한 많은 현대적 진술은 두 가지 측면에서 더 일반적입니다. 이러한 일반화된 진술은 더 광범위한 시스템에 적용하기 위해 사용되며, 더 약한 일관성 가정을 통합하기 위해 사용됩니다.

괴델은 산술의 특정한 체계인 수학 원리의 체계의 불완전성을 증명했지만, 특정한 표현력의 효과적인 체계에 대해서는 병렬적인 증명을 할 수 있었습니다. 괴델은 논문 서론에서 이 사실에 대해 언급했지만, 구체적인 증명을 위해 하나의 체계로 제한했습니다. 정리의 현대적 진술에서는 불완전성 정리에 대한 가설로 유효성과 표현성 조건을 진술하는 것이 일반적이어서 특정한 형식 체계에 국한되지 않습니다. 이러한 조건을 설명하는 데 사용되는 용어는 괴델이 그의 결과를 발표한 1931년에 아직 개발되지 않았습니다.

괴델의 원래 진술과 불완전성 정리에 대한 증명은 시스템이 단순히 일관성이 있을 뿐만 아니라 ω 일관성이 있다는 가정을 필요로 합니다. 어떤 계는 ω-불일치가 아니면 ω-불일치이고, 모든 특정한 자연수 m에 대하여 계가 ~P(m)을 증명하는 술어 P가 있으면 ω-불일치이지만, 또한 계는 P(n)을 나타내는 자연수 n이 존재한다는 것을 증명합니다. 즉, 시스템은 속성 P를 가진 숫자가 존재한다는 것을 말하는 동시에 그것이 어떤 특정한 값을 가지고 있다는 것을 부정합니다. 시스템의 ω 일관성은 시스템의 일관성을 의미하지만 일관성은 ω 일관성을 의미하지 않습니다. J. 바클리 로서(J. Barkley Rosser, 1936)는 ω 일관성이 아닌 시스템이 일관성을 유지하기만 하면 되는 증명의 변형(Rosser의 트릭)을 찾아 불완전성 정리를 강화했습니다. 이것은 대부분 기술적으로 흥미로운 것인데, 왜냐하면 모든 참된 형식적인 산술 이론(공리가 자연수에 대한 참된 진술인 이론)은 ω으로 일관되기 때문이며, 따라서 원래 언급된 괴델의 정리가 그들에게 적용되기 때문입니다. ω 일관성이 아닌 일관성만을 가정한 더 강력한 버전의 불완전성 정리는 현재 일반적으로 괴델의 불완전성 정리와 괴델-로저 정리로 알려져 있습니다.

두 번째 불완전성 정리

기본 산술을 포함하는 각 형식 체계 F에 대해 F의 일관성을 나타내는 공식 Cons(F)를 정준적으로 정의할 수 있습니다. 이 공식은 "결론이 구문 모순인 시스템 F 내에 형식적 파생을 코딩하는 자연수가 존재하지 않는다"는 속성을 표현합니다. 구문 모순은 종종 "0=1"로 간주되며, 이 경우 Cons(F)는 "F의 공리로부터 '0=1'의 유도를 코딩하는 자연수는 없다"고 말합니다.

괴델의 두 번째 불완전성 정리는 일반적인 가정 하에서 이 표준 일관성 진술 Cons(F)를 F에서 증명할 수 없음을 보여줍니다. 이 정리는 괴델의 1931년 논문 "수학 원리와 관련 체계 I의 형식적으로 결정할 수 없는 명제에 관하여"에서 처음으로 "정리 XI"로 나타났습니다. 다음 문장에서 "공식화된 시스템"이라는 용어는 F가 효과적으로 공리화된다는 가정도 포함합니다. 이 정리는 어느 정도의 기본 연산을 수행할 수 있는 일관된 시스템 F에 대해서는 F 자체에서 F의 일관성을 증명할 수 없다는 것을 의미합니다.^[4] 이 정리는 첫 번째 불완전성 정리에서 구성된 문장이 시스템의 일관성을 직접적으로 표현하지 않기 때문에 첫 번째 불완전성 정리보다 더 강합니다. 두 번째 불완전성 정리의 증명은 시스템 F 자체 내에서 첫 번째 불완전성 정리의 증명을 공식화함으로써 얻어집니다.

일관성 표현

F의 언어로 F의 일관성을 수식으로 표현하는 방법에 관한 두 번째 불완전성 정리에는 기술적인 미묘함이 있습니다. 시스템의 일관성을 표현하는 방법은 여러 가지가 있으며, 모두 동일한 결과로 이어지는 것은 아닙니다. 두 번째 불완전성 정리에서 나온 공식 Cons(F)는 일관성의 특별한 표현입니다.

F가 일관성이 있다는 주장의 다른 공식화는 F에서 동등하지 않을 수 있으며 일부는 증명할 수도 있습니다. 예를 들어, 1차 페아노 산술(PA)은 "PA의 가장 큰 일관된 부분 집합"이 일관됨을 증명할 수 있습니다. 그러나 PA는 일관성이 있기 때문에 PA의 가장 큰 일관성 있는 부분 집합은 단지 PA이므로 이러한 의미에서 PA는 "일관성이 있음을 증명"합니다. PA가 증명하지 못하는 것은 PA의 가장 큰 일관된 부분 집합이 사실상 PA의 전체라는 것입니다. (여기서 "PA의 가장 큰 일관된 부분 집합"이라는 용어는 특정한 효과적인 열거 하에서 PA의 공리의 가장 큰 일관된 초기 부분이라는 의미입니다.)

힐베르트-베르네 조건

두 번째 불완전성 정리의 표준 증명은 증명 가능성 술어 Prov_A(P)가 Hilbert-Bernays 증명 조건을 만족한다고 가정합니다. #(P)가 공식 P의 괴델 수를 나타낸다고 하면, 증명 조건은 다음과 같습니다.

1. F가 P를 증명하면 F는 Prov_A(#(P))를 증명합니다.
2. F는 1. 즉, F는 Prov(#(P)) → Prov(#(P))를 증명합니다.
3. F는 Prov(#(P → Q)) ∧ Prov(#(P)) → Prov(#(Q))(모더스포넨스의 analogue)를 증명합니다.

로빈슨 산술과 같이 첫 번째 불완전성 정리의 가정을 충족할 만큼 충분히 강하지만 힐베르트-버네이스 조건을 증명하지 못하는 체계가 있습니다. 그러나 페아노 산술은 모든 이론이 페아노 산술보다 더 강한 것과 마찬가지로 이러한 조건을 검증할 수 있을 만큼 충분히 강합니다.

일관성 증명에 대한 시사점

괴델의 두 번째 불완전성 정리는 또한 위에서 설명한 기술 조건을 만족하는 시스템 F가₁ F의₁ 일관성을 증명하는 어떤 시스템 F의₂ 일관성도 증명할 수 없다는 것을 의미합니다. 이러한 시스템 F는₁ F가₂ F의₁ 일관성을 증명하면 F가₁ 실제로 일관성이 있다는 것을 증명할 수 있기 때문입니다. F가₁ "모든 수 n에 대하여, n은 F의₁ 모순 증명을 위한 코드가 아니라는 결정 가능한 속성을 갖는다"는 주장에 대하여. 만약₁ F가 실제로 일관성이 없다면, F는₂ 어떤 n에 대하여 n이 F의₁ 모순 부호임을 증명할 것입니다. 그러나 F가₁ 일관성이 있다는 것(즉, 그러한 n이 없다는 것)을 F가₂ 증명했다면, 그것 자체는 일관성이 없을 것입니다. 이₂ 추론은 F가 일관성이 있으면 F가₁ 일관성이 있음을 보여주기 위해 F로₁ 공식화할 수 있습니다. 두 번째 불완전성 정리에 의해 F는₁ 일관성을 증명하지 않기 때문에 F의₂ 일관성도 증명할 수 없습니다.

두 번째 불완전성 정리의 이러한 결과는 예를 들어 페아노 산술(PA)에서 증명할 수 있는 시스템에서 형식화할 수 있는 유한한 수단을 사용하여 페아노 산술의 일관성을 증명할 희망이 없음을 보여줍니다. 예를 들어, 유한 수학의 정확한 형식화로 널리 받아들여지고 있는 원시 재귀 산술(PRA)의 시스템은 PA에서 입증 가능하게 일치합니다. 따라서 PRA는 PA의 일관성을 증명할 수 없습니다. 이 사실은 일반적으로 이상적인 원리가 일치한다는 유한한 증거를 제공함으로써 "진짜"(무한한) 수학 진술의 증명에서 "이상적인"(무한한) 수학적 원리의 사용을 정당화하려는 힐베르트의 프로그램이 수행될 수 없음을 암시하는 것으로 보입니다.^[5]

결론은 또한 두 번째 불완전성 정리의 인식론적 관련성을 나타냅니다. 시스템 F가 일관성을 입증한다면 흥미로운 정보를 제공하지 못할 것입니다. 일관성 없는 이론이 일관성을 포함한 모든 것을 증명하기 때문입니다. 따라서 F에서 F의 일관성 증명은 F가 일관성이 있는지 여부에 대한 단서를 제공하지 않을 것입니다. F의 일관성에 대한 의심은 이러한 일관성 증명으로 해결될 것입니다. 일관성 증명에 대한 관심은 어떤 의미에서는 F 자체보다 덜 의심스러운, 예를 들어 F보다 약한, 어떤 시스템 F'에서 시스템 F의 일관성을 증명할 가능성에 있습니다. F = 제르멜로-프렝켈 집합론, F' = 원시 재귀 산술과 같은 많은 자연 발생 이론 F와 F'에 대해 F'의 일관성은 F에서 증명할 수 있으며, 따라서 F'는 두 번째 불완전성 정리의 위의 결과로 F의 일관성을 증명할 수 없습니다.

두 번째 불완전성 정리는 일부 이론 T의 일관성을 증명할 가능성을 완전히 배제하지는 않으며, T 자체가 일관성이 있음을 증명할 수 있는 이론에서만 그렇게 합니다. 예를 들어, 게르하르트 겐첸은 ε이라고 불리는 순서형이 충분히 근거가 있다는 공리를 포함하는 다른 체계에서 페아노 산술의 일관성을 증명했습니다. 겐첸의 일관성 증명을 참조하십시오. 젠젠의 정리는 증명 이론에서 순서형 분석의 발전에 박차를 가했습니다.

결정되지 않은 진술의 예시

"결정할 수 없는"이라는 단어는 수학과 컴퓨터 과학에 두 가지 다른 의미가 있습니다. 이 중 첫 번째는 괴델의 정리와 관련하여 사용되는 증명 이론적 의미로, 특정 연역 체계에서 증명할 수도 반박할 수도 없는 진술입니다. 여기서는 다루지 않을 두 번째 의미는 계산 가능성 이론과 관련하여 사용되며, 각각 예 또는 아니오 답변을 요구하는 셀 수 없을 정도로 무한한 질문 집합인 결정 문제에 적용됩니다. 이러한 문제는 문제 집합의 모든 문제에 정확하게 답하는 계산 가능한 함수가 없으면 결정할 수 없다고 합니다(결정할 수 없는 문제 참조).

결정할 수 없는 단어의 두 가지 의미 때문에 "증명할 수도 반박할 수도 없는" 의미로 결정할 수 없는 대신 독립이라는 용어가 사용되기도 합니다.

특정 연역 체계에서 진술의 미결정성은 그 자체로 진술의 진실 값이 잘 정의되어 있는지 또는 다른 방법으로 결정될 수 있는지에 대한 문제를 해결하지 못합니다. 미결정성은 고려 중인 특정 연역체계가 진술의 진·위조를 입증하지 못한다는 것을 의미할 뿐입니다. 진리값을 결코 알 수 없거나 특정할 수 없는 이른바 '절대적으로 결정되지 않은' 진술이 존재하는지 여부는 수학철학에서 논란의 여지가 있는 대목입니다.

괴델(Gödel)과 폴 코헨(Paul Cohen)의 결합된 연구는 결정할 수 없는 진술의 두 가지 구체적인 예를 제시했습니다(이 용어의 첫 번째 의미에서). 연속체 가설은 ZFC(집합 이론의 표준 공리화)에서 증명되거나 반박될 수 없으며, ZF(선택 공리를 제외한 모든 ZFC 공리)에서는 선택 공리를 증명하거나 반박할 수 없습니다. 이러한 결과는 불완전성 정리를 필요로 하지 않습니다. 괴델은 1940년 ZF나 ZFC 집합론에서 이 두 문장 모두 반증될 수 없다는 것을 증명했습니다. 1960년대에 Cohen은 ZF에서 둘 다 증명할 수 없으며 연속체 가설은 ZFC에서 증명할 수 없음을 증명했습니다.

Shelah(1974)는 그룹 이론의 Whitehead 문제가 표준 집합 이론에서 용어의 첫 번째 의미에서 결정할 수 없음을 보여주었습니다.^[6]

그레고리 차이틴(Gregory Chaitin)은 알고리즘 정보 이론에서 결정할 수 없는 진술을 생성했으며 그 설정에서 또 다른 불완전성 정리를 증명했습니다. 차이틴의 불완전성 정리는 충분한 산술을 나타낼 수 있는 모든 시스템에 대해 그 시스템에서 특정한 수가 c보다 큰 콜모고로프 복잡도를 갖는다는 것을 증명할 수 없는 상한 c가 존재한다고 말합니다. 괴델의 정리는 거짓말쟁이 역설과 관련이 있지만, 차이틴의 결과는 베리의 역설과 관련이 있습니다.

더 큰 시스템에서 입증할 수 있는 결정할 수 없는 진술

이것들은 괴델의 "참이지만 결정할 수 없는" 문장의 자연스러운 수학적 동치입니다. 그것들은 일반적으로 유효한 형태의 추론으로 받아들여지는 더 큰 시스템에서 증명될 수 있지만 페아노 산술과 같은 더 제한된 시스템에서는 결정할 수 없습니다.

1977년, 파리와 해링턴은 무한 램지 정리의 한 버전인 파리-해링턴 원리가 (1차) 피노 산술에서는 결정할 수 없지만 더 강한 2차 산술 체계에서는 증명할 수 있음을 증명했습니다. 커비와 파리는 나중에 파리-해링턴 원리보다 다소 간단한 자연수의 수열에 관한 진술인 굿스타인의 정리가 페아노 산술에서도 결정할 수 없다는 것을 보여주었습니다.

컴퓨터 과학에 응용된 크러스칼의 트리 정리는 피아노 산술에서도 결정할 수 없지만 집합 이론에서는 증명할 수 있습니다. 사실 크루스칼의 나무 정리(또는 그 유한한 형태)는 예측주의라고 불리는 수학 철학에 기초하여 허용 가능한 원칙을 성문화하는 훨씬 더 강력한 시스템 ATR에서₀ 결정할 수 없습니다.^[7] 관련이 있지만 보다 일반적인 그래프 마이너 정리(2003)는 계산 복잡성 이론에 영향을 미칩니다.

계산가능성과의 관계

불완전성 정리는 재귀 이론에서 결정할 수 없는 집합에 대한 여러 결과와 밀접한 관련이 있습니다.

Kleene(1943)은 계산 가능성 이론의 기본 결과를 사용하여 괴델의 불완전성 정리에 대한 증명을 제시했습니다. 그러한 결과 중 하나는 정지 문제가 결정되지 않는다는 것을 보여줍니다. 어떤 컴퓨터 프로그램도 입력으로 P가 주어지면 특정 입력으로 실행될 때 결국 P가 중단되는지 여부를 올바르게 결정할 수 없습니다. Kleene은 일정한 일관성을 가진 완전한 효과적인 산술 시스템의 존재가 중단 문제를 결정할 수밖에 없다는 것을 보여주었는데, 이는 모순입니다.^[8] 이 증명 방법은 Shoenfield(1967), Charlesworth(1981), Hopcroft & Ullman(1979)에 의해 제시되었습니다.^[9]

프란젠(2005)은 힐베르트의 10번째 문제에 대한 마티야세비치의 해가 괴델의 첫 번째 불완전성 정리에 대한 증명을 얻는 데 어떻게 사용될 수 있는지 설명합니다.^[10] 마티야세비치는 정수 계수를 갖는 다변량 다항식 p(x, x,...,x)가 주어졌을 때, 방정식 p = 0에 정수해가 존재하는지 여부를 결정하는 알고리즘이 없다는 것을 증명했습니다. 정수 계수를 갖는 다항식, 그리고 정수 자체는 산술 언어로 직접 표현할 수 있기 때문에, 만약 다변량 정수 다항식 p = 0에 정수에 해가 있다면 충분히 강한 산술 T의 계가 이를 증명할 것입니다. 또한 시스템 T가 ω 일관성이 있다고 가정합니다. 그 경우, 정수에 해가 없을 때 특정 다항식이 해를 갖는다는 것은 결코 증명되지 않습니다. 따라서 T가 완전하고 ω으로 일관된 경우, 마티야세비치의 정리와 반대로 "p는 해를 갖는다" 또는 "p는 해가 없다"가 발견될 때까지 T의 증명을 열거하는 것만으로 다항식이 해를 갖는지 여부를 알고리즘적으로 결정할 수 있습니다. 따라서 T는 ω으로 일관되고 완전할 수 없습니다. 또한 효과적으로 생성된 각 일관된 시스템 T에 대해 정수에 대한 다변량 다항식 p를 효과적으로 생성할 수 있으므로 방정식 p = 0에는 정수에 대한 해가 없지만 해가 없다는 것은 T에서 증명할 수 없습니다.

Smory ń스키(1977)는 재귀적으로 분리할 수 없는 집합의 존재가 첫 번째 불완전성 정리를 증명하는 데 어떻게 사용될 수 있는지 보여줍니다. 이 증명은 종종 페아노 산술과 같은 시스템이 본질적으로 결정할 수 없음을 보여주기 위해 확장됩니다.^[12]

Chaitin의 불완전성 정리는 Kolmogorov 복잡도에 기초하여 독립적인 문장을 생성하는 다른 방법을 제공합니다. 위에서 언급한 Kleene이 제시한 증명과 마찬가지로 Chaitin의 정리는 자연수의 표준모형에서 그들의 모든 공리가 참이라는 추가적인 속성을 가진 이론에만 적용됩니다. 괴델의 불완전성 정리는 표준 모델에 거짓 진술을 포함하는 일관된 이론에 적용할 수 있다는 점에서 구별됩니다. 이러한 이론은 ω 불일치로 알려져 있습니다.

첫 번째 정리에 대한 증명 스케치

모순에 의한 증명에는 세 가지 필수 부분이 있습니다. 먼저 제안된 기준을 충족하는 공식 시스템을 선택합니다.

1. 체계의 문장은 자연수(괴델 수)로 나타낼 수 있습니다. 이것의 중요성은 진리와 거짓과 같은 진술의 속성이 괴델 수가 특정한 속성을 갖는지 여부를 결정하는 것과 같으며, 따라서 진술의 속성은 괴델 수를 조사함으로써 입증될 수 있다는 것입니다. 이 부분은 "S문은 시스템에서 증명 가능하다"(시스템의 모든 "S"문에 적용할 수 있음)는 생각을 표현하는 공식의 구성으로 끝납니다.
2. 형식적인 시스템에서는 일치하는 문장이 해석될 때 자기 참조적이고 본질적으로 (즉, 문장 자체) 증명할 수 없다고 말하는 숫자를 구성할 수 있습니다. 이것은 "대각화"(Cantor의 대각선 논법으로서 그 기원 때문에 소위 "대각화"(diagonalization)라고 불리는 기술을 사용하여 수행됩니다.
3. 공식적인 시스템 내에서 이 진술은 시스템에서 증명할 수도 반증할 수도 없고, 따라서 시스템이 실제로 ω 일관성을 가질 수도 없다는 것을 증명할 수 있게 합니다. 따라서 제안된 시스템이 기준을 충족했다는 원래의 가정은 거짓입니다.

구문의 산술화

위에서 설명한 증명을 구체화하는 데 있어 가장 큰 문제는 처음에는 "p를 증명할 수 없다"에 해당하는 문장 p를 구성하려면 p가 어떻게든 p에 대한 참조를 포함해야 하고, 이는 쉽게 무한 회귀를 일으킬 수 있다는 것입니다. 괴델의 기술은 "문을 증명하는 것"이 "숫자가 주어진 속성을 갖는지 여부를 테스트하는 것"으로 대체될 수 있는 방식으로 문장이 숫자와 일치할 수 있음을 보여주는 것입니다(종종 구문의 산술화라고 함). 이를 통해 정의의 무한 회귀를 방지하는 방식으로 자기 참조 공식을 구성할 수 있습니다. 같은 기술은 나중에 앨런 튜링에 의해 엔체이둥 문제에 대한 연구에 사용되었습니다.

간단히 말해서, 공식과 괴델 수 사이를 기계적으로 앞뒤로 변환할 수 있는 방식으로 시스템에서 공식화할 수 있는 모든 공식이나 문장이 괴델 수라고 하는 고유한 수를 얻게 하는 방법을 고안할 수 있습니다. 관련된 숫자는 실제로 (숫자로 볼 때) 매우 길 수 있지만, 이것은 장벽이 아닙니다. 중요한 것은 이러한 숫자를 구성할 수 있다는 것입니다. 간단한 예는 영어가 각 문자에 대해 숫자의 시퀀스로 저장된 다음 하나의 큰 숫자로 결합되는 방법입니다.

• 이 단어는 ASCII에서 104-101-108-108-111로 인코딩되어 번호 104101108108108111로 변환될 수 있습니다.
• 논리 문은 ASCII로 120-061-121-032-061-062-032-121-061-120으로 인코딩되며 숫자 1200611210320610620으로 변환될 수 있습니다.

원칙적으로 진술의 참 또는 거짓을 증명하는 것은 진술과 일치하는 숫자가 주어진 속성을 갖거나 가지지 않음을 증명하는 것과 동등하다고 볼 수 있습니다. 공식 시스템은 일반적으로 숫자에 대한 추론을 지원할 수 있을 만큼 충분히 강력하기 때문에 공식과 문장을 나타내는 숫자에 대한 추론도 지원할 수 있습니다. 결정적으로, 시스템은 숫자의 속성에 대한 추론을 지원할 수 있기 때문에, 결과는 그들의 동등한 문장의 증명 가능성에 대한 추론과 동등합니다.

"증명 가능성"에 대한 문 구성

원칙적으로 시스템이 증명 가능성에 대한 진술을 간접적으로 할 수 있음을 보여준 후, 진술을 표현하는 숫자의 속성을 분석함으로써 실제로 이를 수행하는 진술을 작성하는 방법을 보여줄 수 있습니다.

정확히 하나의 자유 변수 x를 포함하는 공식 F(x)를 문 형태 또는 클래스 부호라고 합니다. x가 특정 숫자로 대체되는 즉시 문장 형태는 충실한 문장으로 바뀌며, 시스템에서 증명 가능하거나 그렇지 않습니다. 특정 공식에 대해 모든 자연수 n에 대해 $F{\displaystyle (n)}$ ${\displaystyle F(n)}$가 참임을 증명할 수 있는 경우에만 증명할 수 있습니다(원래 증명의 정확한 요구 사항은 약하지만 증명 스케치의 경우에는 이 정도면 충분합니다). 특히 "2 × 3 = 6"과 같이 유한한 수의 자연수 사이의 모든 특정 산술 연산에 대해서도 마찬가지입니다.

명세서 양식 자체는 명세서가 아니므로 증명하거나 반증할 수 없습니다. 그러나 모든 문장 형식 F(x)에는 G(F)로 표시되는 괴델 수가 할당될 수 있습니다. F(x) 형태로 사용되는 자유 변수의 선택은 괴델 수 G(F)의 할당과 관련이 없습니다.

증명 가능성의 개념 자체는 다음과 같은 방식으로 괴델 수에 의해 암호화될 수도 있습니다. 증명은 특정 규칙을 따르는 진술의 목록이기 때문에 증명의 괴델 수는 정의될 수 있습니다. 이제 모든 문장 p에 대해 x가 그 증명의 괴델 수이냐는 질문을 할 수 있습니다. 증명의 잠재적 괴델 수인 p와 x의 괴델 수 사이의 관계는 두 수 사이의 산술적 관계입니다. 따라서 이 산술 관계를 사용하여 y의 증명의 괴델 수가 존재한다는 것을 나타내는 문장 형태인 Bew(y)가 있습니다.

Bew(y) = ∃ x(y는 공식의 괴델 수, x는 y에 의해 부호화된 공식의 증명의 괴델 수).

Bew라는 이름은 독일어로 "provable"을 의미하는 beweisbar의 줄임말입니다. 이 이름은 원래 괴델이 방금 설명한 provability 공식을 나타내기 위해 사용되었습니다. "Bew(y)"는 T의 원래 언어로 된 특정한, 매우 긴 공식을 나타내는 약어일 뿐이며, 문자열 "Bew" 자체가 이 언어의 일부라고 주장되지는 않습니다.

공식 Bew(y)의 중요한 특징은 문장 p가 시스템에서 증명 가능하다면 Bew(G(p))도 증명 가능하다는 것입니다. 왜냐하면 p의 어떤 증명도 상응하는 괴델 수를 가질 것이고, 그 수가 존재하면 Bew(G(p))가 만족하게 되기 때문입니다.

대각화

증명의 다음 단계는 간접적으로 자신의 증명 불가능성을 주장하는 진술을 얻는 것입니다. 비록 괴델이 이 문장을 직접 만들었지만, 적어도 하나의 그러한 문장의 존재는 대각선 보조정리로부터 오는 것이며, 이는 어떤 충분히 강한 형식 체계와 어떤 문장 형태 F에 대해서도 그 체계가 증명하는 문장 p가 존재한다는 것을 의미합니다.

p ↔ F(G(p)).

F를 Bew(x)의 음수로 함으로써 정리를 구합니다.

p ↔ ~Bew(G(p))

그리고 이에 의해 정의되는 p는 대략적으로 자신의 괴델 수가 증명 불가능한 공식의 괴델 수라고 말합니다.

문장 p는 문자 그대로 ~Bew(G(p))와 같지 않으며, 오히려 p는 특정 계산이 수행되면 결과적인 괴델 수가 증명 불가능한 문장의 것이 된다고 말합니다. 그러나 이 계산을 수행하면 결과적인 괴델 수는 p 자체의 괴델 수로 밝혀집니다. 이것은 영어의 다음 문장과 비슷합니다.

", 따옴표에서 그 앞에 오는 경우에는 증명할 수 없습니다."라고 따옴표에서 그 앞에 오는 경우에는 증명할 수 없습니다.

이 문장은 직접적으로 자신을 지칭하는 것이 아니라, 진술된 변형이 이루어질 때 결과적으로 원래의 문장을 얻게 되고, 따라서 이 문장은 간접적으로 자신의 증명 불가능성을 주장합니다. 대각선 보조정리의 증명도 이와 유사한 방법을 사용합니다.

이제 공리계가 ω으로 일치한다고 가정하고, p를 앞 절에서 구한 문장이라고 가정합니다.

p가 증명 가능하다면 위에서 주장한 바와 같이 Bew(G(p))가 증명 가능할 것입니다. 그러나 p는 Bew(G(p))의 부정을 주장합니다. 따라서 시스템은 일관성이 없어 진술과 부정을 모두 증명합니다. 이 모순은 p가 증명될 수 없음을 보여줍니다.

p의 부정이 증명 가능하다면 Bew(G(p))는 증명 가능할 것입니다(p는 Bew(G(p))의 부정과 동등하게 구성되었기 때문입니다). 그러나 각각의 특정한 수 x에 대하여, p는 증명할 수 없기 때문에 x는 p의 증명의 괴델 수가 될 수 없습니다. 따라서 이 계는 한편으로 어떤 성질을 가진 수가 존재한다는 것을 증명하지만, 다른 한편으로 모든 특정 수 x에 대하여 우리는 이 성질을 갖지 않는다는 것을 증명할 수 있습니다. 이는 ω 일관성 시스템에서는 불가능합니다. 따라서 p의 부정은 증명할 수 없습니다.

따라서 명제 p는 우리의 공리 체계에서 결정할 수 없습니다. 그것은 체계 내에서 증명될 수도 반증될 수도 없습니다.

실제로 p가 증명 가능하지 않다는 것을 보여주기 위해서는 시스템이 일관적이라는 가정만 필요합니다. p의 부정이 증명되지 않는다는 것을 보여주기 위해서는 ω 일관성에 대한 더 강한 가정이 필요합니다. 따라서 p가 특정 시스템에 대해 구성된 경우:

• 시스템이 ω으로 일관되면 p도 부정도 증명할 수 없으며 sop는 결정할 수 없습니다.
• 시스템이 일관되면 동일한 상황이 발생할 수도 있고 p의 부정을 증명할 수도 있습니다. 후자의 경우 거짓이지만 증명 가능한 문장("p가 아님")이 있으며, 시스템은 ω 일관성이 없습니다.

시스템의 불완전성을 피하기 위해 누락된 공리를 추가하려고 하면 공리로 p 또는 "not p"를 추가해야 합니다. 그러나 그 다음 문장의 "증명의 괴델 수"라는 정의가 바뀝니다. 이는 Bew(x) 공식이 이제 다르다는 것을 의미합니다. 따라서 이 새로운 Bew에 대각선 보조정리를 적용하면 이전과는 다른 새로운 문장 p를 얻는데, 이 문장은 ω으로 일관된 경우 새로운 시스템에서 결정되지 않습니다.

베리의 역설을 통한 증명

불로스(1989)는 거짓말쟁이 역설이 아닌 베리의 역설을 사용하여 참이지만 증명할 수 없는 공식을 구성하는 첫 번째 불완전성 정리의 대안적 증명을 스케치합니다. 사울 크립케는 이와 유사한 증명법을 독자적으로 발견했습니다.^[13] 불로스의 증명은 계산 가능하게 셀 수 있는 산술의 참 문장 집합 S에 대해 참이지만 S에 포함되지 않은 다른 문장을 구성하는 것으로 진행됩니다. 이것은 첫 번째 불완전성 정리를 결과로 제공합니다. 불로스에 따르면, 이 증명은 효과적이고 일관된 산술 이론의 불완전성에 대한 "다른 종류의 이성"을 제공하기 때문에 흥미롭습니다.^[14]

컴퓨터가 검증한 증명

불완전성 정리는 증명 보조 소프트웨어로 완전히 검증할 수 있는 공식화된 정리로 변환된 비교적 적은 수의 자명하지 않은 정리 중 하나입니다. 대부분의 수학적 증명들과 마찬가지로 불완전성 정리에 대한 괴델의 원래 증명들은 인간 독자들을 위한 자연어로 쓰여졌습니다.

첫 번째 불완전성 정리의 버전에 대한 컴퓨터로 검증된 증명은 1986년 Nqthm(Shankar 1994)을 사용하여 나타라잔 샹카르(Natarajan Shankar)에 의해, 2003년 Coq(O'Connor 2005)를 사용하여 러셀 오코너(Russell O'Connor)에 의해, 2009년 HOL Light(Harrison 2009)를 사용하여 존 해리슨(John Harrison)에 의해 발표되었습니다. 2013년 로렌스 폴슨이 이사벨(Paulson 2014)을 사용하여 두 이론의 불완전성에 대한 컴퓨터로 검증된 증거를 발표했습니다.

두 번째 정리에 대한 증명 스케치

두 번째 불완전성 정리를 증명하는 주요 어려움은 첫 번째 불완전성 정리의 증명에 사용된 증명 가능성에 대한 다양한 사실이 증명 가능성에 대한 공식 술어 P를 사용하여 시스템 S 내에서 공식화될 수 있음을 보여주는 것입니다. 이 작업이 완료되면 시스템 S 자체 내에서 첫 번째 불완전성 정리의 전체 증명을 공식화함으로써 두 번째 불완전성 정리가 뒤따릅니다.

p는 위에서 구성된 결정되지 않은 문장을 의미하고, 시스템 S 자체에서 시스템 S의 일관성이 증명될 수 있다는 모순을 얻기 위한 목적으로 가정합니다. 이는 "System S is consident"라는 문장을 증명하는 것과 같습니다. 이제 c를 생각해 보자. 여기서 c = "시스템 S가 일관되면 p는 증명할 수 없습니다." 문장 c의 증명은 시스템 S 내에서 공식화될 수 있으며, 따라서 "p는 증명할 수 없다"(또는 동일하게 "p(p))"는 문장 c를 시스템 S에서 증명할 수 있습니다.

그렇다면 시스템 S가 일관성이 있다는 것을 증명할 수 있는지 관찰하십시오. c)의 가설에서의 진술, 그러면 우리는 p가 증명할 수 없다는 것을 증명했습니다. 그러나 이것은 제1 불완전성 정리에 의해 이 문장(즉, 문장 c에 암시된 것, "p"는 증명할 수 없음)이 증명할 수 없도록 구성된 것이기 때문에 모순입니다. 이것이 S에서 첫 번째 불완전성 정리를 공식화해야 하는 이유입니다. 두 번째 불완전성 정리를 증명하기 위해, 우리는 그 정리가 S에서 성립한다는 것을 보여줌으로써만 할 수 있는 첫 번째 불완전성 정리와 모순을 얻습니다. 그래서 우리는 시스템 S가 일관성이 있다는 것을 증명할 수 없습니다. 그리고 두 번째 불완전성 정리 진술은 다음과 같습니다.

논의 및 시사점

불완전한 결과는 수학의 철학, 특히 형식 논리의 단일 시스템을 사용하여 그들의 원리를 정의하는 형식주의 버전에 영향을 미칩니다.

논리학과 힐베르트의 두 번째 문제에 대한 결과

불완전성 정리는 논리학 측면에서 자연수를 정의하는 것을 목표로 한 고틀롭 프레지와 버트런드 러셀이 제안한 논리학 프로그램에 심각한 결과를 초래한다고 생각되기도 합니다.^[15] 밥 헤일(Bob Hale)과 크리스핀 라이트(Crispin Wright)는 불완전성 정리가 산술과 마찬가지로 1차 논리에도 동일하게 적용되기 때문에 논리학의 문제가 아니라고 주장합니다. 그들은 자연수가 1차 논리의 관점에서 정의되어야 한다고 믿는 사람들만이 이 문제를 가지고 있다고 주장합니다.

많은 논리학자들은 괴델의 불완전성 정리가 수학에 대한 유한한 일관성 증명을 요구한 데이비드 힐베르트의 두 번째 문제에 치명타를 가했다고 믿고 있습니다. 특히 두 번째 불완전성 정리는 종종 문제를 불가능하게 만드는 것으로 간주됩니다. 그러나 모든 수학자들이 이 분석에 동의하는 것은 아니며, 힐베르트의 두 번째 문제의 지위는 아직 결정되지 않았습니다("문제의 지위에 대한 현대적 관점" 참조).

정신과 기계

철학자 J.R. 루카스와 물리학자 로저 펜로즈를 포함한 저자들은 괴델의 불완전성 정리가 인간의 지능에 대해 암시하는 것이 무엇인지에 대해 논의했습니다. 논쟁의 대부분은 인간의 마음이 튜링 기계와 동등한지 아니면 교회-튜링 이론에 의해 어떤 유한한 기계와 동등한지에 초점을 맞추고 있습니다. 만약 그렇다면, 그리고 만약 기계가 일관성이 있다면 괴델의 불완전성 정리가 거기에 적용될 것입니다.

Putnam (1960)은 괴델의 정리가 인간에게 적용될 수는 없지만, 실수를 저지르고 따라서 일관성이 없기 때문에 과학 또는 수학 일반의 인간 교수진에 적용될 수 있다고 제안했습니다. 일관성이 있다고 가정하면 일관성을 증명할 수 없거나 튜링 기계로 표현할 수 없습니다.^[16]

Wigderson(2010)은 수학적 "지식"의 개념이 논리적 결정 가능성보다는 계산 복잡성에 기초해야 한다고 제안했습니다. 그는 "알 수 있는 가능성이 현대 표준, 즉 계산 복잡성을 통해 해석될 때 괴델 현상은 우리와 매우 밀접합니다."라고 썼습니다.^[17]

더글러스 호프스태터(Douglas Hofstadter)는 그의 저서 괴델(Gödel), 에셔(Escher), 바흐(Bach and I Am a Strange Loop)에서 괴델의 정리를 그가 말하는 이상한 고리, 즉 공리적 형식 체계 내에 존재하는 계층적이고 자기 참조적인 구조의 예로 인용합니다. 그는 이것이 인간의 마음에서 의식, 즉 '나'라는 감각을 발생시키는 것과 같은 종류의 구조라고 주장합니다. 괴델 정리의 자기 참조는 괴델 문장이 수학 원리의 공식 체계 내에서 증명 불가능성을 주장하는 데서 나온 것이지만, 인간의 마음에서 자기 참조는 뇌가 개념에 반응하는 "기호" 또는 뉴런 그룹으로 자극을 추상화하고 분류하는 방법에서 나온 것입니다. 실질적으로 형식적인 시스템이며, 결국 인식을 수행하는 바로 그 실체의 개념을 모델링하는 기호를 생성합니다. 호프스태터(Hofstadter)는 충분히 복잡한 형식 체계의 이상한 고리가 원인과 결과의 정상적인 계층 구조가 거꾸로 뒤집히는 상황인 "아래" 또는 "위아래" 인과 관계를 발생시킬 수 있다고 주장합니다. 괴델 정리의 경우, 이는 간단히 말해 다음과 같이 나타납니다.

공식의 의미를 아는 것만으로도, 사람은 그것을 구태의연하게 유도하기 위한 노력 없이 그것의 참 또는 거짓을 추론할 수 있고, 그것은 사람이 공리로부터 체계적으로 "위로" 터벅터벅 걸어가야 하는 것을 요구합니다. 이것은 단지 특이한 것이 아닙니다. 그것은 놀랍습니다. 일반적으로 수학적 추측이 말하는 것을 보고 그 진술이 참인지 거짓인지를 추론하기 위해 그 진술의 내용에 단순히 호소할 수는 없습니다.^[18]

훨씬 더 복잡한 형식적 체계인 정신의 경우, 이 '하향 인과성'은 호프스태터가 보기에, 우리 정신의 인과성이 높은 수준의 욕망, 개념, 성격, 생각, 관념에 있다는 설명할 수 없는 인간 본능으로 나타나는데, 물리학에 따르면 후자가 인과력을 가지고 있는 것처럼 보이지만 뉴런이나 심지어 기본 입자 사이의 낮은 수준의 상호작용보다는 오히려 더 중요합니다.

따라서 우리의 정상적인 인간이 세상을 인식하는 방식에는 이상한 반전이 있습니다: 비록 작은 것의 영역이 실제 모터 구동 현실이 존재하는 곳처럼 보이지만, 우리는 "작은 것"이 아닌 "큰 것"을 인식하도록 만들어졌습니다.^[18]

파코일런트 논리

괴델의 정리는 일반적으로 고전 논리학의 맥락에서 연구되지만, 역설적인 논리학과 본질적으로 모순되는 진술(dialtheia)의 연구에서도 역할을 합니다. 프리스트(1984, 2006)는 괴델 정리의 형식적 증명 개념을 형식적 증명의 일반적인 개념으로 대체하면 순진한 수학이 일관되지 않음을 보여주는 데 사용할 수 있다고 주장하며, 이를 대화론의 증거로 사용합니다.^[19] 이러한 불일치의 원인은 시스템의 언어 내에 시스템에 대한 진리 술어를 포함시키기 때문입니다.^[20] 샤피로(2002)는 괴델의 이론을 사용하여 신학을 해석하는 데 좀 더 혼합된 평가를 제공합니다.^[21]

다른 분야의 불완전성 정리에 대한 호소

수학과 논리를 뛰어넘는 논증을 뒷받침하는 정리의 불완전성에 대한 호소와 유사성이 제기되기도 합니다. Franzén(2005), Raatikainen(2005), Sokal & Bricmont(1999), Stangroom & Benson(2006) 등 여러 저자가 그러한 확장과 해석에 대해 부정적인 의견을 제시했습니다.^[22] 예를 들어 Sokal & Bricmont (1999)와 Stangroom & Benson (2006)은 괴델이 공언한 플라톤주의와 그의 아이디어가 때때로 적용되는 반실재론적 사용 사이의 차이에 대한 레베카 골드스타인의 논평을 인용합니다. Sokal & Bricmont (1999)는 사회학의 맥락에서 레기스 데브레이의 정리 발동을 비판하고, 데브레이는 이 사용을 은유적(ibid)^[23]이라고 옹호했습니다.

역사

1929년 괴델이 박사 논문으로 완전성 정리의 증명을 발표한 후, 그는 그의 고난에 대한 두 번째 문제로 눈을 돌렸습니다. 그의 원래 목표는 힐베르트의 두 번째 문제에 대한 긍정적인 해결책을 얻는 것이었습니다.^[24] 당시 2차 산술과 유사한 자연수와 실수에 대한 이론은 '해석'으로 알려졌고, 자연수에 대한 이론만 '산술'로 알려졌습니다.

일관성 문제를 연구하는 사람은 괴델뿐만이 아니었습니다. 애커먼은 1925년에 분석을 위한 결함 있는 일관성 증명을 발표했는데, 그는 원래 힐베르트가 개발한 ε 대체 방법을 사용하려고 시도했습니다. 그해 말 폰 노이만은 귀납법의 공리 없이도 산술 체계에 대한 증명을 수정할 수 있었습니다. 1928년에 애커먼은 수정된 증명을 버네이스에게 전달했고, 이 수정된 증명으로 인해 힐베르트는 1929년에 산술의 일관성이 입증되었으며 분석에 대한 일관된 증명이 곧 뒤따를 것이라는 자신의 믿음을 발표했습니다. 불완전성 정리들이 발표된 후, 아커만의 수정된 증명은 틀림없이 오류일 것이라는 것이 밝혀진 후, 폰 노이만은 그것의 주요 기법이 불건전하다는 것을 보여주는 구체적인 예를 제시했습니다.^[25]

연구 과정에서 괴델은 거짓을 주장하는 문장은 역설을 초래하지만, 증명 불가능을 주장하는 문장은 역설을 초래하지 않는다는 사실을 발견했습니다. 특히 괴델은 타르스키의 무한성 정리라고 불리는 결과를 알고 있었지만, 그는 그것을 발표한 적이 없었습니다. 1930년 8월 26일 괴델은 카르납, 페이겔, 와이스만에게 자신의 첫 번째 불완전성 정리를 발표했고, 네 사람 모두 다음 주에 쾨니히스베르크에서 열리는 핵심 회의인 정확한 과학의 인식론에 관한 제2차 회의에 참석했습니다.

알리다

1930년 쾨니히스베르크 회의는 당시 주요 논리학자들이 대거 참석한 가운데 열린 3개 학회의 합동 회의였습니다. 카르납, 헤이팅, 폰 노이만은 각각 논리학, 직관학, 형식주의의 수학철학에 대해 1시간 동안 연설했습니다.^[26] 회의에는 힐베르트가 괴팅겐 대학교에서 퇴임할 때 한 은퇴 연설도 포함되어 있었습니다. 힐베르트는 이 연설을 모든 수학 문제가 해결될 수 있다는 자신의 신념을 주장하기 위해 사용했습니다. 그는 이렇게 말하면서 연설을 마쳤습니다.

수학자에게는 이그나비무스가 없고, 내 생각에는 자연과학에도 전혀 없습니다. 아무도 해결할 수 없는 문제를 찾아내는 데 성공한 진정한 이유는 제 생각에는 해결할 수 없는 문제가 없기 때문입니다. 어리석은 이그나비무스와는 대조적으로, 우리의 신봉자들은 다음과 같습니다. 우리는 알아야 합니다. 우리는 알게 될 것입니다!

이 연설은 힐베르트의 수학에 대한 신념을 요약한 것으로 빠르게 알려지게 되었습니다. 1943년 힐베르트의 비문으로 사용되었다. 괴델이 힐베르트의 연설에 참석했을 가능성이 높았지만, 두 사람은 결코 마주치지 않았습니다.^[27]

회의 셋째 날 원탁 토론 세션에서 괴델은 자신의 첫 번째 불완전성 정리를 발표했습니다. 이 발표는 괴델을 대화를 위해 옆으로 빼낸 폰 노이만을 제외하고는 거의 관심을 끌지 못했습니다. 그해 말, 폰 노이만은 첫 번째 불완전성 정리에 대한 지식을 가지고 독립적으로 작업하여 두 번째 불완전성 정리의 증명을 얻었으며, 1930년 11월 20일자 편지에서 괴델에게 이를 발표했습니다.^[28] 괴델은 두 번째 불완전성 정리를 독자적으로 얻어 1930년 11월 17일 모나셰프테퓌르 수학이 받은 제출된 원고에 포함시켰습니다.

괴델의 논문은 1931년 모나셰프테지에 "Uber formal unentscheidbare Säzze der Principia Mathematical and verwandter Systeme I" ("Principia Mathematica and related systeme I")이라는 제목으로 발표되었습니다. 제목에서 알 수 있듯이 괴델은 원래 모나셰프테의 다음 권에 논문의 두 번째 부분을 발표할 계획이었습니다. 첫 번째 논문을 신속하게 수용한 것이 그가 계획을 변경한 한 가지 이유였습니다.^[29]

일반화 및 수용

괴델은 1933-1934년에 프린스턴에서 처치, 클린, 로서를 포함한 청중들에게 자신의 정리에 대한 일련의 강의를 했습니다. 이때까지 괴델은 자신의 정리가 요구하는 핵심 속성은 시스템이 효과적이어야 한다는 것을 파악했습니다(당시에는 일반 재귀적이라는 용어가 사용되었습니다). 1936년 로서는 괴델의 원래 증명에서 필수적인 부분이었던 ω 일관성 가설을 괴델 문장을 적절히 변경하면 단순한 일관성으로 대체할 수 있음을 증명했습니다. 이러한 발전은 본질적으로 현대적인 형태로 불완전성 정리를 남겼습니다.

Gentzen은 1936년 1차 산술에 대한 일관성 증명을 발표했습니다. 힐베르트는 이 증명을 (괴델의 정리가 이미 보여주었듯이) 일관성이 증명되고 있는 산술 체계 내에서 공식화할 수는 없지만 "무한한" 것으로 받아들였습니다.

불완전성 정리가 힐베르트의 프로그램에 미친 영향은 빠르게 실현되었습니다. 베르네이스는 ε 대체 방법에 대한 아커만의 추가적인 결과와 젠첸의 산술 일관성 증명과 함께 그룬들라겐데르마틱(1939) 제2권에 불완전성 정리에 대한 완전한 증명을 포함시켰습니다. 이것은 두 번째 불완전성 정리에 대한 최초의 완전한 증명이었습니다.

비평

핀슬러

핀슬러(1926)는 리차드 역설의 버전을 사용하여 그가 개발한 특정한 비공식적인 프레임워크에서 거짓이지만 증명할 수 없는 표현을 구성했습니다.^[30] 괴델은 불완전성 정리를 증명할 때 이 논문을 알지 못했습니다. IV., 페이지 9). 핀슬러는 1931년 괴델에게 편지를 써서 이 논문에 대해 알려주었는데, 핀슬러는 이 논문이 불완전성 정리에 우선순위가 있다고 생각했습니다. 핀슬러의 방법은 형식화된 증명 가능성에 의존하지 않고 괴델의 연구와 피상적인 유사성만 있었습니다.^[31] 괴델은 그 논문을 읽었지만 그것에 깊은 결함이 있다는 것을 발견했고, 핀슬러에 대한 그의 반응은 형식화의 부족에 대한 우려를 나타냈습니다.^[32] 핀슬러는 남은 경력 동안 형식화를 피한 수학 철학을 계속 주장했습니다.

저멜로

1931년 9월, 에른스트 제르멜로는 괴델에게 편지를 써서 괴델의 주장에서 "본질적인 차이"라고 묘사한 것을 발표했습니다.^[33] 10월에 괴델은 10페이지짜리 편지로 답장을 보냈는데, 여기서 그는 제르멜로가 어떤 체계에서 진리의 개념이 그 체계에서 정의 가능하다고 잘못 가정했다고 지적했습니다. 일반적으로 타르스키의 정의 불가능 정리에 의해 사실이 아닙니다.^[34] 그러나, 제르멜로는 멈추지 않고 "젊은 경쟁자에 대한 다소 신랄한 단락"과 함께 자신의 비판을 인쇄물로 출판했습니다.^[35] 괴델은 그 문제를 더 이상 추구하는 것이 무의미하다고 판단했고 카르납은 동의했습니다.^[36] 제르멜로의 후속 연구의 대부분은 수학 이론의 일관성과 범주성을 모두 보여주기를 바랐던 1차 논리보다 강한 논리와 관련이 있었습니다.

비트겐슈타인

루트비히 비트겐슈타인은 1953년 "수학의 기초에 관한 발언"에서 사후에 발표된 불완전성 정리에 대한 여러 구절을 썼는데, 특히 러셀의 체계에서 "참"과 "증명할 수 있는" 개념을 혼동하는 것처럼 보이는 한 섹션은 때때로 "명백한 단락"이라고 불립니다. 괴델은 비트겐슈타인의 초기 이상적인 언어 철학과 Tractatus Logico-Philosophicus가 원의 사고를 지배했던 시기에 빈 원의 일원이었습니다. 비트겐슈타인이 불완전성 정리를 잘못 이해한 것인지, 아니면 그저 불분명하게 표현한 것인지에 대해서는 논란이 좀 있었습니다. 괴델의 나클라스에 실린 글들은 비트겐슈타인이 자신의 생각을 잘못 읽었다는 믿음을 표현하고 있습니다.

플로이드 & 푸트남(2000)과 프리스트(2004)는 대부분의 해설이 비트겐슈타인을 오해하고 있다고 주장하는 텍스트 판독을 제공했지만, 여러 해설자들은 비트겐슈타인을 괴델을 오해하고 있다고 읽었습니다.^[37] 버네이스, 뒤메트, 크라이젤은 발표에서 비트겐슈타인의 발언에 대해 별도의 리뷰를 작성했는데, 모두 극도로 부정적이었습니다.^[38] 이러한 비판의 만장일치는 비트겐슈타인의 불완전성 정리에 대한 발언이 논리계에 별다른 영향을 미치지 못하게 만들었습니다. 1972년 괴델은 다음과 같이 말했습니다. "비트겐슈타인은 정신을 잃었습니까? 진심입니까? 그는 의도적으로 말도 안 되는 진술들을 내뱉었고, 비트겐슈타인의 언급은 불완전성 정리 작성에 대한 오해를 보여준다고 칼 멩거에게 썼습니다.

비트겐슈타인이 [첫 번째 불완전성 정리]를 이해하지 못했거나 이해하지 못하는 척 했다는 것은 여러분이 인용하는 구절에서 분명히 알 수 있습니다. 그는 그것을 일종의 논리적 역설로 해석했지만, 사실은 그 반대, 즉 수학의 절대적으로 논쟁의 여지가 없는 부분(무한수 이론 또는 조합론) 내의 수학적 정리입니다.^[39]

2000년 비트겐슈타인의 나클라스가 발표된 이후 일련의 철학 논문들은 비트겐슈타인의 발언에 대한 원래의 비판이 정당한지를 평가하고자 했습니다. Floyd & Putnam(2000)은 비트겐슈타인이 이전에 가정한 것보다 불완전성 정리를 더 완벽하게 이해했다고 주장합니다. 그들은 특히 ω 불일치 시스템에 대한 괴델 문장을 "나는 증명할 수 없다"고 해석하는 것에 관심을 갖는데, 이는 시스템에 증명 가능성 술어가 실제 증명 가능성에 해당하는 모델이 없기 때문입니다. Rodych(2003)는 비트겐슈타인에 대한 그들의 해석이 역사적으로 정당하지 않다고 주장합니다. Berto(2009)는 비트겐슈타인의 글과 역설적 논리 이론의 관계를 탐구합니다.^[40]

참고 항목

참고문헌

인용문

괴델의 기사

• Kurt Gödel, 1931, "Uber formal unentscheidbare Säzze der Principia Mathematical undverwandter Systeme, I", Monatshefte für Matheik und Physik, v. 38 n. 1, pp. 173–198. doi:10.1007/BF01700692
• —, 1931, 솔로몬 페퍼만, 1986, "Uber formal unentscheidbare Säzze der Principia Mathematical and verwandter Systeme, I". 쿠르트 괴델 작품집, 권. I. 옥스퍼드 대학교 출판부, 144-195쪽. ISBN 978-0195147209. 스티븐 콜 클린의 소개에 앞서 영어로 번역된 독일어 원본.
• —, 1951, 솔로몬 페퍼먼, 에드., 1995, "수학의 기초와 그 함의에 관한 몇 가지 기본 정리". 쿠르트 괴델 작품집, 권. III, 옥스퍼드 대학교 출판부, 304-323쪽. ISBN 978-0195147223.

괴델의 논문을 영어로 번역한 것.

다음 중 어느 것도 모든 번역어와 타이포그래피에서 일치하지 않습니다. 타이포그래피는 심각한 문제인데, 괴델은 분명히 "이전에 그들의 일상적인 의미에서 정의되었던 메타수학적 개념들"을 강조하기를 원했기 때문입니다(van Heijenoort 1967, p. 595). 세 가지 번역이 존재합니다. 최초의 존 도슨(John Dawson)은 다음과 같이 말합니다. "Meltzer 번역은 심각하게 부족했고 상징 논리 저널(Journal of Symbol Logic)에서 파괴적인 리뷰를 받았습니다." "Gödel은 Braithweite의 논평에 대해서도 불평했습니다(Dawson 1997, p. 216). "다행히도, 멜처 번역본은 엘리엇 멘델슨이 마틴 데이비스의 문집 "미결의"를 위해 준비한 더 나은 번역본으로 대체되었습니다. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . (각주에서 도슨은 "출판된 책은 엉성한 타이포그래피와 수많은 오판으로 얼룩져 있었기 때문에 그는 그의 준수를 후회할 것입니다."(ibid)라고 말합니다. 도슨은 "괴델이 선호한 번역은 장 판 하이에노르트의 번역이었다"(ibid). 진지한 학생에게는 스티븐 클린과 J. B.가 녹음한 강의 노트 세트로 또 다른 버전이 존재합니다. 로서 "1934년 봄 괴델라트가 고등연구소에 강의하는 동안"(데이비스 1965, p. 39 및 p. 41 시작), 이 버전은 "공식 수학 체계의 결정할 수 없는 명제에 관하여"라는 제목입니다. 출판 순서는 다음과 같습니다.

• B. Meltzer (번역) and R. Braithwaite (소개), 1962. Principia Mathematica와 관련 시스템의 공식적으로 결정되지 않은 명제에 대하여, 뉴욕 도버 출판사(Dover Edition 1992), ISBN 0-486-66980-7(pbk. 여기에는 33-34페이지에 있는 괴델의 독일어 약어의 유용한 번역이 포함되어 있습니다. 위에서 언급했듯이 타이포그래피, 번역 및 해설이 의심됩니다. 불행히도, 이 번역은 모든 의심스러운 내용과 함께 다시 인쇄되었습니다.

• 스티븐 호킹 편집자, 2005. 신이 정수를 창조했습니다. 역사를 바꾼 수학적 돌파구, 러닝 프레스, 필라델피아, ISBN 0-7624-1922-9 괴델의 논문은 1097년에, 호킹의 논평은 1089년에 시작합니다.

• 마틴 데이비스 편집자, 1965. 결정할 수 없는 것: 결정할 수 없는 명제, 해결할 수 없는 문제 및 계산 가능한 함수에 대한 기본 논문, 뉴욕 레이븐 프레스, ISBN 없음. 괴델의 논문은 5페이지에서 시작하여 한 페이지의 해설이 뒤따릅니다.
• 장 반 하이에노르트 편집자, 1967, 제3판 1967. 프레게에서 괴델까지: 수학 논리학의 원천책, 1879-1931, 하버드 대학교 출판부, 케임브리지 매스, ISBN 0-674-32449-8(pbk). van Heijenoort가 번역을 했습니다. 그는 "괴델 교수가 번역을 승인했고, 이는 많은 곳에서 그의 희망에 부응했습니다."(595쪽)라고 말합니다. 괴델의 논문은 595쪽에서 시작하고, 판 하이에노르트의 해설은 592쪽에서 시작합니다.
• 마틴 데이비스 편집자, 1965, I bid. "공식적인 수학 체계의 결정할 수 없는 명제에 관하여" 41페이지에서 괴델의 에라타 수정본과 괴델의 주석이 추가된 사본이 시작되고 데이비스의 주석이 두 페이지 앞서 나옵니다. 데이비스가 이것을 그의 책에 포함시키기 전까지 이 강의는 단지 마임그래프로 된 노트로만 존재했습니다.

타인에 의한 기사

• Boolos, George (1989). "A New Proof of the Gödel Incompleteness Theorem". Notices of the American Mathematical Society. 36: 388–390, 676. reprinted in Boolos (1998, pp. 383–388)
• Boolos, George (1998). Logic, logic, and logic. Harvard University Press. p. 443. ISBN 0-674-53766-1.
• Bernd Buldt, 2014, "Gödel의 첫 번째 불완전성 정리의 범위 2016-03-06 at the Wayback Machine", Logica Universalis, v. 8, pp. 499-552. doi:10.1007/s11787-014-0107-3
• Charlesworth, Arthur (1981). "A Proof of Godel's Theorem in Terms of Computer Programs". Mathematics Magazine. 54 (3): 109–121. doi:10.2307/2689794. JSTOR 2689794.
• Davis, Martin (1965). The Undecidable: Basic Papers on Undecidable Propositions, Unsolvable Problems and Computable Functions. Raven Press. ISBN 978-0-911216-01-1.
• Davis, Martin (2006). "The Incompleteness Theorem" (PDF). Notices of the AMS. 53 (4): 414.
• Finsler, Paul (1926). "Formale Beweise und die Entscheidbarkeit". Mathematische Zeitschrift. 25: 676–682. doi:10.1007/bf01283861. S2CID 121054124.
• Grattan-Guinness, Ivor, ed. (2005). Landmark Writings in Western Mathematics 1640-1940. Elsevier. ISBN 9780444508713.
• van Heijenoort, Jean (1967). "Gödel's Theorem". In Edwards, Paul (ed.). Encyclopedia of Philosophy. Vol. 3. Macmillan. pp. 348–357.
• Hellman, Geoffrey (1981). "How to Gödel a Frege-Russell: Gödel's Incompleteness Theorems and Logicism". Noûs. 15 (4 - Special Issue on Philosophy of Mathematics): 451–468. doi:10.2307/2214847. ISSN 0029-4624. JSTOR 2214847.
• 데이비드 힐버트, 1900, "수학적 문제" 힐베르트의 두 번째 문제에 대한 진술을 담은 파리 국제수학자대회에 앞서 강연한 내용을 영어로 번역한 것입니다.
• 마틴 히르젤, 2000, "수학 원리와 관련 시스템 I의 공식적으로 결정할 수 없는 명제에 대해." 괴델의 논문을 영어로 번역한 것. 원본에서 보관됩니다. 2004년 9월 16일.
• Kikuchi, Makoto; Tanaka, Kazuyuki (July 1994). "On Formalization of Model-Theoretic Proofs of Gödel's Theorems". Notre Dame Journal of Formal Logic. 35 (3): 403–412. doi:10.1305/ndjfl/1040511346. MR 1326122.
• Kleene, S. C. (1943). "Recursive predicates and quantifiers". Transactions of the American Mathematical Society. 53 (1): 41–73. doi:10.1090/S0002-9947-1943-0007371-8. 데이비스 1965년 재인쇄, 페이지 255-287
• Raatikainen, Panu (2020). "Gödel's Incompleteness Theorems". Stanford Encyclopedia of Philosophy. Retrieved November 7, 2022.
• Raatikainen, Panu (2005). "On the philosophical relevance of Gödel's incompleteness theorems". Revue Internationale de Philosophie. 59 (4): 513–534. doi:10.3917/rip.234.0513. S2CID 52083793.
• 존 바클리 로서, 1936, "괴델과 교회의 일부 이론의 확장", 상징 논리 저널 v. 1 (1936) pp. 87–91, 마틴 데이비스 1965, 결정되지 않은 (loc. cit.) pp. 230–235.
• —, 1939, "괴델 정리와 교회 정리의 증명에 대한 비공식적인 설명", 상징 논리학 저널에서 재인쇄, v. 4 (1939) pp. 53–60, Martin Davis 1965, The Uncredible (loc. cit.) pp. 223–230
• Smoryński, C. (1977). "The incompleteness theorems". In Jon Barwise (ed.). Handbook of mathematical logic. Amsterdam: North-Holland Pub. Co. pp. 821–866. ISBN 978-0-444-86388-1.
• Willard, Dan E. (2001). "Self-Verifying Axiom Systems, the Incompleteness Theorem and Related Reflection Principles". Journal of Symbolic Logic. 66 (2): 536–596. doi:10.2307/2695030. JSTOR 2695030.
• Zach, Richard (2003). "The Practice of Finitism: Epsilon Calculus and Consistency Proofs in Hilbert's Program" (PDF). Synthese. Springer Science and Business Media LLC. 137 (1): 211–259. arXiv:math/0102189. doi:10.1023/a:1026247421383. ISSN 0039-7857. S2CID 16657040.
• Zach, Richard (2005). "Kurt Gödel, paper on the incompleteness theorems (1931)". In Grattan-Guinness, Ivor (ed.). Landmark Writings in Western Mathematics 1640-1940. Elsevier. pp. 917–925. doi:10.1016/b978-044450871-3/50152-2. ISBN 9780444508713.

정리에 관한 책들

• 프란체스코 베르토. 괴델에 관한 것이 있습니다. 불완전성 정리에 대한 완전한 가이드 존 와일리와 아들들. 2010.
• 노버트 도미센, 1990. Logik der Antinomien. 베른: 피터 랭. 142 S. 1990. ISBN 3-261-04214-1. Zbl 0724.03003.
• Franzén, Torkel (2005). Gödel's theorem : an incomplete guide to its use and abuse. Wellesley, MA: A K Peters. ISBN 1-56881-238-8. MR 2146326.
• 더글러스 호프스태터, 1979. 괴델, 에셔, 바흐: 영원한 황금 땋음. 빈티지 북스. ISBN 0-465-02685-0. 1999 reprint: ISBN 0-465-02656-7. MR530196
• —, 2007. 나는 이상한 고리입니다. 기본서. ISBN 978-0-465-03078-1. ISBN 0-465-03078-5. MR2360307
• 스탠리 자키, OSB, 2005. 양의 드라마. Real View Books.
• Per Lindström, 1997. 불완전성의 측면, 논리 v. 10의 강의 노트.
• J.R. 루카스, FBA, 1970. 의지의 자유. Clarendon Press, Oxford, 1970.
• 에이드리언 윌리엄 무어, 2022. 괴델 정리: 아주 짧은 소개. 옥스퍼드 대학교 출판부, 옥스포드, 2022.
• 어니스트 네이글, 제임스 로이 뉴먼, 더글러스 호프스태터, 2002(1958). 괴델의 증명, 수정. ISBN 0-8147-5816-9. MR1871678
• 루디 러커, 1995 (1982). Infinity and the Mind: 무한의 과학과 철학. 프린스턴 대학교 누르다. MR658492
• Smith, Peter (2007). An introduction to Gödel's Theorems. Cambridge, U.K.: Cambridge University Press. ISBN 978-0-521-67453-9. MR 2384958.
• Shankar, N. (1994). Metamathematics, machines, and Gödel's proof. Cambridge tracts in theoretical computer science. Vol. 38. Cambridge: Cambridge University Press. ISBN 0-521-58533-3.
• Raymond Smulyan, 1987. 영원히 미정 ISBN 0192801414 - 형식적 체계에서 미정성을 기준으로 한 퍼즐
• —, 1991. 고델의 불완전성 정리. 옥스퍼드 대학교 누르다.
• —, 1994. 대각선화 및 자기 참조. 옥스퍼드 대학교 누르다. MR1318913
• —, 2013. 고델리안 퍼즐북: 퍼즐, 역설과 증명. 택배회사. ISBN 978-0-486-49705-1.
• Wang, Hao (1996). A Logical Journey: From Gödel to Philosophy. MIT Press. ISBN 0-262-23189-1. 미스터1433803

기타참고문헌

• Berto, Francesco (2009). "The Gödel Paradox and Wittgenstein's Reasons". Philosophia Mathematica. III (17).
• Dawson, John W. Jr. (1996). Logical dilemmas: The life and work of Kurt Gödel. Taylor & Francis. ISBN 978-1-56881-025-6.
• Dawson, John W. Jr. (1997). Logical dilemmas: The life and work of Kurt Gödel. Wellesley, Massachusetts: A. K. Peters. ISBN 978-1-56881-256-4. OCLC 36104240.
• 레베카 골드스타인, 2005, 불완전성: 커트 괴델의 증명과 역설, W. W. 노튼 & 컴퍼니. ISBN 0-393-05169-2
• Floyd, Juliet; Putnam, Hilary (2000). "A Note on Wittgenstein's "Notorious Paragraph" about the Godel Theorem". The Journal of Philosophy. JSTOR. 97 (11): 624–632. doi:10.2307/2678455. ISSN 0022-362X. JSTOR 2678455.
• Harrison, J. (2009). Handbook of practical logic and automated reasoning. Cambridge: Cambridge University Press. ISBN 978-0521899574.
• 데이비드 힐버트와 폴 버네이스, 그룬들라겐 더 수학, 스프링어-베를라그.
• Hopcroft, John E.; Ullman, Jeffrey (1979). Introduction to Automata Theory, Languages, and Computation. Reading, Mass.: Addison-Wesley. ISBN 0-201-02988-X.
• Hofstadter, Douglas R. (2007) [2003]. "Chapter 12. On Downward Causality". I Am a Strange Loop. Basic Books. ISBN 978-0-465-03078-1.
• Jones, James P. (1980). "Undecidable Diophantine Equations" (PDF). Bulletin of the American Mathematical Society. 3 (2): 859–862. doi:10.1090/S0273-0979-1980-14832-6.
• Kleene, Stephen Cole (1967). Mathematical Logic. 도버 재인쇄, 2002. ISBN 0-486-42533-9
• O'Connor, Russell (2005). "Essential Incompleteness of Arithmetic Verified by Coq". Theorem Proving in Higher Order Logics. Lecture Notes in Computer Science. Vol. 3603. pp. 245–260. arXiv:cs/0505034. doi:10.1007/11541868_16. ISBN 978-3-540-28372-0. S2CID 15610367.
• Paulson, Lawrence (2014). "A machine-assisted proof of Gödel's incompleteness theorems for the theory of hereditarily finite sets". Review of Symbolic Logic. 7 (3): 484–498. arXiv:2104.14260. doi:10.1017/S1755020314000112. S2CID 13913592.
• Priest, Graham (1984). "Logic of Paradox Revisited". Journal of Philosophical Logic. 13 (2): 153–179.
• Priest, Graham (2004). "Wittgenstein's Remarks on Gödel's Theorem". In Max Kölbel (ed.). Wittgenstein's lasting significance. Psychology Press. pp. 207–227. ISBN 978-1-134-40617-3.
• Priest, Graham (2006). In Contradiction: A Study of the Transconsistent. Oxford University Press. ISBN 0-19-926329-9.
• Putnam, Hilary (1960). "Minds and Machines". In Sidney Hook (ed.). Dimensions of Mind: A Symposium. New York University Press. Anderson, A. R., Ed., 1964에서 재인쇄. Minds and Machine. 프렌티스 홀: 77.
• Wolfgang Rautenberg, 2010, 수학 논리학의 간결한 개론, 3th. ed., Springer, ISBN 978-1-4419-1220-6
• Rodych, Victor (2003). "Misunderstanding Gödel: New Arguments about Wittgenstein and New Remarks by Wittgenstein". Dialectica. 57 (3): 279–313. doi:10.1111/j.1746-8361.2003.tb00272.x. doi:10.1111/j.1746-8361.2003.tb00272.x
• Shelah, Saharon (1974). "Infinite Abelian groups, Whitehead problem and some constructions". Israel Journal of Mathematics. 18 (3): 243–256. doi:10.1007/BF02757281. MR 0357114.
• Shapiro, Stewart (2002). "Incompleteness and Inconsistency". Mind. 111: 817–32. doi:10.1093/mind/111.444.817.
• Sokal, Alan; Bricmont, Jean (1999). Fashionable Nonsense: Postmodern Intellectuals' Abuse of Science. Picador. ISBN 0-312-20407-8.
• Shoenfield, Joseph R. (1967). Mathematical logic. Natick, Mass.: Association for Symbolic Logic (published 2001). ISBN 978-1-56881-135-2.
• Stangroom, Jeremy; Benson, Ophelia (2006). Why Truth Matters. Continuum. ISBN 0-8264-9528-1.
• George Tourlakis, 논리학과 집합론 강의, 1권, 수학 논리학, 캠브리지 대학 출판부, 2003. ISBN 978-0-521-75373-9
• Wigderson, Avi (2010). "The Gödel Phenomena in Mathematics: A Modern View" (PDF). Kurt Gödel and the Foundations of Mathematics: Horizons of Truth. Cambridge University Press.
• 하오왕, 1996, 논리적 여정: 괴델에서 철학으로, MIT 출판사, 케임브리지 MA, ISBN 0-262-23189-1.
• Zach, Richard (2007). "Hilbert's Program Then and Now". In Jacquette, Dale (ed.). Philosophy of logic. Handbook of the Philosophy of Science. Vol. 5. Amsterdam: Elsevier. pp. 411–447. arXiv:math/0508572. doi:10.1016/b978-044451541-4/50014-2. ISBN 978-0-444-51541-4. OCLC 162131413. S2CID 291599.

외부 링크

• BBC에서 고델의 우리 시대 불완전성 정리
• 2011년 7월 5일, 스탠포드 철학 백과사전에 실린 줄리엣 케네디의 "커트 괴델" 항목.
• 2013년 11월 11일, 스탠포드 철학 백과사전에 실린 파누 라티카이넨의 "괴델의 불완전성 정리" 항목.
• 스탠포드 철학 백과사전의 역설적 논리 § 산술과 괴델 정리 항목.
• 맥튜터 전기:
  • 쿠르트 괴델. Wayback Machine에서 아카이브된 2005-10-13
  • 게르하르트 젠첸.
• 수학이란 무엇입니까?칼리스 포디익스의 괴델 정리와 어라운드. 온라인 무료 책.
• 인쇄기를 예로 들어 괴델의 정리를 세계에서 가장 짧게 설명한 것.
• 2011년 10월 라디오랩에서 괴델의 불완전성 정리에 관한 에피소드/포함
• "Gödel incompleteness theorem", Encyclopedia of Mathematics, EMS Press, 2001 [1994]
• 괴델의 증명은 어떻게 작동하는가, 나탈리 월초버, 콴타 매거진, 2020년 7월 14일.
• [1]그리고 [2] 이자벨/HOL에서 공식화된 괴델의 불완전성 정리

`