겐첸의 일관성 증명

Gentzen's consistency proof

겐첸의 일관성 증명은 1936년 게르하르트 겐첸이 발표한 수학 논리의 증명 이론의 결과물이다.그것은 1차 산술의 페아노 공리가 모순을 포함하지 않는다는 것을 보여준다(즉, 증거에 사용된 어떤 다른 시스템도 모순을 포함하지 않는 한, '일관성'이다).오늘날 "서수 ε까지의0 정량자-자유 트랜스피나이트 유도의 추가 원리를 가진 1차 재귀 산술"이라고 불리는 이 다른 시스템은 페아노 공리의 시스템보다 약하지도 강하지도 않다.겐젠은 페아노 산술에 포함된 의심스러운 추론 방식을 피하고 따라서 그 일관성은 논란의 여지가 적다고 주장했다.

겐첸의 정리

겐첸의 정리는 1차 산술 즉, 1차 산술에 의해 공리화된 자연수의 덧셈과 곱셈을 포함한 이론과 관련이 있다.이것은 "1차 순서" 이론이다: 정량자는 자연수에 걸쳐 확장되지만 자연수의 집합이나 함수에 대해서는 확장되지 않는다.이 이론은 지수, 요인 또는 피보나치 수열과 같은 반복적으로 정의된 정수 함수를 설명할 수 있을 만큼 충분히 강하다.

겐젠은 1차적인 페아노 공리의 일관성이 양자 프리 트랜스핀라이트 유도라는 추가 원리를 서수 ε까지의0 원시 재귀산술의 기본이론에 대해 증명할 수 있음을 보여주었다 원시 재귀산술은 훨씬 단순화된 형태의 산술로서 다소 논쟁적이지 않다.추가 원리는 비공식적으로 유한한 뿌리가 있는 나무의 집합에 잘 정돈되어 있다는 것을 의미한다.형식적으로 ε은0 첫 서수 {\}이며,Ω = α = {\즉 수열의 한계.

그것은 큰 수식보다 훨씬 작은 수식이다.산술어로 서수를 표현하기 위해서는 서수 표기법이 필요하다. 즉, ε0 이하의 서수에 자연수를 할당하는 방법이 필요하다.이것은 칸토어의 정상적인 형태 정리에 의해 제공되는 하나의 예로서 다양한 방법으로 행해질 수 있다.겐첸의 증거는 다음과 같은 가정에 근거한다: 어떤 계량기 없는 공식 A(x)에 대해, A(a)가 거짓인 서수 a< ε이0 있다면, 적어도 그런 서수자가 있다.

겐첸은 페아노 산술에서 입증에 대한 "축소 절차"의 개념을 정의하고 있다.주어진 증명에 대해서, 그러한 절차는 증명의 나무를 생산하는데, 주어진 증서는 나무의 뿌리가 되고, 다른 증서는 어떤 의미에서는 주어진 증보다 "심플러"가 된다.이렇게 증가하는 단순성은 모든 증거에 서수 < ε0>를 붙임으로써 공식화되며, 한 사람이 나무 아래로 내려갈수록 이 서수들은 한 걸음씩 더 작아진다는 것을 보여준다.그런 다음 그는 모순의 증거가 있다면, 감소 절차로 인해 계량기 없는 공식에 해당하는 증명에 대한 원시 재귀작용으로 생성된 ord보다0 작은 수의 무한정 엄격한 하향식 서열이 발생한다는 것을 보여준다.[1]

힐베르트의 프로그램과 괴델의 정리와의 관계

겐첸의 증거는 괴델의 두 번째 불완전성 정리에서 흔히 놓친 한 측면을 강조한다.어떤 이론의 일관성은 더 강한 이론에서만 증명될 수 있다고 주장되기도 한다.원시 재귀산술에 정량자 없는 트랜스피나이트 유도를 더하여 얻은 겐첸의 이론은 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]파벨 푸들라크가 증명했던 제2 불완전성 정리의 강력한 형태는 로빈슨 산술 Q를 포함하는 일관된 이론 T는 Q+Con(T)을 해석할 수 없다고 기술하고 있는데,[3] T는 일관성이 있다는 진술이다.대조적으로 Q+Con(T)은 산술화된 완전성 정리의 강력한 형태로 T를 해석한다.그래서 Q+Con(T)은 항상 T보다 (한 가지 좋은 의미로) 강하다.그러나 겐첸의 이론은 Q를 포함하고 콘(PA)을 증명하기 때문에 사소한 것으로 Q+Con(PA)을 해석하고, 그래서 겐첸의 이론은 PA를 해석한다.그러나 푸들라크의 결과에 의하면 겐첸의 이론(지금 말한 바와 같이)은 Q+Con(PA)을 해석하고, 해석가능성은 타동적이기 때문에 PA는 겐첸의 이론을 해석할 수 없다.즉, PA가 겐첸의 이론을 해석했다면, PA도 해석할 것이고, 따라서 Pudlahk의 결과에 의해 일관성이 없을 것이다.그래서 일관성 강도의 의미에서 해석성이 특징인 것처럼 겐첸의 이론은 페아노 산술보다 강하다.

헤르만 바일은 1946년 괴델의 1931년 불완전성 결과가 수학의 일관성을 증명하려는 힐베르트의 계획에 파괴적인 영향을 미친 이후 겐첸의 일관성 결과가 갖는 의의에 대해 다음과 같은 언급을 했다.[4]

만약 힐버트가 그것을 성공적으로 수행할 수 있었다면, 궁극적으로 모든 수학자들은 힐버트의 접근을 받아들였을 것이다.첫 단계는 고무적이고 유망했다.그러나 그 후 괴델은 엄청난 타격을 입혔고, 아직 회복되지 않았다.괴델은 힐베르트의 형식주의에서 나타나는 기호, 공식, 공식의 순서 등을 일정한 방법으로 열거하고, 따라서 일관성의 주장을 산술 명제로 바꾸었다.그는 이 명제가 형식주의 안에서 증명되거나 반증될 수 없다는 것을 보여줄 수 있었다.이것은 단지 두 가지를 의미할 수 있다: 일관성의 증명서가 주어지는 추리는 시스템 내에서 공식적인 상대가 없는 어떤 주장을 포함해야 한다. 즉, 우리는 수학적 유도의 절차를 완전히 공식화하는 데 성공하지 못했다. 또는 완전히 "완성적인" 일관성의 증명에 대한 희망은 완전히 포기되어야 한다.G. 젠첸이 마침내 산술의 일관성을 증명하는 데 성공했을 때, 그는 칸토어의 "제2종 서수"에 침투하는 명백한 추리의 한 유형을 주장함으로써 실제로 그러한 한계를 통과했다.

클레네(2009년, 페이지 479년)는 1952년, 특히 힐베르트가 시작한 형식주의 프로그램의 맥락에서 겐첸의 결과의 의의에 대해 다음과 같은 논평을 했다.

정합성 입증에 의해 고전수학을 안전하게 만들자는 형식주의자들의 원래 제안은 ε까지의0 트랜스피나이트 유도 같은 방법이 사용되어야 한다는 것을 고려하지 않았다.그 문제제정이라는 의미에서 어느 정도까지 고전이론을 확보하는 것으로 받아들여질 수 있는가는 one까지의0 유도를 최종적인 방법으로 받아들일 준비가 되어 있느냐에 따라, 개인의 판단에 관한 현 상태에 있다.

기타 산술 일관성 증명

겐첸의 일관성 증명에 대한 첫 번째 버전은 폴 버네이즈가 그 증명에 암묵적으로 사용되는 방법에 반대했기 때문에 그의 일생 동안 발표되지 않았다.위에 기술된 수정된 증빙은 1936년에 연보에 실렸다.겐젠은 계속해서 1938년과 1943년에 각각 한 권씩, 두 권의 일관성 증명서를 더 출판했다.이 모든 것이 (젠젠&사보 1969)에 포함되어 있다.

쿠르트 괴델은 1938년 한 강연에서 겐첸의 1936년 교정본을 무카운트레렉스 해석으로 알려지게 된 것을 재해석했다.최초의 증거와 개혁은 모두 게임 이론적 용어로 이해할 수 있다. (Tait 2005).

1940년에 빌헬름 아커만은 순서형 ε을0 사용하면서 페아노 산수에 대한 또 다른 일관성 증거를 발표했다.

겐첸의 증명에 의해 시작된 작업

겐첸의 증거는 증명-이론적 서수 분석이라고 불리는 것의 첫 번째 예다.순서형 분석에서 잘 정렬된 것으로 증명될 수 있는 (건설적) 서수가 얼마나 큰지 또는 (건설적) 서수가 얼마나 큰지를 측정하여 이론의 강도를 측정한다.건설적 서수는 자연수의 재귀적 순서의 순서 유형이다.

이 언어에서 겐첸의 저작은 1차 페아노 산술의 증명-이론 서수가 ε임을0 확립한다.

로렌스 커비와 제프 파리는 1982년 굿스타인의 정리가 페아노 산술에서 증명될 수 없다는 것을 증명했다.그들의 증거는 겐첸의 정리에 근거한 것이었다.

메모들

  1. ^ 겐첸의 증거와 그 결과의 역사적이고 철학적인 의의에 대한 다양한 논평에 대한 자세한 설명은 클레네(2009, 페이지 476–499)를 참조하라.
  2. ^ Pudlak, Pavel (1985-06-01). "Cuts, Consistency Statements and Interpretations". Journal of Symbolic Logic. 50 (2): 423–441. doi:10.2307/2274231. ISSN 0022-4812. JSTOR 2274231.
  3. ^ Feferman, S. "Arithmetization of metamathematics in a general setting". Fundamenta Mathematicae. 49 (1). ISSN 0016-2736.
  4. ^ 웨일(2012, 페이지 144).

참조