겐첸의 일관성 증명
"오늘의AI위키"의 AI를 통해 더욱 풍부하고 폭넓은 지식 경험을 누리세요.
1. 개요
겐첸의 일관성 증명은 1936년 게르하르트 겐첸이 페아노 산술의 무모순성을 증명한 것이다. 이 증명은 원시 재귀 산술에 ε₀까지의 양화사 없는 초한 귀납법을 추가하여 이루어졌으며, 겐첸은 페아노 산술에서의 증명에 대한 "축약 절차"를 정의하여 증명의 무모순성을 보였다. 겐첸의 증명은 힐베르트 프로그램과 괴델의 불완전성 정리와 관련하여 논의되었으며, 이론의 강도를 비교하는 데 해석 가능성 개념이 사용되었다. 겐첸의 증명은 증명 이론적 서수 분석의 첫 번째 예시로, 페아노 산술의 증명론적 서수가 ε₀임을 확립했다. 겐첸의 증명은 굿스타인의 정리가 페아노 산술에서 증명될 수 없음을 증명하는 데 기초가 되었다.
더 읽어볼만한 페이지
- 메타논리학 - 동치
동치는 두 명제가 모든 경우에 동일한 진리값을 가져 논리적으로 같음을 의미하며, 논리학에서는 논리식 단순화 및 변환에 유용한 다양한 논리적 동치(항등, 지배, 멱등, 이중 부정, 교환, 결합, 분배, 드 모르간, 흡수, 부정 법칙 등)가 존재한다. - 메타논리학 - 괴델의 불완전성 정리
괴델의 불완전성 정리는 산술을 표현할 수 있는 무모순적 공리계는 그 안에서 증명하거나 반증할 수 없는 명제가 존재하며, 특히 체계 스스로의 무모순성을 증명할 수 없다는 수학적 논리 분야의 핵심 정리이다. - 증명 이론 - 힐베르트 프로그램
힐베르트 프로그램은 20세기 초 수학의 기초를 형식 체계로 구축하고 무모순성과 완전성을 증명하려 했으나, 괴델의 불완전성 정리에 의해 원래 목표 달성이 불가능해졌고 수정된 형태로 연구가 지속되고 있다. - 증명 이론 - 괴델의 불완전성 정리
괴델의 불완전성 정리는 산술을 표현할 수 있는 무모순적 공리계는 그 안에서 증명하거나 반증할 수 없는 명제가 존재하며, 특히 체계 스스로의 무모순성을 증명할 수 없다는 수학적 논리 분야의 핵심 정리이다.
| 겐첸의 일관성 증명 | |
|---|---|
| 겐첸의 일관성 증명 | |
| 개요 | |
| 분야 | 수학기초론 |
| 주제 | 수학적 귀납법 |
| 역사 | 1936년: 게르하르트 겐첸이 출판함. 페아노 산술의 일관성을 증명함. |
| 증명 | |
| 방법 | 초한 귀납법 |
| 관련 이론 | 모순 없는 공리계의 일관성을 증명하기 위해, 더 강력한 시스템이 필요함. |
2. 겐첸의 정리
겐첸의 정리는 자연수의 덧셈과 곱셈을 포함하여 페아노 공리에 의해 공리화된 일차 페아노 공리에 관한 것이다.[1] 이는 양화사가 자연수에만 적용되고 자연수의 집합이나 함수에는 적용되지 않는 "일차" 이론이다. 이 이론은 거듭제곱, 계승, 피보나치 수와 같이 재귀적으로 정의된 정수 함수를 설명할 수 있을 만큼 강력하다.
2. 1. 1차 페아노 산술
페아노 공리에 의해 공리화된 일차 페아노 공리는 자연수의 덧셈과 곱셈을 포함하는 이론이다. 이것은 "일차" 이론인데, 양화사는 자연수에 적용되지만, 자연수의 집합이나 함수에는 적용되지 않는다. 이 이론은 거듭제곱, 계승 또는 피보나치 수와 같이 재귀적으로 정의된 정수 함수를 설명할 만큼 강력하다.젠첸은 원시 재귀 산술의 기본 이론과 서수 ε0까지 양화사가 없는 초한 귀납법의 추가 원리에 의해 일차 페아노 공리의 무모순성이 증명될 수 있음을 보였다. 원시 재귀 산술은 논란의 여지가 거의 없는, 매우 단순화된 형태의 산술이다. 추가 원리는 비공식적으로 유한 근을 가진 트리 집합에 정렬 순서가 있음을 의미한다. 형식적으로, ε0는 인 첫 번째 서수 이다. 즉, 다음 수열의 극한이다.
:
이것은 큰 가산 서수보다 훨씬 작은 가산 서수이다. 산술 언어로 서수를 표현하려면 서수 표기법이 필요하며, 이는 ε0 미만의 서수에 자연수를 할당하는 방법이다. 이는 다양한 방식으로 수행할 수 있으며, 한 예는 칸토어 정규형 정리에서 제공된다. 젠첸의 증명은 다음과 같은 가정을 기반으로 한다. 양화사가 없는 공식 A(x)에 대해, A(a)가 거짓인 서수 ''a''< ε0가 있다면, 그러한 최소 서수가 존재한다.
젠첸은 페아노 산술에서의 증명에 대한 "축약 절차"라는 개념을 정의한다. 주어진 증명의 경우, 이러한 절차는 증명의 트리를 생성하며, 주어진 증명은 트리의 루트 역할을 하고, 다른 증명은 어떤 의미에서 주어진 증명보다 "더 간단"하다. 이러한 단순성 증가는 모든 증명에 ε0 미만의 서수를 첨부하고 트리를 아래로 이동할 때마다 이러한 서수가 단계마다 작아지는 것을 보여주는 방식으로 형식화된다. 그런 다음 그는 모순의 증명이 있다면 축약 절차는 양화사가 없는 공식에 해당하는 증명에 대한 원시 재귀 연산에 의해 생성된 ε0보다 작은 서수의 무한히 엄격하게 감소하는 수열을 초래할 것이라고 보여준다.[1]
2. 2. 증명 방법
겐첸은 원시 재귀 산술의 기본 이론에 서수 ε₀까지의 양화사 없는 초한 귀납법이라는 추가 원리를 더하여 일차 페아노 공리의 무모순성을 증명하였다.[1] ε₀는 ωα = α를 만족하는 첫 번째 서수 α이며, ω, ωω, ωωω, ... 수열의 극한이다.[1] 서수 표기법을 사용하면 ε₀ 이하의 서수에 자연수를 할당할 수 있는데, 이는 칸토어 정규형 정리 등을 통해 가능하다.[1]겐첸은 페아노 산술에서 증명에 대한 "축소 절차"라는 개념을 정의하였다. 주어진 증명에 대해 이 절차는 증명의 트리를 생성하는데, 여기서 주어진 증명은 트리의 뿌리가 되고, 다른 증명은 어떤 의미에서 주어진 증명보다 "간단"하다. 이러한 단순성은 모든 증명에 ε₀보다 작은 서수를 붙임으로써 형식화되고, 트리 아래로 내려갈수록 이 서수들은 한 단계씩 더 작아진다. 겐첸은 모순의 증명이 있다면, 감소 절차로 인해 양화사 없는 공식에 해당하는 증명에 대한 원시적 재귀 작용으로 생성된 ε₀보다 작은 서수의 무한 순감소 서수열이 발생한다는 것을 보여주었다.[1]
2. 3. 축약 절차
겐첸은 페아노 산술에서 증명에 대한 "축약 절차"라는 개념을 정의했다. 주어진 증명에 대해, 이 절차는 증명 트리(proof tree)를 생성하며, 주어진 증명은 트리의 루트(root)가 되고, 다른 증명들은 주어진 증명보다 "더 간단"해진다. 이러한 단순성은 모든 증명에 ε₀보다 작은 서수를 붙이고, 트리를 아래로 이동할 때마다 이 서수들이 작아지는 방식으로 형식화된다. 모순의 증명이 있다면, 축약 절차는 ε₀보다 작은 서수의 무한히 감소하는 수열을 초래한다.[1]3. 힐베르트 프로그램, 괴델의 정리와의 관계
괴델의 두 번째 불완전성 정리는 어떤 이론의 무모순성이 더 강한 이론에서만 증명될 수 있다는 주장을 뒷받침한다. 겐첸의 정리는 이 정리의 중요한 측면을 강조한다.[1]
겐첸의 이론은 원시 재귀 산술에 양화사 없는 초한 귀납법을 추가하여 얻어지며, 일차 페아노 산술(PA)의 무모순성을 증명한다. 그러나 겐첸의 이론은 PA를 포함하지 않으며, PA 역시 겐첸의 이론을 포함하지 않는다. 예를 들어, 겐첸의 이론은 모든 명제에 대한 일반적인 수학적 귀납법을 증명하지 않지만, PA는 귀납법의 모든 사례가 공리이기 때문에 이를 증명한다. 겐첸의 이론은 PA가 할 수 없는 수론적 사실, 즉 PA의 무모순성을 증명할 수 있기 때문에 PA에 포함되지 않는다. 따라서 두 이론은 어떤 의미에서 비교 불가능하다.
3. 1. 이론의 강도 비교
어떤 이론의 무모순성은 더 강한 이론에서만 증명될 수 있다는 주장이 제기되기도 한다. 겐첸의 이론은 1차 페아노 산술(PA)의 무모순성을 증명하지만, PA를 포함하지 않으며, PA도 겐첸의 이론을 포함하지 않아 두 이론은 어떤 의미에서 비교 불가능하다.[1]이론의 강도를 비교하는 더 강력한 방법으로 해석 가능성 개념이 사용된다. 파벨 푸들라크(Pavel Pudlák)는 제2 불완전성 정리의 강력한 형태를 증명하여, 로빈슨 산술 Q를 포함하는 무모순적인 이론 T는 Q + Con(T)를 해석할 수 없음을 보였다. 겐첸의 이론은 PA를 해석하지만, PA는 겐첸의 이론을 해석할 수 없으므로, 겐첸의 이론은 페아노 산술보다 더 강력하다.[2]
3. 2. 힐베르트 프로그램에 대한 영향
헤르만 바일은 괴델의 불완전성 정리 이후 겐첸의 무모순성 결과가 갖는 의의에 대해 언급하며, 겐첸이 칸토어의 "제2종 서수"에 침투하는 추론 유형을 주장함으로써 한계를 극복했다고 평가했다.[2] 스티븐 콜 클리니는 겐첸의 결과가 형식주의 프로그램에 미친 영향에 대해 논평하며, ε₀까지의 초한 귀납법을 유한적인 방법으로 받아들일 수 있는지에 대한 개인의 판단 문제를 제기했다.[1] 파울 베르나이스는 힐베르트의 유한적인 방법에 대한 제한이 너무 제한적일 수 있음을 지적하며, 증명 이론의 방법 확장을 제안했다.4. 겐첸의 증명에 의해 시작된 작업
겐첸의 증명은 증명 이론적 서수 분석의 첫 번째 예시이다. 서수 분석에서 이론의 강도는 (구성적) 서수가 얼마나 큰지, 즉 잘 정렬됨을 증명할 수 있는지, 또는 동등하게, 얼마나 큰 (구성적) 서수에 대해 초한 귀납법을 증명할 수 있는지 측정하여 측정한다. 구성적 서수는 자연수의 재귀적 잘 정렬의 순서 유형이다.[1]
4. 1. 서수 분석
서수 분석은 이론의 강도를 측정하기 위해 잘 정렬된 것으로 증명될 수 있는 (구성적) 서수가 얼마나 큰지를 측정하는 방법이다. 겐첸은 1차 페아노 산술의 증명-이론 서수가 ε₀임을 확립했다.[1]겐첸의 연구는 1차 페아노 산술의 증명론적 서수가 ε₀임을 보였다.
로렌스 커비와 제프 파리스는 1982년에 굿스타인의 정리가 페아노 산술에서 증명될 수 없다는 것을 증명했는데, 그들의 증명은 겐첸의 정리에 기초했다.
4. 2. 굿스타인 정리
로렌스 커비와 제프 파리스는 1982년에 굿스타인 정리가 페아노 산술에서 증명될 수 없다는 것을 증명했다. 그들의 증명은 겐첸의 정리에 기초했다.[1]5. 산술의 다른 무모순성 증명
쿠르트 괴델은 1938년 강연에서 겐첸의 1936년 증명을 재해석했는데, 이는 무반례 해석으로 알려지게 되었다.[1] 1940년 빌헬름 아커만은 순서수 ε₀을 사용하여 페아노 산술에 대한 또 다른 일관성 증명을 발표했다. 1959년 I. N. 클로도프스키는 산술의 일관성에 대한 또 다른 증명을 발표했다.
6. 한국 수학계에 미친 영향
겐첸의 정리는 한국 수리논리학 및 수리철학 분야의 발전에 중요한 자극을 주었다.
참조
[1]
서적
2009
[2]
서적
2012
본 사이트는 AI가 위키백과와 뉴스 기사,정부 간행물,학술 논문등을 바탕으로 정보를 가공하여 제공하는 백과사전형 서비스입니다.
모든 문서는 AI에 의해 자동 생성되며, CC BY-SA 4.0 라이선스에 따라 이용할 수 있습니다.
하지만, 위키백과나 뉴스 기사 자체에 오류, 부정확한 정보, 또는 가짜 뉴스가 포함될 수 있으며, AI는 이러한 내용을 완벽하게 걸러내지 못할 수 있습니다.
따라서 제공되는 정보에 일부 오류나 편향이 있을 수 있으므로, 중요한 정보는 반드시 다른 출처를 통해 교차 검증하시기 바랍니다.
문의하기 : help@durumis.com