겐첸의 일관성 증명
겐첸의 일관성 증명 또는 겐첸의 무모순성 증명은 1936년 게르하르트 겐첸이 발표한 수리 논리학의 갈래인 증명 이론의 결과이다. 이는 1차 산술의 페아노 공리가 증명에 사용된 어떤 다른 체계도 모순을 포함하지 않는 한 모순을 포함하지 않는다는 것을 보인다(즉, '무모순적'이다). 오늘날 "서수 ε0까지의 양화사-자유 초한귀납법의 추가 원리를 가진 원시적 재귀 산술"이라고 불리는 이 다른 체계는 페아노 공리계보다 약하지도 강하지도 않다. 겐첸은 페아노 산술에 포함된 의심스러운 추론 방식을 피하고 따라서 그 일관성은 논란의 여지가 적다고 주장했다.
겐첸의 정리 편집
겐첸의 정리는 1차 산술 즉, 1차 산술에 의해 공리화된 자연수의 덧셈과 곱셈을 포함한 이론과 관련이 있다. 이것은 "1차" 이론이다: 정량자는 자연수에 걸쳐 확장되지만 자연수의 집합이나 함수에 대해서는 확장되지 않는다. 이 이론은 지수, 계승 또는 피보나치 수열과 같이 재귀적으로 정의된 정수 함수를 설명할 수 있을 만큼 충분히 강하다.
겐첸은 서수 ε0까지의 양화사-자유 초한귀납법의 추가 원리를 가진 원시적 재귀 산술의 기초 이론 위에서 1차 페아노 공리의 일관성을 증명할 수 있음을 보여주었다. 원시적 재귀 산술은 훨씬 단순화된 형태의 산술로서 다소 논쟁적이지 않다. 추가 원리는 비형식적으로 유한한 뿌리가 있는 나무의 집합에 정렬순서가 있음을 의미한다. 형식적으로, ε0은 를 만족하는 첫 번째 서수 이다. 즉, 열 의 극한이다.
그것은 큰 수식보다 훨씬 작은 수식이다. 산술 언어로 서수를 표현하기 위해서는 서수 표기법이 필요하다. 즉, ε0 이하의 서수에 자연수를 할당하는 방법이 필요하다. 이는 칸토어 표준형 정리에 의한 예시 등 다양한 방법으로 행해질 수 있다. 겐첸의 증명은 다음과 같은 가정에 근거한다: 양화사 없는 공식 A(x)에 대해, A(a)가 거짓인 서수 a<ε0이 존재한다면, 이러한 서수 중 가장 작은 것이 존재한다.
겐첸은 페아노 산술에서 증명에 대한 "축소 절차"의 개념을 정의하고 있다. 주어진 증명에 대해서 이 절차는 증명의 나무를 생산하는데, 주어진 증명은 나무의 뿌리가 되고, 다른 증명은 어떤 의미에서 주어진 증명보다 "간단"하다. 이러한 증가하는 단순성은 모든 증명에 ε0보다 작은 서수를 붙임으로써 공식화되고, 나무 아래로 내려갈수록 이 서수들은 한 단계씩 더 작아진다. 그런 다음 그는 모순의 증명이 있다면, 감소 절차로 인해 양화사 없는 공식에 해당하는 증명에 대한 원시적 재귀 작용으로 생성된 ε0보다 작은 서수의 무한 순감소 서수열이 발생한다는 것을 보여준다.
힐베르트 프로그램, 괴델의 정리와의 관계 편집
겐첸의 증명은 괴델의 두 번째 불완전성 정리에서 흔히 놓친 한 측면을 강조한다. 어떤 이론의 일관성은 더 강한 이론에서만 증명될 수 있다고 주장되기도 한다. 원시 재귀산술에 정량자 없는 트랜스피나이트 유도를 더하여 얻은 겐첸의 이론은 1차적 페아노 산술(PA)의 일관성을 증명하지만 PA는 들어 있지 않다. 예를 들어, PA는 모든 공식에 대해 일반적인 수학적 유도를 증명하지 않는 반면(모든 유도의 예는 PA의 공리이기 때문이다). 그러나 젠첸의 이론은 PA에도 포함되어 있지 않은데, 이는 PA가 할 수 없는 숫자 이론적 사실 즉 PA의 일관성을 증명할 수 있기 때문이다. 그러므로 이 두 이론은 한 가지 의미에서 비할 수 없는 것이다.
그렇기는 하지만 이론의 강도를 비교할 수 있는 다른, 더 강력한 방법이 있는데, 그 중 가장 중요한 것은 해석가능성의 개념으로 정의된다. 하나의 이론 T가 다른 B에서 해석될 수 있다면, 그 이론 T가 B라면 일치한다는 것을 보여줄 수 있다. (사실, 이것은 해석성의 개념의 큰 지점이다.) 그리고, T가 극히 약하지 않다고 가정하면, T자체는 바로 다음과 같은 조건부 증명할 수 있을 것이다. B가 일관성이 있다면 T도 일치한다. 따라서 T는 두 번째 불완전성 정리로는 B가 일관성이 있다는 것을 증명할 수 없는 반면, B는 T가 일관성이 있다는 것을 증명할 수 있을 것이다. 이것이 이론을 비교하기 위해 해석력을 사용한다는 생각, 즉 B가 T를 해석하면 B가 적어도 T만큼 강하다는 생각('일관성 강도'의 의미)을 동기부여하는 것이다.
솔로몬 페퍼만의 앞선 연구를 토대로 구축하던 파벨 푸들라크가 증명했던 제2 불완전성 정리의 강력한 형태는 로빈슨 산술 Q를 포함하는 일관된 이론 T는 Q+Con(T)을 해석할 수 없다고 기술하고 있는데, T는 일관성이 있다는 진술이다. 대조적으로 Q+Con(T)은 산술화된 완전성 정리의 강력한 형태로 T를 해석한다. 그래서 Q+Con(T)은 항상 T보다 (한 가지 좋은 의미로) 강하다. 그러나 겐첸의 이론은 Q를 포함하고 콘(PA)을 증명하기 때문에 사소한 것으로 Q+Con(PA)을 해석하고, 그래서 겐첸의 이론은 PA를 해석한다. 그러나 푸들라크의 결과에 의하면 겐첸의 이론(지금 말한 바와 같이)은 Q+Con(PA)을 해석하고, 해석가능성은 타동적이기 때문에 PA는 겐첸의 이론을 해석할 수 없다. 즉, PA가 겐첸의 이론을 해석했다면, PA도 해석할 것이고, 따라서 Pudlahk의 결과에 의해 일관성이 없을 것이다. 그래서 일관성 강도의 의미에서 해석성이 특징인 것처럼 겐첸의 이론은 페아노 산술보다 강하다.
헤르만 바일은 1946년 괴델의 1931년 불완전성 결과가 수학의 일관성을 증명하려는 힐베르트의 계획에 파괴적인 영향을 미친 이후 겐첸의 일관성 결과가 갖는 의의에 대해 다음과 같은 언급을 했다.
만약 힐베르트가 그것을 성공적으로 수행할 수 있었다면, 궁극적으로 모든 수학자들은 힐베르트의 접근을 받아들였을 것이다. 첫 단계는 고무적이고 유망했다. 그러나 그 후 괴델은 엄청난 타격을 입혔고, 아직 회복되지 않았다. 괴델은 힐베르트의 형식주의에서 나타나는 기호, 공식, 공식의 순서 등을 일정한 방법으로 열거하고, 따라서 일관성의 주장을 산술 명제로 바꾸었다. 그는 이 명제가 형식주의 안에서 증명되거나 반증될 수 없다는 것을 보여줄 수 있었다. 이것은 단지 두 가지를 의미할 수 있다: 일관성의 증명서가 주어지는 추리는 시스템 내에서 공식적인 상대가 없는 어떤 주장을 포함해야 한다. 즉, 우리는 수학적 유도의 절차를 완전히 공식화하는 데 성공하지 못했다. 또는 완전히 "완성적인" 일관성의 증명에 대한 희망은 완전히 포기되어야 한다. G. 젠첸이 마침내 산술의 일관성을 증명하는 데 성공했을 때, 그는 칸토어의 "제2종 서수"에 침투하는 명백한 추리의 한 유형을 주장함으로써 실제로 그러한 한계를 통과했다.
클레네(2009년, 페이지 479년)는 1952년, 특히 힐베르트가 시작한 형식주의 프로그램의 맥락에서 겐첸의 결과의 의의에 대해 다음과 같은 논평을 했다.
정합성 입증에 의해 고전수학을 안전하게 만들자는 형식주의자들의 원래 제안은 ε0까지의 트랜스피나이트 유도 같은 방법이 사용되어야 한다는 것을 고려하지 않았다. 그 문제제정이라는 의미에서 어느 정도까지 고전이론을 확보하는 것으로 받아들여질 수 있는가는 one까지의0 유도를 최종적인 방법으로 받아들일 준비가 되어 있느냐에 따라, 개인의 판단에 관한 현 상태에 있다.
겐첸의 증명에 의해 시작된 작업 편집
겐첸의 증명은 증명 이론적 서수 분석의 첫 번째 예다. 서수 분석에서 잘 정렬된 것으로 증명될 수 있는 (구성적) 서수가 얼마나 큰지 또는 (구성적) 서수가 얼마나 큰지를 측정하여 이론의 강도를 측정한다. 구성적 서수는 자연수의 재귀적 순서의 순서 유형이다.
이 언어에서 겐첸은 1차 페아노 산술의 증명-이론 서수가 ε0임을 확립한다.
로렌스 커비와 제프 파리는 겐첸의 정리에 근거하여 1982년 굿스타인의 정리가 페아노 산술에서 증명될 수 없다는 것을 증명했다.
참조 편집
- (Gentzen & Szabo 1969)에서 "산술의 일관성"로 번역되었다.
- (Gentzen & Szabo 1969)에서 "초등번호 이론에 대한 일관성 증명의 새로운 버전"으로 번역되었다.
- 영어의 논문 번역.