ProofTheory 1407

Proof Theory✔

20세기 초에 수학에서 안전하지 않다고 여겨지는 개념들을 안전하게 만드는 노력들이 있었다. 대표적으로 무한소와 무한대라는 개념을 안전하게 만드는 작업들이 진행되었다. 칸토어는 집합론을 만들어서 무한대에 대한 수학적 이론을 만들었다. 그러나 칸토어의 집합론에는 모순이 있었다. 또한 선택공리는 임의의 정렬집합에 대하여 모순을 낳을 가능성이 있다고 여겨졌다.

그러나 수학계는 쉽게 칸토어의 공로를 무시할 수 없었다. Weyl 은 집합론에서 나타난 문제가 해석학과 관련된 수학의 매우 핵심적인 문제임을 "근본적인 위기" 라는 용어를 사용하면서 동시대 사람들을 설득했다. 그는 제한되지 않은 집합 구성법을 사용하지 않는 수학을 개발하여 제시했다.

Brouwer 는 수학의 논리적 기반을 의심했다. 논리학은 배중률을 공리로 삼는데, 이 배중률 때문에 명시적으로 구성되지 않은 대상의 존재성을 증명할 수 있었기 때문이다. 그는 배중률을 배척하고 직관주의적인 원리를 기초로 수학을 개발하여 제시했다. 이것이 직관주의 논리로 알려져있다.

Weyl 과 Brouwer 의 접근법은 수학을 엄격하게 제한하는 접근이었다. 그러나 힐베르트는 기존의 수학을 제한하는 이러한 접근법을 거부했다. 그에 따르면 수학은 과학이고, 모든 과학의 모델이며, 수학에서 정의된 안전한 추론규칙을 기반으로 진리를 증명할 수 있고, 그러므로 현실에서도 타당했다. 그는 수학의 이러한 위상이 위협받고 있다고 여기고 이 수학의 권위를 지키려 했다. 또한, 그는 칸토어의 집합론을 지키려 했다. 그에 따르면 칸토어의 초한귀납법은 인류가 생각해낼 수 있는 가장 뛰어난 성과였고 성취였다. 그가 제시한 수학을 힐베르트 프로그램이라고 하는데, 이는 다음과 같은 특징을 지닌다.

1. 수학 전체의 공리화.
2. 공리화된 수학 안에서 무모순성을 증명하기.

힐베르트는 증명 이론(proof theory)안에서 무모순성 증명이 수행되어야 한다고 주장했다. 그에 따르면 증명 이론은 오직 유한한(finitistic) 방법만을 사용해야 했다. 하지만 유한한 방법의 정의는 조금 모호했고, 아마도 유한한 영역 위에서의 조합적 추론(combinatorial reasoning)을 뜻하는 것으로 생각된다. 아커만, 폰 노이만, 버네이즈 같은 그의 학생들은 곧바로 성과를 내기 시작했다. 그들은 먼저 기초 산술의 부분체계를 공략했고, 곧이어 완전 귀납꼴을 포함하지 않는 부분 체계에 대한 유한한 방법을 사용하는 무모순성 증명을 얻어내었다. 그러나 완전귀납법을 포함하는 체계의 무모순성을 증명하기는 힘들었다. 이 실패는 그들이 부족해서가 아니라 괴델의 불완전성 정리에 의하여 근본적으로 불가능한 시도였음이 밝혀졌다. 귀납 공리를 허용하면 불완전성이 발생하여 체계 내에서의 무모순성 증명이 존재할 수 없게 되고, 이에 따라 유한한 방법으로 무모순성 증명을 수행할 수 없게 된다.

괴델의 정리가 힐베르트 프로그램을 끝내는 것 같았다. 괴델의 첫번째 불완전성 정리로 힐베르트 프로그램의 1단계가 불가능한 것으로 여겨졌다. 그러나 이 문제는 가능한 모든 수학을 형식화 할 필요가 없고 현재 존재하는 수학만 공리화하는 것으로 충분하다는 사실로 해결되었다. 실제로 오늘날은 연속체 가설 같은 것을 제외하고 거의 모든 수학이 선택공리를 가정한 ZFC 라는 단일 형식 체계 안으로 형식화된다.

그러나 괴델의 두번째 불완전성 정리가 힐베르트 프로그램에 치명상을 입혔다. 유한한 방법론에 의한 무모순성 증명은 반드시 수학 안으로 형식화될 수 있었기에 기초 산술에 완전귀납꼴을 포함시켜서 온전한 산술 체계를 만들면 두번째 불완전성 정리에 의하여 그 안에서 유한한 무모순성 증명이 존재할 수 없다. 하지만 힐베르트 학파원들은 유한한 무모순성 증명을 의심하게 되었으면서도 괴델의 결과가 힐베르트 프로그램의 불가능을 의미하게 된 것이라고 선뜻 받아들이지 못했다. 이 현상은 힐베르트의 권위와 힐베르트 프로그램의 모호함 때문이었다. 힐베르트는 유한한 방법에 대한 엄밀하고 정확한 정의를 내려주지 않았다. 따라서 수학자들은 유한한 방법들이 수학 안으로 형식화될 수 없은 어떠한 형태로든 이루어져있을 것이라고 생각하게 되었다.

수학자들은 무모순성 정리를 찾기 위하여 계속 노력했고 결국 겐첸이 기초 산술의 무모순성을 증명하는데에 성공했다. 괴델의 두번째 정리에 의하여 겐첸의 증명은 비유한한 방법론을 사용해야 했다. 겐첸은 모든 비유한한 방법을 한 점으로 집중시키는데에 성공했다. 이것은 초한 순서형의 정렬순서를 따르는 귀납이었다. 따라서 이 초한 귀납을 제외한 모든 증명의 부분이 유한한 방법을 사용했다. 이 결과는 힐베르트 학파의 유한한 방법론에 대한 입장을 조금 바꾸게 만들었다.

겐첸의 증명은 논리에서 가장 중요하고 가장 깊은 결과이다. 사실 수론의 무모순성 증명은 매우 쉽다. 왜냐하면 그것의 모델이 존재한다는 것만 보이면 되기 때문이다. 그렇다면 겐첸의 증명의 이점은 무엇인가? 모델을 구성하는 것 자체가 집합론 같은 어떤 체계를 필요로 한다. 그러므로 모델 구성에 의한 무모순성 증명은 집합론의 무모순성이 수론의 무모순성을 수반한다는 것을 증명하는 것이다. 그러나 겐첸의 증명은 더 많은 정보를 준다. 겐첸의 증명은 초한 서수형의 정렬에 대한 귀납법을 사용하는 것 외에는 유한하다는 것을 앞서 언급했다. 이것은 다음을 의미한다.

1. 겐첸의 증명의 귀납법은 매우 제한된 복잡성의 식만을 필요로 한다. 그의 무모순성 증명은 배중률까지도 필요로 하지 않는다. 따라서 매우 낮은 복잡도의 식으로 제한된 귀납꼴에 대한 초한 서수형의 정렬에 대한 귀납꼴을 갖는 직관주의를 기반으로 하는 체계 \(T\) 에서도 형식화될 수 있다. 따라서 산술의 무모순성이 체계 \(T\) 안에서 결정된다. 괴델의 두번째 정리에 의하여 체계 \(T\) 의 증명 이론적 강도는 수론의 그것을 초과해야 한다. 그러나 \(T\) 의 귀납법을 제한하여 얻은 부분체계 \(T_0\) 는 오직 수론의 무모순성과 자신의 무모순성의 동치만을 증명할 수 있다. 따라서 겐첸의 증명은 수론의 무모순성을 개념적으로 수론보다 안전하게 여겨지는 \(T_0\) 의 무모순성으로 환원시킬 수 있었다. 이것이 환원적 증명 이론(reductive proof theory)의 예시이다. 환원적 증명 이론에서 이론 \(T_1\) 의 무모순성을 더 다루기 쉬운, 같은 증명 이론적 강도를 갖는 \(T_2\) 의 무모순성으로 환원시킬 수 있다.
2. 정렬에 대한 귀납법이 겐첸의 증명에서 유일한 비유한한 방법이다. 여기에서 착안하여 형식 이론 \(T\) 의 증명 이론적 서수를 정의할 수 있다. 서수 \(\alpha\) 가 \(T\) 에서 증명가능하다는 것은 정렬순서가 \(T\) 에서 증명가능하다는 조건을 만족하는 순서형 \(\alpha\) 를 갖는 원시 재귀적으로 정의가능한 정렬순서 \(\prec\) 가 존재한다는 것이다. \(T\) 의 증명 이론적 서수는 \(T\) 의 증명가능한 서수가 아니다. 그러므로 \(T\) 에서 증명 불가능한 가장 작은 서수를 찾으면, \(T\) 의 증명 이론적 서수를 정의할 수 있고 증명 이론적 강도를 측정할 수 있게 되는 것이다. 이 결과가 서수 분석(ordinal analysis)의 발전으로 이어졌다. 오늘날에는 이론 \(T\) 의 증명 이론적 서수를 \(T\) 의 공리로 정초성(well-foundedness)을 연역해낼 수 있는 자연수에 대한 원시 재귀 정렬순서의 순서형의 최소상계로 정의한다.

겐첸은 \(\epsilon_0\) 이 \(\mathsf{PA}\)(페아노 산술)의 공리로 증명 불가능한 최소 서수라는 것을 보였다. 반면 임의의 \(\alpha < \epsilon_0\) 에 대한 정렬순서는 산술 \(\mathsf{PA}\) 의 공리로 증명 될 수 있다. 이 결과 자체가 \(\mathsf{PA}\) 의 무모순성을 증명한다. 왜냐하면 만약 수론이 모순적이라면 모든 것이 증명가능하기 때문이다. 그러므로 괴델의 두번째 불완전성 정리 때문에 수론의 무모순성 증명은 적어도 \(\epsilon_0\) 이상의 증명이어야만 한다. 무모순성 증명이 \(\epsilon_0\) 보다 작은 증명이면 수론 안에서 증명되어버리기 때문이다.

겐첸의 결과는 ordinal analysis 이라는 새로운 분야를 시작시켰다. 서수 분석(ordinal analysis)은 주어진 이론 \(T\) 에 대하여 \(T\) 의 무모순성을 증명하기에 충분한 최소 서수 \(\alpha\) 를 찾는 것이 목표이다. 다음의 표에 각 이론의 무모순성을 증명할 수 있는 최소 서수가 나와있다. 1차 논리의 수론, 즉, \(\mathsf{PA}\) 의 무모순성을 증명할 수 있는 최초 서수는 \(\epsilon_0\) 라는 것을 확인하자.

이제부터 서수 분석의 기초적인 내용을 알아보자. 여기에서 중점을 두고 이해해야 하는 부분은 체계 내에서 증명불가능한 사실이 어떻게 다른 체계의 힘을 빌려서 증명되는지 이다. 또한, 수학자들이 표현하는 유한과 무한이 아닌 실질적인 유한과 실질적인 무한의 개념을 이해하는 것이다. 만약 \(\mathsf{PA}\) 의 무모순성 증명이 실질적인 무한을 요구한다면, 그 증명과 그 증명을 담고 있는 이 웹페이지 자체가 무한한 용량을 필요로 할 것이다. 수학자들이 유한이라거나 무한이라고 표현하는 것은 실질적 유한과 실질적 무한이 아니다. \(\mathsf{PA}\) 의 증명을 위하여 실질적으로 무한한 과정이 필요하면, 그것의 증명에 대한 생각은 영원히 끝나지 않았을 것이다. 그러나 명백히 \(\mathsf{PA}\) 의 유일한 비유한한 증명의 부분, 즉, 초한귀납에 관한 생각은 끝이 났고, 그것을 이해하는데에 무한한 시간이 소요되지 않는다.

명백히 뇌는 무한의 영역에 존재하는 신적인 존재가 아니라고 보여진다. 뇌는 유한한 절차에 의하여 생각한다. 그럼에도 불구하고 무한에 관한 생각을 유한한 절차로 해내었다. 그러므로 중요한 것은 어떤 대상이 수학적으로 무한일 수도 있어도 그것을 어떻게 유한한 생각 체계 안에서 처리했는지 파악하는 것이다. 이로써 지능의 강도와 한계를 밝힐 수 있을까? 그러하다면 체계 내에서 증명 불가능한 사실들을 증명할 방법에 대한 단서를 얻을 수 있다. 이는 도달가능성이 결정불가능한 컴퓨팅 지점으로 도달할 수 있는 방법을 마련할 힌트를 줄 수 있고, 지능을 재귀적으로 발전시킬 수 있는 실마리도 될 수 있다. 전자는 해킹에 관한 인공지능을 만들 수 있는 힌트를 주고 후자에 대해서는 자기 자신에 대한 생각과 그것의 기계화가 생각의 끝이 될 수 있다고 말할 수 있다. 튜링은 자기 자신의 설정표를 수정해나가며 발전하는 기계가 지능과 같은 역할을 할 것이라고 말했다.

그러나 튜링의 증명의 정지문제와 수리논리학의 계산가능성의 정지문제에 관한 정리 5.13과 정리 5.14에서 알 수 있듯이 기계가 자기 자신을 입력받으면 모순이 일어난다. 체계는 불완전성 정리에 의하여 체계 내에 갇혀있다. 기계도 결정불가능성에 의하여 기계 안에 갇혀 있다. 탈출 방법은 수학적으로 없다는 것이 증명되었다. 힐베르트 프로그램은 이미 100년전에 폐기되었다. 이 울타리를 어떻게 바라보아야 할지, 이 안에서 그래도 뭘 할 수 있을지

Ordinal Analysis of Number Theory✔

수학자의 목표는 어떤 구조의 이론 속에서 어떤 수학적 사실이 구조에서 성립한다는 것을 밝히는 것이다. 이를 위해서는 구조를 기술할 언어가 필요하다. 언어로 표현된 문장이 구조에서 참임을 보이기 위해서는 증명이 필요하다. 그러나 문장을 증명할 유일한 방법은 문장이 구조 속에서 이미 참이라고 알려진 문장의 귀결임을 보이는 것뿐이다. 이 절차를 역추적하면 우리는 구조 속에서 증명 없이 참이라고 받아들이기로 한 문장들인 공리(axiom)에 도달하게 된다. 문장의 증명이란 공리에 추론 규칙을 적용하여 문장을 도출하는 것이다. 공리와 추론규칙의 채택은 임의적이지 않다. 공리는 반드시 의심할 여지가 없이 참이여야 하고 추론규칙 또한 참인 결론을 내린다는 것이 명백해야 한다. 그러나 수학자는 자기 자신만 증명된 문장인 정리가 참이라는 것을 확신할 뿐만 아니라 그의 동료들도 확신하기를 원한다. 그러므로 주어진 문장이 공리인지 아닌지, 추론규칙이 올바르게 적용되었는지 아닌지 결정가능해야 한다. 그러므로 구조의 이론을 공리화하기 위해서는 다음이 필요하다.

• 구조의 언어의 형식화. (구조의 형식 언어는 주어진 기호열이 잘 형성된 식인지 결정가능해야 한다.)
• 구조의 공리가 될 의심할여지가 없이 참인 결정가능한 문장들.
• 결정가능한 추론 규칙(증명 절차).

결정가능한 공리와 증명 절차를 지닌 결정가능한 형식 언어를 형식 체계 또는 구조에 대한 형식 이론이라고 한다. 한 형식 체계에서 증명가능한 문장 집합은 재귀적으로 열거가능(r.e.)한 집합이다.

1차 논리 언어에는 완전한 증명절차가 존재한다. 그러나 이는 수학적 공리를 지닌 모든 증명 절차가 1차 논리의 모든 참인 문장을 생성해낸다는 것은 아니다. 일반적으로 구조의 참인 문장 집합은 재귀적으로 열거가능하지 않을 정도로 복잡도가 높다. 그렇다면 이제 우리가 해야 할 일은 형식 체계가 어디까지 불완전하고 어디까지 완전한지, 즉, 형식 체계의 한계에 대하여 판정하는 것이다. 이제부터 형식 체계의 능력을 \(\Pi_{1}^{1}\)-문장의 증명가능성을 빗대어 판정해볼 것이다.

\(\Pi_{1}^{1}\) 문장이라거나 \(\Sigma_{1}^{0}\) 식이라는 것은 산술 계층이 확장된 해석 계층으로 분류되는 식들을 뜻한다.

Language \(\mathscr{L}\) of number theory✔

수리논리학에서 1차 논리의 일반적인 언어를 정의하면서 시작한 것과 달리 애시당초 산술의 언어 \(\mathscr{L}\) 로 시작한다. 산술의 언어는 1차 논리 수론에서 정의했었다. 여기에서는 증명 이론의 언어로 산술의 언어를 재정의하며 시작한다.

구조(해석)는 상수, 함수, 관계의 모임으로 구성된 비어있지 않은 집합으로 주어진다. 자연수 구조 \(\N\) 에 대한 형식 언어를 얻기 위하여 구조를 정의해야 한다. 자연수 집합은 \(0\) 과 다음수에 의하여 특정되고 모든 자연수는 유일하게 결정되는 자연수로 판정된다. \(0\) 에 상수 \(\underline{0}\) 를 부여하고 다음수 함수에 기호 \(\underline{S}\) 를 부여하며 모든 자연수 상수에 \(\underline{0}\) 에 대한 다음수 함수를 적용한 결과를 부여할 수 있다. 그러므로 최소한 \(0\) 과 다음수 함수에 대한 상수가 언어에 필요하다는 것을 알 수 있다.

이제 자연수 위에서 다음수 함수 말고 또 다른 어떤 함수와 관계가 고려되어야 할까? 물론 자연수 집합 위에서 정의 가능한 모든 함수와 관계를 정의하자는 대답을 생각할 수 있다. 함수와 관계는 비가산적으로 많기 때문에 그렇게 하면 비가산적으로 많은 기본 기호를 지닌 언어가 만들어질 것이다. 형식 체계에서는 오직 정의된 공리를 갖는 상수만이 형식 체계의 능력에 기여한다. 모든 결정가능한 집합은 가산이므로 형식 체계의 범위를 벗어나는 비가산 공리 집합이 필요하다. 함수와 관계 상수에도 정의된 공리를 분배하면 그것들을 변수로 다루는 것이고, 이는 언어가 2차 논리 변수를 갖게 되는 것이다. 그러나 지금은 집합 변수를 도입하는 것으로 충분하다. 집합 변수나 함수 변수의 도입은 형식 체계의 능력을 올리지 못한다.(문제 3.15.4) 그러나 집합 변수에 정의된 공리를 추가하면 증명 이론적 분석이 불가능할 정도로 강력한 체계가 탄생한다. 그러므로 체계를 제한하는 일이 필요하다.

수론에서 가장 중요한 함수는 \(+\) 와 \(\cdot\) 이다. 이 함수는 원시 재귀 함수이고, 이 함수로부터 모든 원시 재귀 함수를 얻을 수 있다. 그러므로 모든 원시 재귀 함수와 관계에 대한 상수를 갖는 겉으로 보기에 강력한 체계를 정의할 것이다. 이를 위해 다음과 같이 모든 원시 재귀 함수에 이름을 부여하고, 의미를 부여한다.

• 수리논리학에서 정의했던 치환과 원시 재귀

• 이로써 모든 원시 재귀 함수와 관계에 항에 의하여 이름을 붙일 수 있다.

• 밑줄은 혼동이 없을 때 생략한다.

• \(A[\dots ]\) 표기가 \(A\) 에서 나타난 자유변수를 표시하기 위하여 사용되지만, \(A\) 의 자유변수에 할당되는 값을 표기하는 용도로도 사용된다. \([]\) 표기가 두 가지 의미로 사용되니 주의해야 한다.

Semantics for \(\mathscr{L}\)✔

지금까지 \(\mathscr{L}\) 의 항과 식을 순전히 문법적으로 정의했는데, 이는 아무런 의미도 없는 순수한 기호 덩어리, 데이터 조각들에 불과하다. 여기에 의미를 부여하기 위하여 형식 언어 \(\mathscr{L}\) 의 해석이 필요하다. 그러나 의미론의 일반적인 이론을 세우지는 않고 \(\mathscr{L}\) 의 표준 해석(표준 모델)인 자연수 구조 \(\N\) 만을 살펴볼 것이다. 의미론의 일반적인 이론은 1차 논리에서 이미 살펴보았다.

• 즉, 할당은 자유 변수에 할당할 자연수의 모든 경우의 수 중 어떤 한 가지 경우이다.

• 상수는 자유변수가 아니므로 할당과 독립적이다. 오직 자유변수만 할당에 의하여 구체화된다.

• 이처럼 의미론은 근본적으로 집합론에 의존하여 술어의 참과 거짓을 결정한다. 모든 의미론은 1) 에서 정의한 술어의 타당성을 결정하는 집합론의 포함관계 \({\dots} \in {\dots}\) 가 참인지, 거짓인지에 따라 결정된다.

• \(\restriction\) 은 함수의 제한 기호이다.

• \([]\) 라는 표기가 두 가지 의미로 사용된다. 위와 같은 표기는 자유변수를 할당하는 의미로 \(A[\dots ]\) 표기가 사용되었지만, \(A[\dots ]\) 표기가 \(A\) 에 나타난 자유변수의 의미로 사용되는 경우도 있으니 주의해야 한다.

Formal System \(\mathsf{Z}_1\) for Number Theory✔

이렇게 자연수 구조 \(\N\) 의 의미론을 알아보았다. 이제 형식적 추론 작업으로 모든 진리를 도출해낼 수 있다는 힐베르트 프로그램의 철학(물론 불완전성 정리로 반박되었지만)을 따라 자연수 구조 \(\N\) 에서 타당한 문장을 최대한 많이 도출해낼 수 있는 형식체계 \(\mathsf{Z}_1\) 을 세우려 한다. 이 \(\mathsf{Z}_1\) 은 산술 체계 \(\mathsf{PA}\) 와 동형이다.

먼저 논리적 구조에 의하여 타당하게 되는 문장들을 다뤄야 한다. \(\mathscr{L}\) 의 모든 식은 문장과 양화사 구조를 갖는다. 논리적 연결사 \(\lnot ,\land ,\lor\) 이 주어진 \(\mathscr{L}\)-식의 문장 구조를 명확하게 하기 위하여 \(\mathscr{L}\)-식의 부분식을 정의하자.

• \(A ^{\Bbb{B}}\) 의 계산에 필요한 것은 오직 \(\Bbb{B} \restriction \operatorname{AE}(A)\) 의 값이다.

• 증명

  (\(A \in \operatorname{AT}(F)\) 의 정의에 대한 귀납법으로 쉽게 증명할 수 있다.)

• 증명

  식 \(A\) 의 길이에 대한 귀납법으로 쉽게 증명된다.

  \(A \in \operatorname{AE}\) 이면 정의에 의하여 \(\N \vDash A ^{\Phi } \iff A ^{\Bbb{B}_\Phi }=t\) 이다.

  (\(A\) 가 식 \(\lnot B\), \(B \lor C\), \(B \land C\) 인 경우도 쉽게 증명된다.)

  ■

• 증명

  (3.4 의 따름정리이다.)

• \(A_x(t) \to \exists xA\) 와 \(\forall xA \to A_x(t)\) 를 뜻한다.

• 증명

  \(\N \vDash A_x(t) ^{\Phi }\) 를 가정하자. \(A\) 의 길이에 대한 귀납법으로 쉽게 \(\N \vDash A_x(t) ^{\Phi } \iff \N \vDash A_x(\underline{t}^{\Phi })^{\Phi }\) 를 얻을 수 있다. 그러므로 \(\N \vDash \exists x A ^{\Phi }\) 이다. ▲

  이제 \(\N \vDash \forall xA ^{\Phi }\) 가 \(\N \vDash A_x(t) ^{\Phi }\) 를 함의한다는 것을 보이려 한다. \(\N \vDash \forall xA ^{\Phi }\) 는 \(\N \vDash A_x(\underline{t}^{\Phi })^{\Phi }\) 를 함의하므로 \(\N \vDash A_x(t)^{\Phi }\) 이다. ■

• 사실, 완전히 엄밀하게 하기 위해서는, 위의 증명에서 \(t\) 가 \(x\) 에 대하여 치환가능하다는 가정이 필요하다. 즉, \(t\) 의 자유변수들이 \(A\) 에서 종속되면 안된다. 그러나 이 치환가능성에 대한 조건을 편의상 이 증명에서도 그렇고 앞으로도 암묵적으로 가정하자.

Axiom, Inference✔

이제 수론의 형식 체계 \(\mathsf{Z}_1\) 의 공리와 추론규칙을 형식화할 준비를 하려 한다. \(\mathsf{Z}_1\) 의 언어는 1차 논리 언어 \(\mathscr{L}_1\) 이다.

• 2) 는 \(\forall xA \to A_x(t)\) 와 \(A_x(t) \to \exists xA\) 를 뜻한다.

• 다음과 같이 이해하면 된다.

  1. \((\text{mp})\quad\) \(A, \lnot A \lor B \vdash B \quad\) (modus ponens)
  2. \((\forall)\quad\) \(\lnot A \lor B \vdash \lnot A \lor \forall xB \quad\)
  3. \((\exists)\quad\) \(\lnot B \lor A \vdash \lnot \exists x B \lor A \quad\)

• 추론은 타당성을 보존해야 하고, 이것을 보장해주는 속성이 체계의 건전성이다.

• 그러나 1) 와 2) 의 증명에 필요한 재귀 함수의 이론을 다루지는 않을 것이다. 재귀 함수 이론은 수리논리학에서 자세히 다루었고, 그 결론으로써 수론이 무모순일 때 재귀 함수 모임이 수론에서 표현가능한 함수의 모임과 동일하다는 결론(형식적 수론 따름정리 3.30)을 얻었다.

Soundness✔

• \(\mathsf{Z}_1\) 을 완전히 형식적으로 정의했으므로 그것의 공리와 추론규칙들은 의미론적으로 아무런 의미가 없는 순수한 기호 덩어리, 더미 데이터에 불과하다. 우리가 \(\mathsf{Z}_1\) 을 세운 이유는 힐베르트의 철학을 따라 자연수 구조 \(\N\) 의 진리를 형식적으로(기계적으로) 최대한 많이 도출하는 공리적 추론 절차를 세우기 위함이었다. 그러므로 \(\mathsf{Z}_1\) 이 아무리 무의미한 기호 덩어리의 형식 체계에 불과하다고 해도, 먼저 그것의 공리가 자연수 구조 \(\N\) 에서 타당해야 하고, 그것의 추론규칙이 공리의 타당성을 보존해야 한다는 것이 보장되어야 한다. 그렇지 않고 체계의 추론 규칙이 타당성을 보존할 능력이 없고, 하물며 공리부터 거짓이라면, 이 체계는 무의미한 쓰레기 기호 덩어리에 불과할 것이다.

  건전성 정리는 이 형식 체계가 타당한 진리만을 도출해낸다는 것을 보장해준다.¹

• 증명

  \(\mathsf{Z}_1 \vdash F\) 의 정의에 대한 귀납으로 \(\mathsf{Z}_1 \vdash F\) 이 임의의 할당 \(\Phi\) 에 대하여 \(\N \vDash F ^{\Phi }\) 를 함의한다는 것을 보이자.

  \(F\) 가 논리적 공리이면, 정리 3.5 와 보조정리 3.6 에 의하여 \(\N \vDash F ^{\Phi }\) 이다. ▲

  동등성 공리나 수학적 공리에 대하여서는 자명하다. ▲

  다만, 수학적 공리 3) 귀납공리꼴에 대해서만 증명해보자. 그러니까 \(\N \vDash A(\underline{0})^{\Phi }\) 와 \(\N \vDash \forall y(A(y) \to A(\underline{S}y)) ^{\Phi }\) 가 모든 \(n \in \N\) 에 대하여 \(\N \vDash A(\underline{n})^{\Phi }\) 를 함의한다는 것을 보이자. 그런데 \(\N \vDash \forall y(A(y) \to A(\underline{S}y)) ^{\Phi }\) 와 \(\N \vDash A(\underline{n})^{\Phi }\) 는 \(\N \vDash A(\underline{Sn})^{\Phi }\) 를 함의한다. \(\N \vDash A(\underline{0})^{\Phi }\) 이고 모든 자연수에 대하여 \(0\) 으로부터 다음수 함수를 유한번 적용하는 메타귀납법으로 모든 \(n \in \N\) 에 대한 \(\N \vDash A(\underline{n})^{\Phi }\) 를 얻을 수 있기 때문이다. ▲

  이제 추론 규칙이 타당성을 보존한다는 것을 증명하면 끝난다.

  \(\N \vDash A ^{\Phi }\) 와 \(\N \vDash (A \to B) ^{\Phi }\) 로부터 곧바로 \(\N \vDash B ^{\Phi }\) 를 얻을 수 있다. ▲

  \(F\) 가 양화추론 \((\forall)\) 의 결론이라면 \(F\) 는 \(A \to \forall xB\) 이고, 귀납적 가정에 의하여 이것의 전제 \(A \to B\) 는 모든 할당 \(\Phi\) 에 대하여 \(\N \vDash (A \to B)^{\Phi }\) 이다. 이제 모든 \(n \in \N\) 에 대하여 \(\N \vDash A ^{\Phi }\) 가 \(\N \vDash B_x(\underline{n})^{\Phi }\) 를 함의한다는 것을 보여야 한다. 임의의 \(n \in \N\) 에 대하여 할당 \(\Psi\) 를 다음과 같이 정의하자.

  \[ \begin{cases} \Psi (x) = n & \\ \Psi (y) = \Phi (y) & y \neq x\\ \Psi (X) = \Phi (X) & \\ \end{cases}\]

  \(x \not\in \operatorname{FV}_{1}(A)\) 이므로 \(\N \vDash A ^{\Psi }\) 이고 \(\N \vDash (A \to B) ^{\Psi }\) 이므로 \(\N \vDash B ^{\Psi }\) 이다. 이는 \(\N \vDash B_x(\underline{\Psi x})^{\Phi }\) 를 함의한다. 그러므로 모든 \(n \in \N\) 에 대하여 \(\N \vDash B_x(\underline{n})^{\Phi }\) 이다. ▲

  \((\exists)\) 에 대하여서도 비슷하게 증명된다. ■

• 괴델의 불완전성 정리에 의하여 산술의 형식 체계 \(\mathsf{Z}_1\) 이 자연수 구조 \(\N\) 의 모든 진리를 형식적으로 도출해내지 못한다는 것이 밝혀졌을 때, 힐베르트의 철학은 무너졌다. 그러나 이 실패가 오히려 지금의 이야기의 출발점이다. 우리는 이제부터 산술 체계의 연역에 의한 증명의 한계를 명확하게 규명해낼 것이고, 괴델의 두번째 불완전성 정리에 의하여 산술이 자체적인 능력으로 증명할 수 없었던 산술의 무모순성을 증명할 수 있는 해답을 찾아낼 것이다. 우리는 이렇게 실패 속에서도 계속 길을 찾을 것이고, 오히려 실패로 진리에 더욱 가까워질 것이다.

  지금까지의 내용은 수리논리학에서 살펴본 1차 논리(완전성)와 1차 산술(불완전성)의 내용을 앞으로 다룰 증명이론의 언어로 다시 복습한 것 뿐이다.

  이제부터가 본론이다.

Infinitary Language \(\mathscr{L}_{\infty}\)✔

불완전성이 내재되어 있는 유한한 형식 체계 \(\mathsf{Z}_1\) 으로는 \(\N\) 의 모든 \(\Pi_{1}^{1}\)-정리를 얻을 수 없다. 하지만 \(\mathsf{Z}_1\) 같은 유한 형식 체계의 범위 바깥에 있는 식을 분류할 수 있어야 하고, 이로써 \(\mathsf{Z}_1\) 같은 형식 체계의 능력을 제대로 측정해야 한다.

이를 위하여 아예 \(\N\) 의 모든 \(\Pi_{1}^{1}\)-정리를 도출할 수 있는 무한 체계 \(\mathsf{Z}_{\infty}\) 를 만들어보자! \(\mathsf{Z}_1\) 이 산술의 언어 \(\mathscr{L}\) 위에 세워졌듯이, 무한 체계 \(\mathsf{Z}_{\infty}\) 를 만들기 위해서는 무한 언어 \(\mathscr{L}_{\infty}\) 가 필요하다. 표준적인 무한 연역 절차가 존재하는 무한 언어 \(\mathscr{L} _{\infty}\) 안에서 \(\N\) 의 \(\Pi_{1}^{1}\)-문장을 재형식화하자. 힐베르트와 Schutte가 증명 이론에서 무한 체계를 암묵적으로 사용했지만, 타이트(W. Tait)가 이 언어를 정립하여 타이트 언어라고도 한다.

• 기술적인 편의상 부정 기호 \(\lnot\) 을 기호로 채택하지 않는다. 그러나 아래의 정의 4.4 에서 \(\lnot\) 을 따로 정의한다.

• \(\bigvee_{}^{}\{A_i : i \in I\}\) 를 \(\bigvee_{i \in I}^{}A_i\) 라고 표기하고, \(\bigwedge_{}^{}\{A_i : i \in I\}\) 를 \(\bigwedge_{i \in I}^{}A_i\) 라고 표기할 수 있다.

  \(\bigvee_{}^{}\{A_1, \dots, A_n\}\) 를 \(A_1 \lor \dots \lor A_n\) 라고 표기하고, \(\bigwedge_{}^{}\{A_1, \dots, A_n\}\) 를 \(A_1 \land \dots \land A_n\) 라고 표기할 수 있다.

• 원시 재귀 여관계

• 증명

  \(\lnot A\) 의 정의에 대한 귀납법으로 쉽게 증명 가능하다. ■

Semantics for \(\mathscr{L}_{\infty}\)✔

무한 언어 \(\mathscr{L}_{\infty}\) 을 만들었으니 늘 그래왔듯이 먼저 의미론부터 세워야 한다. 무한 언어에서 정의된 식이 자연수 구조 \(\N\) 에서 참이라는 것을 다음과 같이 정의한다.

Validity Relation \(\svDash{}{\Omega}\) for Language \(\mathscr{L}_{\Omega}\)✔

이제는 언어 \(\mathscr{L} _{\Omega}\) 에 대한 타당성 관계에 대한 구문론적인 정의가 필요하다. 이를 위하여 \(\N\) 에서 타당한 \(\mathscr{L} _{\Omega}\)-식을 완전히 도출해낼 수 있는 무한 연역을 도입하자. 이로써 앞서 언급했듯이 유한 언어에서 정의된 유한 산술 체계가 지니는 불완전성을 해결한다.

• 이로써 \(\svDash{}{\Omega}\) 의 2가지 공리들이 타당하고, 2가지 추론 규칙들이 타당성을 보존한다는 것이 보장된다. 그러나 더 중요한 것은 완전성이다. 완전성으로 \(\N\) 에서 타당한 \(\mathscr{L}_{\Omega}\)-식을 완전히 특징지을 수 있다는 것이 보장되어야 하기 때문이다.

• 증명

  \(\svDash{}{\Omega} \Delta\) 의 정의에 대한 귀납법으로 증명가능하다.

  \(\operatorname{(Ax1)}\) 그러면 \(\Delta\) 가 \(\mathcal{X}_P(t _{1}^{\N },\dots , t _{n}^{\N }) = 1\) 를 만족하는 원자식 \((\underline{P}t_1 \dots t_n)\) 을 포함한다. 정의 5.1(1) 에 의하여 임의의 할당 \(\Phi\) 에 대하여 \(\N \vDash (\bigvee_{}^{}\{F:F \in \Delta\})^{\Phi }\) 이다. ▲

  \(\operatorname{(Ax2)}\) 임의의 할당 \(\Phi\) 와 \(s ^{\N } = t ^{\N }\) 인 항 \(s\) 와 \(t\) 에 대하여 자명하게 \(t ^{\N } \in \Phi (X)\) 또는 \(s ^{\N } \not\in \Phi (X)\) 이므로 정의 5.1(2) 에 의하여 \(\N \vDash (t \in X) ^{\Phi }\) 또는 \(\N \vDash (s \not\in X)^{\Phi }\) 이다. 그러므로 \(\N \vDash (\bigvee_{}^{}\Delta \lor (t \in X) \lor (s \not\in X))^{\Phi }\) 이다. ▲

  \((\land)\) 귀납적 가정에 의하여 모든 \(i \in I\) 에 대하여 \(\N \vDash (\bigor_{}^{} \Delta \lor A_i)^{\Phi }\) 이다. \(\N \vDash \bigor_{}^{}\Delta ^{\Phi }\) 이면 \(\N \vDash (\bigor_{}^{}\Delta \lor \bigand_{i \in I}^{}A_i)^{\Phi }\) 이다. \(\N \not \vDash \bigor_{}^{}\Delta ^{\Phi }\) 이면 모든 \(i \in I\) 에 대하여 \(\N \vDash A_i ^{\Phi }\) 이므로 \(\N \vDash \bigand_{i \in I}^{}A_i ^{\Phi }\) 이고, 결국 \(\N \vDash (\bigor_{}^{}\Delta \lor \bigand_{i \in I}^{}A_i)^{\Phi }\) 이다. ▲

  \((\lor)\) 의 경우는 \((\land)\) 의 경우와 비슷하다. ■

• 이로써 자연수 구조 \(\N\) 에서 타당한 \(\mathscr{L} _{\Omega}\) 식은 모두 \(\svDash{}{\Omega}\) 로 도출할 수 있다는 것이 보장된다. \(\mathsf{Z}_1 \vdash\) 는 불완전성이 내재되어 있어 \(\N\) 에서 타당한 모든 문장을 도출해내지 못했다. 이 단점을 보완하는데에 성공한 것이다.

• 집합 변수의 존재 때문에 본 정리의 증명은 쉽지 않다. 증명을 위한 준비가 더 필요하다.

Coding Machinery, Sequence Number✔

• \(t \in \operatorname{Seq}\) 는 어떤 자연수 \(\left< \right>(x_1, \dots, x_n) = \left< x_1, \dots, x_n \right> = t \in \N\) 이다.

• \(\operatorname{Seq}(x)\) 는 \(x \in \operatorname{Seq}\) 이다.

• 증명

• 두 시퀸스 수의 연결 \(\concat\) 은 \(*\) 로도 표기된다.

Tree✔

• 트리는 다음과 같이 루트 \(\left< \right>\) 로부터 자라나는 구조이다.

  

• 트리를 초기 절편에 대하여 닫혀있는 시퀸스 수 집합이라고 정의했다. 쉽게 말해, 다음이 성립한다는 것이다.

  • \(\left< x_0, \dots, x _{n-1} \right>\) 가 \(T\) 의 길이가 \(n\) 인 열이면 \(0 \leq m < n\) 에 대한 그것의 프리픽스(prefix) \(\left< x_0, \dots, x _{m-1} \right>\) 도 \(T\) 에 속한다.

• 예시

  다음 트리는 길이 \(2\) 의 모든 열(sequence)로 구성된다.

  

  \(\left< 1,2 \right>\) 는 다음과 같은 트리로 표현된다. \(T _{\left< 1 \right>} = \{\left< 2 \right>\}\) 는 \(\left< 1 \right>\) 위의 \(T\) 의 부분트리이다.

  

  다음 트리는 순감소하는 모든 열로 구성된다.

  

  위의 예시의 트리는 모두 wf 트리이다. 그러나 모든 시퀸스 수 집합 \(\operatorname{Seq}\) 는 명백히 모든 무한 시퀸스를 포함하므로 wf 트리가 아니다.

• 선 귀납은 쉽게 말해 노드 \(s\) 의 모든 하위 노드에 대하여 \(F\) 가 성립할 때 반드시 \(s\) 에서도 \(F\) 가 성립한다면, \(T\) 의 모든 노드에서 \(F\) 가 성립한다는 것이다.

• 선 재귀로 정의된 함수가 어떻게 구성되었는지 쉽게 시각화할 수 있기 때문에 보통 선 재귀를 구성 원리로 간주한다. 선 재귀로 정의된 함수의 구성성(constructiveness)은 wf 트리의 복잡도에 의존한다.

• 증명

  \(\operatorname{(BI)}\):

  만약 어떤 노드 \(s\) 에서 \(F\) 가 성립하지 않는다면, 선 귀납의 가정부에 의하여 \(s\) 의 후행 노드에서 \(F\) 를 만족하지 않는 노드 \(s'\) 이 반드시 하나 이상 있어야 한다. 그러면 그 \(s'\) 의 후행 노드에도 \(F\) 를 만족하지 않는 노드 \(s''\) 이 반드시 하나 이상 있어야 한다. 이런 식으로 어떤 노드 \(s ^{(n)}\) 이 \(F\) 를 만족하지 않으면 가정을 충족시켜야 하므로 \(F\) 를 만족하지 않는 그것의 후행노드 \(s ^{(n+1)}\) 가 반드시 존재해야 한다. 이로써 우리는 무한 경로를 얻는다. 그러나 \(T\) 가 wf 트리이므로 이는 모순이다. 따라서 모든 노드에서 \(F\) 를 만족해야 한다. ▲

  \(\operatorname{(BR)}\):

  \(T\) 가 wf 라는 것과 \(s \prec _Tt:\iff t \subsetneq s\) 와 같이 정의된 트리 관계가 wf 라는 것이 동치라는 것은 증명하기 쉽다. 그러면 \(\operatorname{(BR)}\) 의 증명은 트리 관계에 따른 초한 재귀의 특수한 경우가 된다. ■

Deduction Tree✔

• 위와 같이 준연역트리를 만드는 규칙 1)-4) 는 \(\Delta\) 로부터 공리로의 역연역이다. 즉, 이는 주어진 \(\Delta\) 로부터 공리를 역추적하기 위한 도구이다.

  이 역연역을 계속 해내서 준연역트리를 만들어나간다. 이때 준연역트리가 wf 이면, 즉, 모든 준연역경로가 무한경로가 아니면, 준연역경로들이 각 리프(공리)들로부터 루트 \(\Delta\) 를 도출하는 연역을 보여준다. 즉, \(\svDash{}{\Omega} \Delta\) 라는 것이다.

  만약 준연역트리가 wf 가 아니면, 즉, 무한경로가 존재한다면, \(\Delta\) 로부터 공리를 역추적해낼 수 없었다는 말이 된다. 이는 공리로부터 \(\Delta\) 를 연역해낼 수 없다, 즉, \(\not \svDash{}{\Omega} \Delta\) 라는 것이다.

Proof of Completeness✔

• 다음 증명에서 알 수 있듯이 준연역트리의 준연역경로가 리프를 가질 때, 리프는 공리이고, 이 준연역경로 자체가 공리(리프)로부터 \(\Delta\)(루트)까지의 준연역을 보여준다.

• 증명

  \(\Delta\) 의 모든 준연역경로가 공리를 포함하면, 정의 5.6 2) 에 의하여 각 준연역경로가 유한하다, 즉, 리프를 갖는다. 그러면 무한 경로가 존재하지 않으므로 \(B _{\Delta}\) 는 wf 이다. 이제 \(B _{\Delta}\) 에 대한 선 귀납으로 \(\sigma \in B _{\Delta}\) 에 대한 \(\svDash{}{\Omega} \delta (\sigma )\) 를 보이자.

  \(\delta (\sigma )\) 가 공리인 경우, 즉, \(\sigma \in B _{\Delta}\) 가 리프인 경우:

  자명하게 \(\vDash \delta (\sigma )\) 이다.

  그렇지 않은 경우 \(\delta (\sigma )\) 는 축소가능하다.

  \(\delta (\sigma )\) 의 특별한 축소가능한 식이 \(\bigand_{i \in I}^{}A_i\) 인 경우:

  모든 \(i \in I\) 에 대하여 \(\sigma * \left< i \right> \in B _{\Delta}\) 이고, 귀납적 가정에 의하여 \(\svDash{}{\Omega} \delta (\sigma * \left< i \right>)\), 즉, 모든 \(i \in I\) 에 대하여 \(\svDash{}{\Omega} \delta (\sigma )^{r}, A_i\) 이다. 그러면 추론 \((\land)\) 에 의하여 \(\svDash{}{\Omega} \delta (\sigma )^{r}, \bigand_{i \in I}^{}A_i\), 즉, \(\svDash{}{\Omega} \delta (\sigma )\) 이다.

  특별한 축소가능한 식이 \(\bigor_{i \in I}^{}A_i\) 인 경우:

  \(\sigma * \left< k_0 \right> \in B _{\Delta}\) 인 \(k_0 \in I\) 가 존재한다. 귀납적 가정에 의하여 \(\svDash{}{\Omega} \delta (\sigma )^{r}, A _{k_0}, \bigor_{i \in I}^{}A_i\) 이고, 추론 \((\lor)\) 에 의하여 \(\svDash{}{\Omega} \delta (\sigma )\) 이다. ■

• 증명

  공리를 갖지 않는 \(B _{\Delta}\) 의 경로 \(f\) 를 잡으면, 다음이 성립한다.

  1. \(\sigma \in f\) 이고 식 \(P \in \delta (\sigma )\) 가 원자식이면 모든 \(\sigma \subset \tau \in f\) 에 대하여 \(P \in \delta (\tau)\) 이다.

  왜냐하면 \(P\) 가 축소가능한 식이 아니므로 절대 제거되지 않기 때문이다.

  2. \(\sigma \in f\) 이고 \(R \in \delta (\sigma )\) 가 축소가능한 식이면, 다음을 만족하는 \(\tau \in f\) 가 존재한다.

     • \(\sigma \subset \tau\) 이고 \(R\) 은 \(\delta (\tau)\) 에서 특별하다.

  3. \(\sigma \in f\) 이고 \(\bigand_{i \in I}^{}A_i \in \delta (\sigma )\) 이면 \(A_i \in \delta (\tau)\) 인 \(i \in I\) 와 \(\tau \in f\) 가 존재한다.

  4. \(\sigma \in f\) 이고 \(\bigor_{i \in I}^{}A_i \in \delta (\sigma )\) 이면 모든 \(i \in I\) 에 대하여 \(A_i \in \delta (\tau_i)\) 인 \(\tau_i \in f\) 가 존재한다.

  이제 다음과 같은 할당 \(\Phi\) 를 정의하자.

  \[ \Phi (X) = \{n \in \N : \exists t(t ^{\N } = n \land (\exists \sigma \in f)((t \not\in X) \in \delta (\sigma )))\} \]

  그러면 다음이 성립한다.

  5. 모든 \(\sigma \in f\) 에 대하여 \(\N \not \vDash F ^{\Phi }\) 이고 \(F \in \delta (\sigma )\) 이다.

  a)-e) 들을 쉽게 증명할 수 있다. ■

• 증명

  \(\not \svDash{}{\Omega}F\) 이면 구문론적 주요 보조정리에 의하여 공리를 포함하지 않는 준연역경로가 존재한다. 그러면 의미론적 주요 보조정리에 의하여 \(\N \not \vDash F ^{\Phi }\) 인 할당 \(\Phi\) 를 얻는다. 즉, \(\N \not \vDash F\) 이다. ■

Ordinals✔

관계 \(\svDash{}{\Omega} \Delta\) 는 할당을 사용하지 않고 정의되었으므로 관계 \(\N \vDash F\) 보다 더 문법적으로 정의되었다. 문장의 유한 집합에서 두 정의는 본질적으로 같다. 이제 질문은 이것이다. \(\svDash{}{\Omega}\) 가 \(\vDash\) 보다 더 많은 정보를 주는가? \(\svDash{}{\Omega} \Delta\) 는 무한 브랜칭(branching) wf 트리에 의하여 시각화된다. 이것이 준연역트리의 정의에서 우리가 가져야하는 이미지이다. 그러므로 wf 트리의 복잡도는 식 집합 \(\Delta\) 의 타당성의 복잡도의 척도가 된다. 이 타당한 문장의 복잡도로써 \(\mathsf{Z}_1\) 바깥의 문장들까지도 분류하고, 이로써 각 형식 체계의 능력을 정확하게 측정하는 것이 목표이다.

그러나 트리를 비교하기란 어렵다. 그러므로 wf 트리의 본질적인 정보를 지니는 특유의 크기를 찾아야 한다. 이러한 크기가 트리의 깊이이다. 그러므로 다른 트리보다 복잡한 트리란 더 깊은 트리이다.

wf 트리의 모든 경로는 유한하므로 트리의 깊이를 최대 경로의 길이로 정할 수 있다. 그러나 연역트리는 \(\omega\)-브랜칭 무한 트리이다. 가령, 다음과 같은 무한 브랜치 트리를 생각하자.

이 트리의 모든 경로는 유한하므로 이는 wf 트리이다. 그러나 이 트리는 최대 경로를 갖지 않는다. 이 사례는 자연수로는 무한 브랜칭 트리의 깊이를 서술하기가 불충분하다는 것을 보여준다. 따라서 수학자들은 자연수의 개념을 일반화해야 했다.

자연수는 2가지 특징을 갖는다. 하나는 \(n\) 개처럼 양(기수)을 서술할 수 있는 것이고, 또 하나는 \(0,1,\dots,n-1\) 처럼(첫번째, 두번째, ...) 순서(서수)를 서술할 수 있다는 것이다. 기수와 서수는 유한 집합에서 구분할 수 없다. 그러나 무한 집합에서 이 두 개념은 구분된다.

가령, 작은 수를 왼쪽으로 두는 보통의 순서 관계가 주어진 자연수 집합 \(\N\) 을 생각하자. 보통 자연수의 순서는 \(0,1,2,\dots\) 이다. 이 자연수를 다 센 것을 서수 \(\omega\) 라고 한다. 하지만 자연수의 순서를 \(1,2,3, \dots , 0\) 로 세우고 셀 수도 있다. \(1,2,3, \dots\) 은 \(\N\) 과 동형이므로 서수 \(\omega\) 인데, \(\omega\) 까지 다 세고 \(0\) 을 한 번 더 셌으므로 이것의 서수는 \(\omega +1\) 이다. 한편, 자연수를 짝수와 홀수로, 즉, \(0,2,4, \dots , 1,3,5, \dots\) 로 세울 수도 있다. 짝수와 홀수는 각각 \(\N\) 과 동형이므로 짝수를 다 세면 \(\omega\) 이고 홀수까지 세면 \(\omega +\omega\) 이다. 이때 오직 \(\N\) 만을 다루고 있으므로 집합의 크기는 불변하지만, 순서는 분명 달라졌다. 즉, 초한(transfinite)까지 세는 것이 우리가 관심있는 수의 순서에 대한 측면이다. 우리는 먼저 자연수를 모두 세고도 숫자를 더 셀 수 있는 것이다.

그런데 모든 순서에서 카운팅, 즉, 세는 것이 가능하지 않다. 가령, 음이 아닌 유리수 집합에서 \(0\) 다음에 무엇을 세야 하는가? \(0\) 다음에 셀 수 있는 수가 없는 것은 최소 원소가 존재하지 않기 때문이다. 그러므로 어떤 집합에서 비어있지 않도록 임의의 원소를 제거해도 항상 최소원소가 존재하도록 하는 순서에서만 카운팅이 가능하다. 이러한 순서를 정의하는 개념이 바로 정렬 순서(well-ordering)이다.

이 정렬 순서를 정의해야만 서수도 정의할 수 있다. 먼저 집합론에서 가장 기초적으로 정렬을 살펴보았고, 비슷하게 위상수학에서도 기초적으로 정렬을 살펴보았고, 수리논리학에서 더욱 형식적으로 정렬을 살펴보았었다. 여기에서는 이렇게 정의한다.

두 순서 사이에 순서 보존 사상이 존재하면 두 순서가 동등하다고 한다. 순서형은 순서의 동치류이다. 초한까지 카운팅하기 위해서는 정렬순서의 순서형이 필요하고, 반대로 카운팅 행위 자체가 집합을 정렬한다. 그러므로 정렬순서의 순서형을 서수(ordinal)라고 정의한다. 가령, \(\{0,1,2\}\) 와 \(\{1,2,3\}\) 과 \(\{a,b,c\}\) 은 같은 순서형을 가지므로 같은 서수 \(3\) 으로 표현된다.

공리적 집합론에서 순서의 동치류는 집합이 아니다. 그러나 서수가 전체의 원소, 즉, 집합이 되게 하고 싶다. 이제 문제는 서수의 특유의 표현을 선택하는 것이다. 집합론의 언어에서 \(\in\) 은 유일한 비논리 기호이다. 그러므로 관계 \(\in\) 로 정렬되는 집합을 표현으로 삼는 것이 합리적이다.

순서 \((A, \prec )\) 가 정렬순서라고 하자. \(U \subset A\) 이고, \(a \prec b \in U\) 일 때 \(a \in U\) 이면, \((U, \prec )\) 를 \((A, \prec )\) 의 절편이라고 한다. \(U \subsetneq A\) 이면 절편 \((U, \prec )\) 을 진절편(proper segment)이라고 한다.

정렬순서에 대한 순서관계 \(<\) 를 다음과 같이 정의한다. 이 관계는 서수 모임 \(\operatorname{On}\) 을 정렬한다.

\((A, \prec _A) <(B, \prec _B) : \iff\) \((A, \prec _A)\) 와 동등한 \((B, \prec _B)\) 의 진절편이 존재한다.

서수 \(\beta\) 의 표현 \((A, \prec )\) 에 대하여 집합 \(\{(B, \prec _B) : (B, \prec _B) < (A, \prec )\}\) 의 순서형은 정확하게 서수 \(\beta\) 이다. 그러므로 서수를 \(\beta := \{\alpha :\alpha <\beta \}\) 라고 정의할 수 있고, 이는 \(\alpha \in \beta\) 가 \(\alpha <\beta\) 와 동치라는 것을 함의한다. 그러므로 최종적으로, \(\in\)-관계에 의하여 정렬되는 집합을 서수의 표준적인 표현으로 선택할 수 있다. 그러면 이제, 집합론 위에 서수의 이론을 만들어야 하는데, 집합론에는 기초 공리(foundation axiom)가 존재하므로 서수를 유전적으로 추이적인 집합(hereditarily transitive set)으로만 정의해도 충분하다.

• 증명 이론에서는 서수가 꽤 추상적으로 정의된다. 기초 집합론에서 정의한 서수의 정의를 참고해야 한다.

• 증명

  (정의에 의해 곧바로 도출된다.)

• 이는 \(F\) 를 만족시키는 최소 \(x\) 의 존재성 공리이다.

• 이 기초꼴을 가정하면 \((3.3)\) 의 역방향도 성립한다. 이로써 아래의 다음의 정리가 성립한다. 그러므로 집합론에서 기초 공리를 가정하면 서수를 유전적으로 추이적인 집합으로만 정의해도 충분하다.

• 증명

  \(\implies\):

  \((3.3)\).

  \(\impliedby\):

  \(\in\) 이 전체에서 선형순서라는 것만 보이면 된다.

  기초꼴에 의해 \(\in\) 은 비반사적이고 \(\alpha\) 에서 정초되었다. \(\alpha\) 가 유전적으로 추이적이므로 포함 관계는 \(\alpha\) 에서 추이적이다. 이제 \(\in\) 의 선형성만 보이면 된다. \(\beta\) 가 유전적으로 추이적이라고 가정하고 다음을 보이자.

  \[ \beta \text{ 가} \in \text{에 의하여 정렬되고 } \alpha \subseteq \beta \text{ 이면 }\alpha =\beta \lor \alpha \in \beta \text{ 이다. }\tag{3.6} \]

  \(\alpha \neq \beta\) 를 가정하고 \(\xi\) 를 \(\beta \setminus \alpha\) 에서 \(\in\)-최소 원소라고 하자. 그러면 \(\beta\) 가 추이적이므로 \(\xi\) 의 모든 원소가 \(\beta\) 에 속한다. 하지만 \(\xi\) 가 \(\beta \setminus \alpha\) 에서 \(\in\)-최소 원소이므로 \(\xi\) 의 원소는 모두 \(\alpha\) 에 속하고, 따라서 \(\xi \subseteq \alpha\) 이다. 한편, \(\eta \in \alpha\) 에 대하여 \(\xi \not\in \eta\) 이고 \(\eta \neq \xi\) 이다. 만약 \(\xi \in \eta\) 였다면 \(\alpha\) 의 추이성 때문에 \(\xi \in \alpha\) 이고 이는 모순이다. 어쨌든 \(\beta\) 가 \(\in\) 에 의한 선형 순서를 가지므로 \(\eta \in \xi\), 즉, \(\alpha \subseteq \xi\) 이다. 그러므로 \(\alpha = \xi \in \beta\) 이다. 이로써 \((3.6)\) 에 증명되었다. ▲

  기초꼴의 대우는 다음과 같이 \(\in\)-귀납법이다.

  \[ (\forall x)[(\forall y \in x)F(y) \to F(x)] \to (\forall x)F(x) \]

  이제 \(\alpha\) 가 유전적으로 추이적이면 \(\alpha\) 가 \(\in\) 에 의한 선형 순서를 갖게 된다는 사실을 \(\in\)-귀납법으로 증명하면 된다.

  (나머지 증명은 책에 있다.)

• \((3.6)\) 에 의하여 다음을 얻는다.

  \[ \alpha \in \operatorname{On}\land \beta \in \operatorname{On}\implies (\alpha \subseteq \beta \iff \alpha \leq \beta ) \]

  역방향은 자명하다. \(\alpha <\beta\) 가 \(\beta\) 의 추이성에 의해 \(\alpha \subseteq \beta\) 를 함의하기 때문이다. 그러므로 다음이 성립한다.

  \[ \alpha \in \operatorname{On}\land \beta \in \operatorname{On}\iff (\alpha \subseteq \beta \iff \alpha \leq \beta ) \]

• 증명

  (기초꼴을 가정하지 않아도 보조정리 3.2.1 의 증명에 의하여 이 사실을 얻을 수 있다.)

• 즉, 서수에서 관계 \(\in\) 과 \(<\) 는 일치한다.

• \(\operatorname{On}\) 은 고유 모임이다. \(\operatorname{On}\) 이 유전적으로 추이적인 것과 \(\in\) 에 의하여 정초되었다는 것 때문에 \(\operatorname{On}\) 이 집합이라는 가정은 보조정리 3.2.2 에 의하여 \(\operatorname{On}\in \operatorname{On}\) 이라는 모순을 도출한다.

• 본 정리에 의하여 \(\operatorname{On}\) 에 대한 귀납 원리를 얻는데, 이를 초한 귀납법(transfinite induction)이라 한다.

• 증명

• 증명

Supremum of Ordinal Set✔

지금까지 서수를 꽤 추상적으로 논했다. 집합론적 서수에 대한 감을 잡기 위하여 서수들을 나열해볼 수 있다. 자신의 멤버도 추이적인 최소 추이적 집합은 명백하게 공집합 \(\varnothing\) 이다. \(x\) 가 유전적으로 추이적이면 \(x \cup \{x\}\) 도 유전적으로 추이적임을 곧바로 알 수 있다. 그러므로 다음과 같이 서수를 나열할 수 있다.

결국, 서수는 자신보다 작은 서수를 원소로 갖는 집합이다.

• \(\sup 0 = \sup \varnothing = \bigcup \varnothing = \varnothing = 0\) 이다.

• 서수 \(\alpha\) 가 극한 서수일 경우 \(\sup \alpha = \alpha\) 이고, 그렇지 않을 경우 \(\sup \alpha\) 는 \(\alpha\) 의 이전수이다.

  한원소 집합(singleton set)에 대해서는 \(\sup \{\alpha \} = \alpha\) 이다.

• 다음 예시의 경우 러프하게 \(\max\) 처럼 생각해도 된다.

• 예시

  \[ \begin{align}\begin{split} \sup \{1, 3\} &= \min \{\xi \in \operatorname{On}:(\forall \alpha \in \{1,3\})[\alpha \leq \xi ]\} \\ &= \min \{3,4,5,\dots \} = 3\\ \end{split}\end{align} \tag*{} \]
  \[ \begin{align}\begin{split} \sup \{1, 3\} = \bigcup \{1,3\} &= \{\xi :(\exists \alpha \in \{1,3\})[\xi \in \alpha ]\} \\ &= \{0,1,2 \} = 3\\ \end{split}\end{align} \tag*{} \]

• 다음 예시처럼 유한 서수에 \(\sup\) 가 적용된 경우 러프하게 \(-1\) 로 생각해도 된다.

• 예시

  \[ \begin{align}\begin{split} \sup 3 = \sup \{0, 1, 2\} &= \min \{\xi \in \operatorname{On}:(\forall \alpha \in \{0, 1, 2\})[\alpha \leq \xi ]\} \\ &= \min \{2, 3, 4, \dots \} = 2\\ \end{split}\end{align} \tag*{} \]
  \[ \begin{align}\begin{split} \sup 3 = \sup \{0, 1, 2\} = \bigcup \{0, 1,2\} &= \{\xi :(\exists \alpha \in \{0, 1,2\})[\xi \in \alpha ]\} \\ &= \{0,1 \} = 2\\ \end{split}\end{align} \tag*{} \]

• 예시

  \[ \begin{align}\begin{split} \sup \omega = \sup \{0,1,\dots \} &= \bigcup \omega = \{\xi :(\exists \alpha \in \omega )[\xi \in \alpha ]\} \\ &= \{0,1,\dots \} = \omega \\ \end{split}\end{align} \tag*{} \]
  \[ \begin{align}\begin{split} \sup (\omega+1) = \sup \{\overbrace{0,1,\dots}^{\omega } ,\omega \} &= \bigcup (\omega + 1) \\ &= \{\xi :(\exists \alpha \in (\omega+1) )[\xi \in \alpha ]\} \\ &= \{0,1,\dots \} = \omega \\ \end{split}\end{align} \tag*{} \]
  \[ \begin{align}\begin{split} \sup (\omega+2) &= \sup \{\overbrace{0,1,\dots}^{\omega } ,\omega,\omega +1 \} \\ &= \bigcup (\omega + 2) \\ &= \{\xi :(\exists \alpha \in (\omega+2) )[\xi \in \alpha ]\} \\ &= \{0,1,\dots,\omega \} = \omega+1 \\ \end{split}\end{align} \tag*{} \]

• 증명

Successor, Limit Ordinal✔

• 극한 서수의 존재성은 무한 공리에 의하여 보장된다.

극한 서수의 존재는 증명 불가능하다. 따라서 공리적 집합론에서는 최소한 하나의 극한 서수의 존재성을 요구하는 무한 공리가 필요하다. 우리의 경우 그러한 공리는 단지 \(\exists \lambda (\lambda \in \operatorname{Lim})\) 가 된다. 그러나 정칙 서수 모임 \(\operatorname{Reg}\) 에 대하여 다음과 같은 무한 공리의 더 강한 형태가 필요하다.

\(\operatorname{Reg}\) 는 \(\operatorname{On}\) 에서 무계이다. 즉, \(\forall \xi \in \operatorname{On}\exists \eta \in \operatorname{Reg}(\xi <\eta )\)

그러나 집합론이 주제가 아니므로 이런 강한 형태를 증명하지 않고 기본 성질이라고 하고 넘어간다.

Transfinite Induction✔

• 초한 귀납(6.2, 6.16)

• 증명

  가정이 성립하는데 \(M = \{\xi \in \operatorname{On}: \lnot F(\xi )\} \neq \varnothing\) 이라고 하자. 그러면 \(\alpha := \min M\) 을 잡을 수 있다.

  가정부의 첫번째 조건 \(F(0)\) 에 의하여 \(\alpha \neq 0\) 이다. ▲

  \(\alpha = \beta '\) 이면 \(\alpha\) 가 \(M\) 의 최소 서수이므로 \(\beta \not\in M\) 이고, 이에 따라 \(F(\beta )\) 이다. 그러면 가정부의 두번째 조건에 의하여 \(F(\beta ') = F(\alpha )\) 이다. 이는 모순이다. ▲

  그렇다면 \(\alpha \in \operatorname{Lim}\) 이어야만 하는데, 가정부의 세번째 조건에 의하여 \((\forall \xi <\alpha )F(\xi ) \implies F(\alpha )\) 인데, \(\alpha\) 보다 작으면 \(F\) 를 만족하므로 결국 \(F(\alpha )\) 이다. ■

field, restriction✔

Transfinite Recursion✔

• 원시 재귀를 초한까지 일반화시킨 것이 초한 재귀이다.

  가령, \(\alpha = 3\) 이면 \(3 = \{0,1,2\}\) 이므로 제한의 정의에 의하여 \(F \restriction 3\) 은 \(0, 1, 2\) 에 대한 함숫값만을 지닌다. 그러므로 \(F(3)\) 을 \(G(F \restriction 3)\) 으로 정의하는 것은 \(3\) 이전의 \(F\) 의 함숫값에 의하여 \(F\) 를 정의하는 재귀가 된다. 이 재귀가 모든 서수 \(\operatorname{On}\) 에 대하여 진행되므로 이는 원시 재귀를 초한까지 일반화시킨 초한 재귀가 되는 것이다.

• 서수의 세 종류를 따라 초한 재귀의 원리를 다음과 같이 재형식화 할 수 있다.

  • 집합 \(a\) 와 집합들을 집합들로 보내는 함수 \(S\) 와 \(L\) 에 대하여 다음을 만족하는 유일하게 정의되는 함수 \(F:\operatorname{On}\to V\) 가 존재한다.

    \[ F(0) = a \]
    \[ F(\alpha ') = S(F(\alpha )) \]
    \[ \lambda \in \operatorname{Lim}\implies F(\lambda ) = L(F \restriction \lambda ) \]

• 초한 재귀 원리는 \(a \in A\) 에 대한 모임 \(\prec \restriction a := \{b \in A : b \prec a\}\) 이 항상 집합이라는 조건 하에서 정초 관계 \((A, \prec )\) 로 확장될 수 있다.

• 증명

  \(F\) 의 존재성:

  다음과 같이 정의하자.

  \[ \begin{align}\begin{split} M:= \{f : \enspace &f: \operatorname{On}\to _pV \land \operatorname{dom} (f) \in \operatorname{On}\land \\ &(\forall \alpha \in \operatorname{dom} (f))[f(\alpha ) = G(f \restriction \alpha )]\}\\ \end{split}\end{align} \tag{1} \]

  그러면 \(\alpha\) 에 대한 귀납법으로 다음을 얻을 수 있다.

  \[ f \in M \land g \in M \land \alpha \in \operatorname{dom} (f) \cap \operatorname{dom} (g) \implies f(\alpha ) = g(\alpha ) \tag{2} \]

  귀납적 가정에 의하여 \(f \restriction \alpha = g \restriction \alpha\) 이고, 따라서 \(f(\alpha ) = G(f \restriction \alpha ) = G(g \restriction \alpha ) = g(\alpha )\) 를 얻는다. 이제 다음과 같이 정의하자.

  \[ F:= \{(\alpha ,b) : (\exists f \in M)[f(\alpha ) = b]\} \tag{3} \]

  \((2)\) 에 의해 모임 \(F\) 는 함수이다. 다음을 보여야 한다.

  \[ (\forall \alpha \in \operatorname{On})(\exists b)[F(\alpha ) = b] \land F \restriction \alpha ' \in M \tag{4} \]

  \(\alpha\) 에 대한 귀납법으로 \((4)\) 를 증명하자. \(\alpha \in \operatorname{On}\) 를 잡자. 귀납적 가정에 의하여 \(f_0 := F \restriction \alpha \in M\) 이다. 다음과 같이 정의하자.

  \[ f(\beta ) := \begin{cases} f_0(\beta ) & \beta < \alpha \\ G(f_0 \restriction \alpha ) & \beta = \alpha \\ \end{cases} \]

  그러면 \(\operatorname{dom} (f) = \alpha ' \in \operatorname{On}\) 이고 모든 \(\beta \leq \alpha\) 에 대하여 \(f(\beta ) = G(f \restriction \beta )\) 이다. 즉, \(f \in M\) 이다. 그러므로 \(F(\alpha ) = f(\alpha )\) 이고 \(F \restriction \alpha ' = f\) 이다. 이로써 \((4)\) 가 증명되었다. ▲

  \(F\) 의 유일성:

  유일성에 대해서는 \(H\) 가 정리의 성질을 만족하는 두번째 함수임을 가정하고 \(F(\alpha ) = H(\alpha )\) 를 \(\alpha\) 에 대한 귀납법으로 보이면 되는데, 이는 쉽다. ■

• 증명

  (증명은 본질적으로 정리 3.2.7 의 증명과 같다. 그러나 \(\prec\) 이 추이적이라는 가정이 없으므로 엄밀한 증명은 \((A, \prec )\) 의 추이적 폐포(transitive closure)의 정의 같은 추가적인 사전지식이 필요하다. 그러나 이 사전지식을 모두 짚고 넘어가려면 집합론에 꽤 딥하게 들어가야만 한다. 따라서 증명을 생략하는 것이 낫다. 엄밀한 증명은 집합론에 대한 전공서적들에서 찾을 수 있다.)

Cardinality✔

• 모든 집합이 정렬될 수 있다고 가정한다면(이는 선택 공리와 동치이다) 서수에 의하여 집합의 크기를 측정할 가능성이 존재한다.

• \(a \sim b \iff \overline{\overline{a}} = \overline{\overline{b}}\) 이므로 집합의 크기를 기수를 판정함으로써 측정할 수 있다.

Initial Ordinal✔

• 기수는 초기 서수이다.

  즉, 초기 서수는 그것보다 작은 서수와 기수가 동등하지 않은 서수이다. 그러므로 유한 서수는 모두 초기 서수이다. \(\omega\) 는 무한하지만 초기 서수이며, 기수이다. 반면 무한서수 \(\omega ^{2}\) 는 다음을 만족하므로 자신보다 작은 \(\omega\) 와 기수가 같고, 이에 따라 초기 서수가 아니다.

  \[ \overline{\overline{\omega ^{2}}} = \omega \]

  \(\omega\) 보다 큰 첫 기수 \(\omega ^{+}\) 를 \(\omega _1\) 라고 표기한다.

Regular Ordinal✔

• 정칙 서수는 위키에서 다음과 같이 정의된다.

  극한 서수 \(\alpha\) 가 \(\alpha\) 보다 작은 순서형을 가지면서 \(\alpha\) 보다 작은 서수로 이루어진 집합의 극한이 아니면 정칙 서수라고 한다.

  이는 위 정의와 같은 말이다. 즉, \(\alpha\) 보다 작은 서수로 이루어진 집합의 기수가 \(\alpha\) 의 기수보다 작은데도 \(\alpha\) 에 근사된다면, 특이하다고 해서 특이 서수라고 한다. 그런 집합이 \(\alpha\) 에 근사되지 않으면 일반적이다, 정칙적이다 라고 해서 정칙 서수라고 한다.

  • 예시

    \(\omega\) 보다 작은 서수들은 유한한데, 유한 서수의 유한열은 반드시 유한한 최댓값을 가진다. 그러므로 \(\omega\) 는 \(\omega\) 보다 작은 서수를 원소로 갖고 \(\omega\) 보다 작은 순서형을 갖는 그 어떠한 열의 극한도 아니다. 그러므로 \(\omega\) 는 정칙 서수이다.

    한편, 정칙 기수라는 개념도 있는데, 이는 정칙 서수와 동치이다. \(\aleph _0\) 는 그것의 초기 서수 \(\omega\) 가 정칙 서수이므로 정칙 기수이다.

    \(\omega +1\) 은 극한 서수가 아니므로 특이 서수이다.

    \(\omega +\omega\) 는 \(\omega\) 이후로 처음 나타나는 극한 서수이다. 이는 열 \(\omega ,\omega +1,\omega +2,\dots\) 의 극한으로 볼 수 있다. 이 열은 순서형 \(\omega\) 를 갖는다. 그러므로 \(\omega +\omega\) 는 자신보다 작은 서수로 이루어지고 \(\omega +\omega\) 보다 작은 순서형을 갖는 열의 극한이다. 따라서 \(\omega +\omega\) 는 특이 서수이다.

    \(\aleph _1\) 은 \(\aleph _0\) 보다 큰 다음 기수이다. 연속체 가설에서 이는 실수 \(\R\) 의 기수이다. \(\aleph _1\) 은 정칙 기수의 정의에 의하여 정칙 기수가 된다. 그러므로 \(\omega _1\) 도 정칙 서수이다.

    \(\aleph _{\omega }\) 는 열 \(\aleph _0, \aleph _1, \aleph _2, \dots\) 다음에 나타나는 기수이다. 이것의 초기 서수 \(\omega _{\omega }\) 는 열 \(\omega ,\omega _1, \omega _2, \dots\) 의 극한이다. 이 열의 순서형은 \(\omega\) 이므로 \(\omega _{\omega }\) 는 특이 서수이다. 그러므로 \(\aleph _{\omega }\) 도 특이 기수이다. 이는 최초의 특이 기수이다.

  • 위 예시를 본 정의를 기준으로 다시 살펴보자.

    \(\omega\) 보다 작은 서수 집합은 오직 최소한 \(\omega\) 크기를 가져야만 \(\omega\) 에 근사될 수 있다. 따라서 \(\omega\) 는 정칙 서수이다. 즉, 모든 \(x \subseteq \omega\) 에 대하여 다음이 성립하므로 정칙 서수이다.

    \[ \overline{\overline{x}} < \omega \implies \sup x < \omega \]

    \(\omega +1\) 은 초기 서수가 아니므로 특이 서수이다.

    \(\omega +\omega\) 를 조사하자. 열 \(\omega , \omega +1, \omega +2, \dots\) 은 \(\omega +\omega\) 보다 작은 서수로 이루어져있고 그 크기도 \(\omega +\omega\) 보다 작은 \(\omega\) 이다. 그럼에도 불구하고 이 열은 \(\omega +\omega\) 로 근사된다. 그러므로 \(\omega +\omega\) 는 특이 서수이다. 즉, \(x = \{\omega ,\omega +1, \omega +2, \dots \}\) 로 잡으면 다음이 성립하므로 특이 서수이다.

    \[ \overline{\overline{x}}(=\omega ) < \omega \implies \sup x = \omega + \omega \]

    \(\omega _{\omega }\) 를 조사하자. 열 \(\omega , \omega _1, \omega _2, \dots\) 은 \(\omega _{\omega }\) 보다 작은 서수로 이루어져있고 그 크기도 \(\omega _{\omega }\) 보다 작은 \(\omega\) 이다. 그럼에도 이 열은 \(\omega _{\omega }\) 로 근사된다. 따라서 \(\omega _{\omega }\) 는 특이 서수이다. 즉, \(x = \{\omega ,\omega _1, \omega _2, \dots \}\) 로 잡으면 다음이 성립하므로 특이 서수이다.

    \[ \overline{\overline{x}}(=\omega ) < \omega \implies \sup x = \omega_\omega \]

  • 본 정의는 유한 서수를 정칙 서수로 인정하는 뉘앙스이고, 위키의 정의는 유한 서수는 정칙 서수로 인정하지 않는 뉘앙스이다. 그러나 애초에 유한 서수 자체가 그렇게 중요한 화두가 아니라서, 크게 신경쓰지 않아도 될듯.

• 정칙 서수이면 기수이다. 그러나 \(\aleph _{\omega }\) 처럼 기수여도 정칙 서수가 아닐 수 있다. 그러므로 정칙 서수는 기수의 진 부분 집합이다. 임의의 서수 \(\alpha\) 에 대하여 \(\alpha\) 보다 큰 최소 기수 \(\alpha ^{+}\) 가 존재한다. \(\alpha ^{+}\) 형태의 모든 기수는 정칙이다.

  집합론에서는 기수의 모임과 정칙 기수의 모임이 \(\operatorname{On}\) 에서 무계이고, 따라서 고유 모임이라는 사실이 알려져있다.

• 증명

  \(M\) 이 유계라면 \(M\) 의 상계 모임 \(\bar{M} = \{\xi \in \operatorname{On}: \forall \eta \in M(\eta \leq \xi )\}\) 은 비어있지 않으므로 \(\sup M := \min \bar{M}\) 으로 잡으면 된다. ■

• 증명

  6.8 의 증명의 맥락을 재사용하면, \(\beta < \sup M \implies \beta \not\in \bar{M} \implies \exists \eta \in M(\beta <\eta )\) 이다. ■

• 증명

  \(\sup M = 0\) 이면 \(M \neq \varnothing\) 은 \(M = \{0\}\) 를 의미한다. 즉, \(\sup M = \max M\) 이다.

  \(\sup M = \alpha '\) 이면 보조정리 6.10 에 의하여 \(\alpha < \eta \leq \alpha '\) 인 \(\eta \in M\) 가 존재한다. 그러므로 \(\eta =\alpha ' \in M\) 이고, \(\sup M = \max M\) 이다.

  그 외의 경우 \(\sup M \in \operatorname{Lim}\) 이다. ■

• 지금까지 \(\omega\) 를 자연수 집합 \(\N\) 의 서수로 암묵적으로 사용해와서 늦은 감이 있지만, 이렇게 \(\omega\) 를 엄밀하게 정의한다.

• 증명

• \(\omega _1\) 은 최초의 비가산 서수이다. 연속체 가설을 가정하면 이는 실수 집합 \(\R\) 의 기수이다.

• 증명

Order type✔

• 증명

• 보조정리 6.15 에 의하여 \(\operatorname{Otyp}(M) = \operatorname{On}(M) = \operatorname{On}\) 이거나 \(\operatorname{Otyp}(M) = \beta\) 인 서수 \(\beta\) 가 존재한다.

  보조정리 6.18 에 의하여 \(\operatorname{ord}_M\) 은 \(M\) 에 의하여 유일하게 결정된다.

• 증명

• 증명

Closed, Continuous, Normal Function✔

• \(\kappa\) 가 \(M\) 보다 작으면, \(\kappa\) 에서 유계인 \(M\) 의 어떠한 부분집합을 가져와도 반드시 \(\sup U \in M\) 이다. 이 경우 \(M\) 은 항상 \(\kappa\) 에서 닫혀있다. 그러므로 만약 집합 \(M\) 이 무계이면 어떤 \(\kappa\) 를 잡아도 항상 그것에 대하여 닫혀있다.

  \(\kappa\) 가 \(M\) 과 같거나 크면, \(M\) 의 부분집합인 \(M\) 그 자체의 상한은 \(\sup M \not\in M\) 이 아닐 수도 있다. 이러한 경우 \(M\) 이 \(\kappa\) 에서 닫혀있지 않을 수도 있다.

• 증명

  \(\implies\):

  \(\operatorname{ord}_{M}\) 이 (\(\kappa\)-)연속이라고 하자. 그러면 \(\operatorname{Otyp}(M)\) 은 (\(\kappa\)-)닫혀있다. \(U \neq \varnothing\) 이고 \(U \subset M\) 이고 \(U\) 가 (\(\kappa\) 에서) 유계라고 하자. \(B := \operatorname{ord}_M ^{-1}(U)\) 라고 정의하면, \(\xi \in B\) 에 대하여 \(\xi \leq \operatorname{ord}_M(\xi ) \in U\) 이다. 그러므로 \(B\) 도 (\(\kappa\) 에서) 유계이다. 그러면 \(\sup B \in \operatorname{Otyp}(M)\) 이 존재하고, \(\operatorname{ord}_M(\sup B) \in M\) 이다. \(\operatorname{ord}_M\) 의 연속성에 의하여 \(\operatorname{ord}_M(\sup B) = \sup \{\operatorname{ord}_M(\xi ):\xi \in B\} = \sup U\) 이다. ▲

  \(\impliedby\):

  (나머지 증명은 책에 있다.)

• 즉, 순증가하면서 연속이면 정규 함수이다. 정규 함수의 핵심 요소는 연속과 순증가이다. 다음과 같은 위키의 정의를 참고하자.

  함수 \(f: \operatorname{On}\to \operatorname{On}\) 가 정규인 것은 그것이 순서 위상에 대하여 연속이고 순증가인 것과 동치이다. 즉, 이 조건은 다음과 같다.

  1. 모든 극한 서수 \(\gamma\) 에 대하여 \(f(\gamma ) = \sup \{ f(v) : v < \gamma \}\) 이다.
  2. 모든 서수 \(\alpha <\beta\) 에 대하여 \(f(\alpha )<f(\beta )\) 이다.

• 예시

  \(f(\alpha ) = \alpha + 1\) 은 정규가 아니다. 이 함수는 어떠한 극한 서수에서도 연속이 될 수 없기 때문이다. 함수의 정의에 따라 \(f(\omega ) = \omega + 1\) 인데 위 연속의 조건을 살펴보면 다음과 같다.

  \[ \begin{align}\begin{split} f(\omega ) &= \sup \{f(v) : v < \omega \} = \sup \{f(0), f(1), \dots \} \\ &= \sup \{1, 2, \dots \} = \omega \\ \end{split}\end{align} \tag*{} \]

  본 정의의 연속의 조건을 살펴봐도 다음과 같다.

  \[ \begin{align}\begin{split} \sup f[\omega ]&= \sup \{f(0), f(1), \dots \} = \omega \\ f(\sup \omega )&= f(\omega ) = \omega + 1 \\ \end{split}\end{align} \tag*{} \]

  반면, \(f(\alpha ) = 1 + \alpha\) 는 정규함수이다.

• 증명

  1.

  \(\impliedby\):

  \(M\) 이 무계이면 정리 6.23 에 의하여 \(\operatorname{dom} (\operatorname{ord}_M) = \operatorname{On}\) 이다. 즉, 정의역이 \(\operatorname{On}\) 이다. \(M\) 이 닫혀있으면 보조정리 6.25 에 의하여 \(\operatorname{ord}_M\) 의 연속성이 성립한다. 보조정리 6.21 은 \(\operatorname{ord}_M\) 이 순서를 보존한다는 것을 보장한다.

  \(\implies :\)

  \(\operatorname{ord}_M\) 이 정규 함수라고 하자. 보조정리 6.25 에 의하여 \(M\) 은 닫혀있고, 정리 6.23 에 의하여 \(\operatorname{dom} (\operatorname{ord}_M) = \operatorname{On}\) 이다. ▲

Ordinal Arithmetic✔

Addition✔

• 증명

• 증명

• \(\alpha +1=(\alpha +0')=\alpha '\) 이므로 \(\alpha '\) 대신 \(\alpha +1\) 라고 쓸 수 있다.

Principal Ordinal✔

• 주요 서수 모임은 닫혀있고 무계이다. 이것의 열거 함수 \(\omega ^{\alpha }\) 는 정규 함수이다.

• 예시

  \(1\) 은 주요 서수이다. \(0 + 0 < 1\) 이기 때문이다. \(1\) 외에 유한 주요 서수는 없다.

  \(\omega\) 는 자명하게 주요 서수이고, 일반적으로 모든 무한 초기 서수, 즉, 기수는 주요 서수이다.

  (이 사실들을 아래의 보조정리 3.3.5 에서 증명한다.)

• 증명

  5:

  \(\alpha <\kappa\) 를 잡아보자. \(\alpha _0:= \alpha ', \alpha _{n+1} := \alpha _n + \alpha _n, M := \{\alpha _n : n < \omega \}\) 라고 정의하자. 그러면 보조정리 7.2 에 의하여 \(M \subset \kappa\) 이고 \(M\) 과 \(\omega < \kappa\) 사이의 전단사 함수가 존재한다. 따라서 \(M\) 은 \(\kappa\) 에서 유계이고 \(\alpha < \alpha _0 \leq \sup M := \beta < \kappa\) 를 얻는다. \(\eta ,\xi < \alpha _n\) 인 \(n < \omega\) 를 잡을 수 있고 \(\xi + \eta \leq \alpha _n + \eta < \alpha _n + \alpha _n = \alpha _{n+1}\leq \beta\) 이므로 \(\beta \in \Bbb{H} \cap \kappa\) 이다. 따라서 \(\Bbb{H}\) 는 \(\kappa\) 에서 무계이다. ▲

  \(\kappa\) 에서 유계인 \(U \subset \Bbb{H}\) 를 잡자. 그러면 \(\sup U < \kappa\) 이다. \(\eta ,\xi < \sup U\) 에 대하여 \(\eta ,\xi < \rho\) 인 \(\rho \in U\) 가 존재한다. 따라서 \(\xi +\eta <\rho \leq \sup U\) 는 \(\sup U \in \Bbb{H}\) 를 함의한다. 즉, \(\Bbb{H}\) 는 \(\kappa\) 에서 닫혀있다. ■

• \(\Bbb{H}\) 안의 주요 서수가 서수 \(\beta\) 에 대한 \(\omega ^{\beta }\) 의 형태이므로 \(\Bbb{H}\) 의 열거함수로 \(\omega\) 의 지수를 정의한다.

• 증명

  1) 에 대해서는 위 정의에서 언급했다. 2)-4) 는 자명하다. ▲

  5) 는 쉽게 증명된다.

• 증명

  \(\implies\):

  \(\alpha \in \Bbb{H}\) 라고 하자. \(\alpha =1\) 이면 \(1\) 보다 작은 서수는 \(0\) 이고, \(0 + 1 = 1\) 이다. 그렇지 않은 경우 \(\alpha \in \operatorname{Lim}\) 이고 \(\xi + \alpha = \sup \{\xi +\eta :\eta <\alpha \} \leq \alpha \leq \xi +\alpha\) 이다. ▲

  \(\impliedby\):

  \(\xi ,\eta <\alpha\) 에 대하여 \(\xi +\eta <\xi +\alpha =\alpha\) 이다. ■

• 증명

  (정리 3.3.6 에서 곧바로 나온다.)

Cantor normal-form✔

• 증명

  존재성:

  \(\alpha\) 에 대한 귀납법으로 증명하자. \(\alpha \in \Bbb{H}\) 에 대하여 \(\alpha = _{NF}\alpha\) 이다. 그렇지 않은 경우 \(\xi ,\eta <\alpha\) 에 대하여 \(\alpha =\xi +\eta\) 이다. 귀납적 가정에 의하여 \(\xi = _{NF}\xi _1+\dots +\xi _m\) 이고 \(\eta =_{NF}\eta _1+\dots +\eta _n\) 이다. 그러면 \(\xi _j \geq \eta _1\) 를 만족하는 가장 큰 인덱스 \(1 \leq j \leq m\) 에 대하여 \(\alpha = _{NF}\xi _1 + \dots + \xi _j + \eta _1 + \dots + \eta _n\) 가 성립한다. ▲

  유일성:

  (나머지 증명은 책에 있다.)

• 증명

  정리 3.3.8 칸토어 표준형에 의하여 자명하다. ■

Multiplication and Exponentiation✔

Notation System for a Segment of the Ordinals✔

• 증명

  \(\omega _0(0) = 0, \omega _1(0) = \omega ^{0} = 1, \omega _2(0) = \omega ^{1} = \omega, \omega _{3}(0) = \omega ^{\omega }, \omega _4(0) = \omega ^{\omega ^{\omega }}, \dots , \omega _n(0) = \omega ^{\overbrace{\omega ^{\rddots ^{\omega }}}^{n-2}}\) 을 참고하면, \(n\) 에 대한 귀납으로 \(\omega _n(0) < \omega _{n+1}(0)\) 을 쉽게 얻을 수 있다는 것을 알 수 있다. 그러므로 집합 \(M = \{\omega _n(0) : n < \omega \}\) 은 최댓값을 갖지 않는다. 정리 6.11 의 증명과정을 보면 \(\sup M\) 은 \(\max M\) 이거나 \(\sup M \in \operatorname{Lim}\) 인데, 최댓값이 존재하지 않으므로 정리 6.11 에 의하여 반드시 \(\sup M = \omega _{\omega }(0) \in \operatorname{Lim}\) 이어야 한다. 그러므로 다음이 성립한다.

  \[ \begin{equation}\begin{split} \omega ^{\omega _{\omega }(0)} &= \sup \{\omega ^{\xi } : \xi < \omega _{\omega }(0)\} = \sup \{\omega ^{\omega _n(0)} : n < \omega \} \\ &= \sup \{\omega _{n+1}(0) : n < \omega \} = \omega _{\omega }(0) \\ \end{split}\end{equation} \tag*{} \]

  이 결과는 \(\epsilon_0 \leq \omega _{\omega }(0)\) 임을 보여준다. 만약 \(\epsilon_0 < \omega _{\omega }(0)\) 라면 \(\omega _n(0) \leq \epsilon_0 < \omega _{n+1}(0)\) 인 \(n < \omega\) 이 존재하게 되고, 이로부터 \(\omega _{n+1}(0) \leq \omega ^{\epsilon_0} = \epsilon_0 < \omega _{n+1}(0)\) 를 얻는데 이는 불가능하다. ■

• 기수에서는 고작 \(2 ^{\aleph _0} = \mathfrak{c}\) 가 되는데, 서수에서는 어째서 \(\omega ^{\omega ^{\omega ^{\rddots }}} < \omega _1\) 일까.

• 증명

  보조정리 7.9 에 의하여 \(\lambda \xi .\omega ^{\xi }\) 는 \(\Omega\)-정규 함수이다. 따라서 모든 \(n\) 에 대하여 \(\omega _n(0) < \Omega\) 이다. \(\{\omega _n(0) : n < \omega \}\) 를 \(\omega < \Omega\) 로 보내는 전단사 함수가 존재하므로 이 집합은 \(\Omega\) 에서 유계이다. 따라서 \(\epsilon_0 = \sup \{\omega _n(0) : n < \omega \} < \Omega\) 이다. ■

• 이로써 \(\epsilon_0\) 아래의 모든 서수를 \(\text{E}\) 의 원소로 표현할 수 있다. 하지만 이 표현은 유일하지 않기 때문에 유일성을 위하여 표준형을 사용한다.

• 증명

  먼저 다음을 보이자.

  \[ \alpha \in \text{E} \implies \alpha < \epsilon_0 \tag{1} \]

  \(0 < \epsilon_0\) 은 자명하다. \(\epsilon_0 \in \Bbb{H}\) 이므로 \(\alpha ,\beta <\epsilon_0\) 에 대하여 \(\alpha +\beta <\epsilon_0\) 이다. \(\alpha <\epsilon_0\) 이면 \(\omega ^{\alpha }< \omega ^{\epsilon_0} = \epsilon_0\) 이다. ▲

  이제 다음을 \(\alpha\) 에 대한 귀납으로 보이자.

  \[ \alpha <\epsilon_0 \implies \alpha \in \operatorname{E} \tag{2} \]

  \(\alpha =0\) 이면 자명하다. \(\alpha \in \Bbb{H}\) 이면 \(\alpha =\omega ^{\xi }\) 인 \(\xi \leq \alpha\) 가 존재한다. \(\alpha <\epsilon_0\) 은 \(\xi < \alpha\) 를 함의한다. 그러면 귀납적 가정에 의하여 \(\xi \in \operatorname{E}\) 이고 정의 8.4 3) 에 의하여 \(\alpha = \omega ^{\xi } \in \operatorname{E}\) 이다.

  \(\alpha \not\in \Bbb{H}\) 이면 \(\alpha _1+\alpha _2=\alpha\) 인 \(\alpha _1,\alpha _2<\alpha\) 가 존재한다. 귀납적 가정에 의하여 \(i=1,2\) 에 대하여 \(\alpha _i \in \operatorname{E}\) 이고, 정의 8.4 2) 에 의하여 \(\alpha =\alpha _1+\alpha h_2 \in \operatorname{E}\) 이다. ■

• 증명

  칸토어 표준형 정리에 의하여 \(\alpha =_{NF} \omega ^{\alpha _1}+\dots +\omega ^{\alpha _n}\) 인 서수 \(\alpha _1,\dots ,\alpha _n\) 가 유일하게 결정되고, 존재한다. \(\alpha \in \operatorname{E}\) 는 \(\alpha <\epsilon_0\) 을 함의하고, 이로써 \(\alpha _1,\dots ,\alpha _n < \alpha \subset \epsilon_0 = \operatorname{E}\) 이다. ■

• \(\ulcorner 0\urcorner = 0\), \(1 = _{NF} \omega ^{0}\) 이므로 \(\ulcorner 1\urcorner = \left< 1, \ulcorner 0\urcorner \right>\), \(2 = _{NF} \omega ^{0} + \omega ^{0}\) 이므로 \(\ulcorner 2\urcorner = \left< 1, \ulcorner 0\urcorner, \ulcorner 0\urcorner \right>\), \(\dots\)

  \(\omega = _{NF} \omega ^{1}\) 이므로 \(\ulcorner \omega \urcorner = \left< 1, \ulcorner 1\urcorner \right>\), \(\omega \cdot 2 = _{NF} \omega ^{1} + \omega ^{1}\) 이므로 \(\ulcorner \omega \cdot 2\urcorner = \left< 1, \ulcorner 1\urcorner, \ulcorner 1\urcorner \right>\), \(\dots\)

• 증명

  먼저 다음을 얻는다.

  \[ \begin{equation}\begin{split} n \in \ulcorner \operatorname{E}\urcorner \iff & n =0 \lor \operatorname{Seq}(n) \land (n)_0 = 1 \\ & \land \forall x < \operatorname{lh}(n)(0 < x \implies (n)_x \in \ulcorner \operatorname{E}\urcorner) \\ &\land \forall x < \operatorname{lh}(n) - 1(0 < x \implies (n) _{x+1} \leq (n)_{x}) \\ \end{split}\end{equation} \tag*{} \]
  \[ \begin{equation}\begin{split} n_1 \prec n_2 \iff & n_1 \in \ulcorner \operatorname{E}\urcorner \land n_2 \in \ulcorner \operatorname{E}\urcorner \land [(n_1 = 0 \land n_2 \neq 0) \\ & \lor (\exists x < \min \{\operatorname{lh}(n_1), \operatorname{lh}(n_2)\} ((n_1)_x \prec (n_2)_x) \\ & \land \forall y < x ( 0 < y \implies (n_1)_y = (n_2)_y)) \\ & \lor (\operatorname{lh}(n_1) < \operatorname{lh}(n_2) \land \forall x<\operatorname{lh}(n_1)((n_1)_x = (n_2)_x))] \\ \end{split}\end{equation} \tag*{} \]

  따라서 집합 \(\ulcorner \operatorname{E}\urcorner\) 와 관계 \(\prec\) 은 course-of-value 재귀에 의하여 동시에 정의가능하고, 이 둘은 원시 재귀이다. ■

• course-of-value 재귀

Norm Function for \(\Pi_{1}^{1}\)-sentence✔

서수를 정의했으니 이제 본격적으로 wf 트리의 복잡도를 측정하여 식 집합 \(\Delta\) 의 타당성의 복잡도를 측정해보자.

• 이로써 공리의 연역의 길이를 \(0\) 으로 정의하고, \((\land)\) 이나 \((\lor)\) 의 연역을 한 단계 진행하면 연역의 길이가 \(1\) 씩 늘어나게 된다. \(\svDash{a}{\Omega}\) 에서 \(a\) 가 연역의 길이를 뜻하게 된다. 이것으로 무한 체계의 연역을 나타내는 wf 트리의 복잡도를 측정할 수 있다.

• 이 정리는 정의 5.2 에서 정의한 타당성 관계 \(\svDash{}{\Omega}\) 의 타당성의 복잡도를 \(\svDash{\alpha }{\Omega}\) 로써 정확하게 분석해낼 수 있다는 것을 말해준다. \(\svDash{}{\Omega}\) 의 건전성과 완전성을 증명해서 자연수 구조 \(\N\) 의 타당성 관계 \(\vDash\) 를 완전하게 \(\svDash{}{\Omega}\) 으로 교체할 수 있었다. 이는 \(\mathsf{Z}_1\) 의 불완전성 때문에 \(\mathsf{Z}_1\) 이 연역해낼 수 없는 \(\mathsf{Z}_1\) 바깥에 있는 식까지의 복잡도도 측정하기 위해서이다. 이를 위해 서수를 도입하여 wf 트리인 연역 트리의 최대 경로의 길이를 측정하려 했다. 서수를 도입한 것은 wf 트리의 최대 경로를 자연수로는 측정할 수 없기 때문이었다.

  즉, 이 정리에 도착한 시점에서 우리는 자연수 구조 \(\N\) 에서 참인 문장의 타당성의 복잡도를 제대로 측정할 수 있게 된 것이다. 그러므로 참인 문장 \(F\) 의 타당성의 척도를 아래와 같이 정의할 수 있다.

• 증명

  1:

  \(\implies\):

  \(\svDash{\alpha }{\Omega}\Delta\) 의 정의의 귀납에 의하여 \(\svDash{\alpha }{\Omega}\Delta \implies \alpha < \Omega\) 를 증명하자.

  \(\operatorname{(Ax)}\) 의 경우는 자명하다. ▲

  \((\lor)\) 의 경우 귀납적 가정에 의하여 \(\alpha _0 < \Omega\) 이고, \(\Omega \in \operatorname{Lim}\) 이므로 \(\alpha '_0 < \Omega\) 이다. ▲

  \((\land)\) 의 경우 귀납적 가정에 의하여 모든 \(i \in I\) \(\alpha _i < \Omega\) 이다. \(\Delta\) 가 \(\mathscr{L} _{\Omega}\)-식의 유한 집합이므로 인덱스 집합 \(I\) 는 가산이고, 그러므로 집합 \(\{\alpha _i : i \in I\}\) 도 가산이다. 그러므로 \(\alpha = \sup \{\alpha _i + 1 : i \in I\} < \Omega\) 이다. ▲

  \(\impliedby\):

  \(\svDash{\alpha }{\Omega}\) 의 정의에 의하여 자명하다. ▲

  2:

  건전성, 완전성 정리에 의하여 \(\N \vDash F\) 와 \(\svDash{}{\Omega}F\) 는 동치이고, 이에 따라 1) 에 의하여 바로 나온다. ■

• \(F\) 의 노름을 \(F\) 를 도출할 수 있는 최단 연역 단계로 정의한다. 이로써 진리들의 타당성의 복잡도의 척도를 정의내리는 것이다.

• 자연수 구조 \(\N\) 의 진리를 모두 도출할 수 있는 무한 체계가 완성되었고 그 진리들의 복잡도를 측정할 방법도 마련되었으니 이제 우리가 할 일은 이렇게 유한 언어 \(\mathscr{L}_1\) 를 무한 언어 \(\mathscr{L}_{\infty}\) 로 매장시켜서 \(\mathscr{L}_1\) 에서 다루던 진리를 \(\mathscr{L}_{\infty}\) 에서도 다룰 수 있게 하는 것이다.

• 이 정리가 유한 언어를 무한 언어로 매장시켜도 진리가 보존된다는 것을 보장해준다. 만약 \(\mathscr{L}_1\) 의 타당성이 \(\mathscr{L}_{\infty}\) 에서 훼손된다면 무한 언어를 만든 의미가 없을 것이다.

• 증명

  (\(\mathscr{L}_1\)-식 \(F\) 의 정의에 대한 귀납으로 쉽게 증명된다.)

• 진리의 타당성의 복잡도는 반드시 가산, 즉, \(< \Omega\) 이고, 거짓의 타당성의 복잡도는 반드시 \(\Omega\) 라는 것이다.

• 증명

  \(\implies\):

  \(\N \vDash F\) 이면 보조정리 9.2 에 의하여 \(\svDash{\alpha }{\Omega}F\) 인 \(\alpha < \Omega\) 가 존재한다. 그러므로 \(|F| \leq \alpha < \Omega\) 이다. ▲

  \(\impliedby\):

  \(\N \not \vDash F\) 는 건전성 정리에 의하여 \(\not \svDash{}{\Omega}F\) 를 함의한다. 그러면 보조정리 9.2 에 의하여 \(\left\{ \alpha : \svDash{\alpha }{\Omega}F \right\} = \varnothing\) 이고, \(|F| = \Omega\) 이다. ■

• 이 정리를 첫번째 비가산, 비재귀 서수 \(\omega _{1}^{CK}\) 에 대하여 다음과 같이 더 깎을 수 있다.

  \[ \N \vDash F \iff |F| < \omega _{1}^{CK} \]

  또한, 다음을 증명할 수도 있다.

  \[ \sup \{|F| : \N \vDash F\} = \omega _{1}^{CK} \]

  이 둘의 증명은 재귀 이론의 방법을 사용한다.

• 증명

  (보조정리 9.5, 정리 9.6 에 의한 따름정리이다.)

Infinitary System \(\mathsf{Z}_{\infty}\)✔

이로써 수론의 언어의 \(\Pi_{1}^{1}\)-문장에 대한 노름(타당성의 복잡도의 척도)을 도입했다. 이제 드디어 메인 질문으로 되돌아가자! \(\mathsf{Z}_1\) 에서 증명가능한 \(\Pi_{1}^{1}\)-문장이 갖는 노름은 무엇인가? 이 질문에 답하기 위해 절단 규칙이 없는 연역이 \(\svDash{}{\Omega}\) 로 해석되고, 이로써 연역가능한 식의 노름에 대한 상계를 얻을 수 있는 무한 체계 \(\mathsf{Z}_{\infty}\) 를 도입해야 한다.

• 증명

  (정의 10.1 에서 바로 나온다.)

• 절단규칙 \(\operatorname{(cut)}\) 에서 \(\svdash{\alpha_1}{\rho}\Delta ,A\) 와 \(\svdash{\alpha_2}{\rho}\Delta ,\lnot A\) 형태가 있어도 \(\rho\) 가 너무 작고 \(\operatorname{rk}(A)\) 가 너무 커서 \(\operatorname{rk}(A) \not\in M \cap \rho\) 가 되면, \(\operatorname{(cut)}\) 을 사용할 수 없다. 그러나 \(\rho\) 가 충분히 크면, 어떤 \(A\) 와 \(\lnot A\) 가 오든간에 절단규칙을 사용할 수 있다.

  그러므로 \(\svdash{\alpha}{\rho}\) 의 \(\rho\) 는 쉽게 말해서, 절단규칙을 사용할 수 있는 제한범위를 의미한다. \(\operatorname{(Ax)}\) 에서 \(\rho =0\) 으로 설정하여 \(\svdash{\alpha}{0}\) 으로 추론을 시작하면 절단규칙 \(\operatorname{(cut)}\) 을 아예 사용 못한다.

• \(\operatorname{(Ax)}\) 에서 \(\alpha\) 를 \(M\) 안의 임의의 서수로 정하고 나서, 추론 \((\land)\), \((\lor)\), \(\operatorname{(cut)}\) 을 사용할 때마다 \(\svdash{\alpha}{\rho}\) 의 \(\alpha\) 는 반드시 커진다. 그러나 \(M\) 이 너무 작으면, 가령 \(M = 1 = \{0\}\) 이면, \(\alpha\) 가 커지는 한도가 생긴다. 즉, \(M\) 의 한도에 막혀서 추론을 진행할 수 없는 순간이 온다.

  그러나 \(M\) 이 충분히 커서, 가령 \(M = \operatorname{On}\) 이면, \(\alpha\) 는 한도 없이 커질 수 있다.

• 이 정리는 사실상, 무한 언어의 무한 연역에 의한 타당성 관계 \(\svDash{\alpha }{\Omega}\) 가 무한 체계 \(\svdash{\alpha }{0}\) 와 동치라는 것을 말해준다. \(\svdash{\alpha }{0}\) 의 \(\alpha\) 에 끼여있는 거품만 제거하면 곧바로 \(\svDash{\alpha }{\Omega}\) 로 치환가능하고, 이로써 진리 복잡도를 얻을 수 있다.

• 증명

  (\(\svDash{\alpha }{\Omega}\) 와 \(\mathsf{Z}_M \svdash{\alpha}{0}\) 의 정의에 의하여 정리가 곧바로 성립한다)

• 증명

  (\(\alpha\) 에 대한 귀납으로 쉽게 증명된다.)

• 증명

  (\(\alpha\) 에 대한 귀납으로 증명되며, \(\svdash{\alpha}{\rho}\Delta\) 가 \(\operatorname{(Ax)}\), \((\land)\), \((\lor)\), \(\operatorname{(cut)}\) 에 의하여 도출되었을 경우마다 따져보면 쉽게 증명할 수 있다.)

• 증명

  \(\alpha\) 에 대한 귀납으로 증명된다.

  \(\displaystyle \svdash{\alpha }{\rho}\Delta ,\bigand_{i \in I}^{}A_i\) 가 공리이면 \(\bigand_{i \in I}^{}A_i\) 는 주요식이 될 수 없다. 그러면 모든 \(i \in I\) 에 대한 \(\svdash{\alpha }{\rho}\Delta ,A_i\) 는 같은 종류의 공리이다. ▲

  \(\bigand_{i \in I}^{}A_i\) 가 마지막 추론 \((S)\) 의 주요식이 아니라고 하자. 추론 \((S)\) 는 다음과 같다.

  \[(S) \quad \svdash{\alpha _j}{\rho}\Delta _j, \bigand_{i \in I}^{} \implies \svdash{\alpha }{\rho}\Delta ,\bigand_{i \in I}^{}A_i \]

  그러면 귀납적 가정에 의하여 모든 \(i \in I\) 에 대하여 \(\svdash{\alpha _j}{\rho}\Delta _j, A_i\) 이다. 같은 추론 \((S)\) 에 의하여 모든 \(i \in I\) 에 대하여 \(\svdash{\alpha }{\rho}\Delta ,A_i\) 이다. ▲

  \(\bigand_{i \in I}^{}A_i\) 가 마지막 추론의 주요식인 경우 이 추론은 모든 \(i \in I\) 에 대한 전제 \(\svdash{\alpha _i}{\rho}\Delta _0,A_i\) 들을 갖는 \(\land\)-추론이다. 구조적 규칙에 의하여 \(\svdash{\alpha _i}{\rho}\Delta ,A_i, \bigand_{i \in I}^{}A_i\) 이고 귀납적 가정에 의하여 모든 \(i \in I\) 에 대하여 \(\svdash{\alpha _i}{\rho}\Delta ,A_i\) 이다. 그러면 보조정리 10.5 에 의하여 모든 \(i \in I\) 에 대하여 \(\svdash{\alpha }{\rho}\Delta ,A_i\) 이다. ■

• 증명

  (쉽게 증명된다. 책에 증명이 있다.)

• 증명

  (\(\operatorname{rk}(F_1)\) 에 대한 귀납으로 \(F_1\) 이 공리인 경우, \(\bigand A\) 인 경우를 조사하면 쉽게 증명된다.)

• 정의 3.1 와 같이 정의하는 것이다.

• \(A[t_1, \dots, t_n]\) 는 \(A ^{\Phi }\) 의 자유변수의 할당을 표기하는 방법이다.

• 4) 의 근거는 정리 10.8 의 \(\lor\)-내보내기이다. 5) 에서는 정리 10.7 \(\land\)-역 규칙 때문에 축소가능하다고 하는 것이다.

• 증명

  \(\impliedby\):

  \(\Delta ^{a}\) 가 \(\Delta _0,F_1,F_2\) 이면, 모든 문장 할당에 대하여 \(F_1 ^{\Bbb{B}} = t\) 또는 \(F_2 ^{\Bbb{B}} = t\) 이다. ▲

  \(\implies\):

  \(\Delta ^{a}\) 가 \(\Delta _0,F_1, F_2\) 의 형태가 아니면, \(\Delta ^{a}\) 의 모든 문장적 원자에 진리값 \(f\)(false) 를 할당하는 문장 할당이 존재한다. ■

• 증명

  (자명하다. 증명은 책에 있다.)

• 증명

  \(G(\Delta ^{a})\) 에 대한 귀납으로 증명된다.

  \(G(\Delta ^{a}) = 0\) 이면 \(\Delta\) 는 축소불가능하다. 보조정리 10.13 에 의하여 \(\Delta ^{a}\) 는 쌍대 문장적 원자 \(F_1\) 와 \(F_2\) 에 대한 \(\Delta _0,F_1,F_2\) 의 형태를 갖는다. 항진식 보조정리에 의하여 \(\svdash{2 \operatorname{rk}F_1}{0}\Delta ^{a}\) 이다. \(\operatorname{rk}F_1 \leq \alpha\) 이고 \(\Delta\) 는 \(\lor\)-가져오기에 의하여 \(\Delta ^{a}\) 로부터 얻을 수 있다. 그러므로 \(\svdash{2 + \alpha + m}{0}\Delta\) 인 \(m < \omega\) 이 존재한다. ▲

  (\(G(\Delta ^{a}) > 0\) 인 경우도 쉽게 증명된다.)

• \(\dots \to \dots\) 를 \(\lnot \dots \lor \dots\) 으로 표현한 것이다. 즉, 다음을 표현한 것이다.

  \[ \svdash{\alpha_n}{0}F_x(\underline{0}) \land \bigand _{k<\omega }(F_x(\underline{k}) \to F_x( \underline{k'})) \to F_x( \underline{n}) \]

• 증명

  \(n\) 에 대한 귀납으로 증명된다.

  \(n = 0\) 인 경우 항진식 보조정리에 의하여 \(\svdash{\alpha_0}{0}\lnot F_x(\underline{0}), \lnot \bigand_{k < \omega }^{}(\lnot F_x(\underline{k}) \lor F(\underline{k'})), F_x(\underline{0})\) 가 성립한다. ▲

  (\(n>0\) 인 경우 귀납적 가정으로부터 구조적 추론, 항진식 보조정리, \(\land\)-추론, \(\lor\)-추론을 사용하여 쉽게 증명할 수 있다.)

Embedding of \(\mathsf{Z}_1\) into \(\mathsf{Z}_{\Omega}\)✔

정의 9.4 에서 정의한 \(\mathscr{L}_1\)-식을 \(\mathscr{L} _{\Omega}\)-식으로 보내는 \(^{*}\)-변환은 다음과 같은 성질을 가진다.

• 증명

  식 \(F[x_1, \dots, x_n]\) 의 길이에 대한 귀납으로 증명된다.

  원자식에 대해서는 자명하게 성립한다. ▲

  \(F[x_1, \dots, x_n]\) 이 문장적 원자가 아니면, 귀납적 가정에 의하여 곧바로 결론을 얻을 수 있다. ▲

  \(F[\mathbf{x} ]\) 가 식 \(\forall yG[y, \mathbf{x} ]\) 라고 하자. 임의의 \(n+1\)-튜플 \((l, k_1, \dots, k_n)\) 에 대한 식 \(G[l, \underline{\mathbf{k}}]^{*}\) 은 귀납적 가정에 의하여 유한 랭크 \(m\) 을 갖는 \(\mathscr{L}_{\infty}\)-식이다. 그러면 \(\forall y G[y, \underline{\mathbf{k}}]^{*}\) 은 랭크 \(m+1\) 을 갖는 식 \(\bigand_{l < \omega }^{}G[l, \underline{\mathbf{k}}]^{*}\) 이다. ▲

  \(F[\mathbf{x} ]\) 가 식 \(\exists y G[y, \mathbf{x} ]\) 인 경우도 비슷하게 증명된다. ■

• 다음 증명에서 귀납공리꼴 \(\operatorname{(IND)}\) 에 대한 증명을 보면 \(\operatorname{(IND)}\) 가 존재하므로 \(\mathsf{Z}_{\Omega}\) 안에서의 무한 연역만을 고려해야 한다는 것을 알 수 있다. \(\operatorname{(IND)}\) 가 없어도 된다면, 매장 보조정리는 \(\omega +\omega\) 대신 오직 \(\omega\) 안에서도 성립하며, 이는 유한 연역을 의미한다.

• 증명

  연역 \(\mathsf{Z}_1 \vdash F[x_1, \dots, x_n]\) 의 길이에 대한 귀납으로 증명된다.

  • \(F[x_1, \dots, x_n]\) 이 문장적 공리인 경우:

    \(F[\underline{k_1},\dots ,\underline{k_n}]^{*}\) 는 문장적으로 타당한 식이고 정리 10.16 과 보조정리 11.1 에 의하여 어떤 \(m < \omega\) 에 대하여 \(\svdash{m}{0}F[\underline{k_1},\dots ,\underline{k_n}]^{*}\) 이다. 정리 10.16 의 연역의 길이가 항 \(\underline{k_1}, \dots , \underline{k_n}\) 의 선택에 의존하지 않는다는 것을 조사해야 하지만, 그렇게 하기 귀찮다면 \(m = \omega\) 로 잡고 \(\svdash{\omega}{0}F[\underline{k_1},\dots ,\underline{k_n}]^{*}\) 라고 두어도 본 정리에는 충분하다. ▲

  • \(F[x_1, \dots, x_n]\) 이 식 \(\lnot \forall xA[x_1, \dots, x_n] \lor A_x(t) [ x_1, \dots, x_n]\) 인 경우:

    (이 경우는 \(F\) 가 \(\forall xA \to A_x(t)\) 인 경우이다.)

    n-튜플 \(\underline{\mathbf{k}} = (\underline{k_1},\dots ,\underline{k_n})\) 을 선택하면, \(t _{\mathbf{x} }(\underline{\mathbf{k}})\) 는 닫힌 항 \(t_0\) 이다. \(k := t_0 ^{\N }\) 라고 하자. 항진식 보조정리에 의하여 \(\alpha := 2 \operatorname{rk}(A_x(\underline{k})[\underline{\mathbf{k}}])^{*}<\omega\) 에 대하여 다음이 성립한다.

    \[ \svdash{\alpha}{0}\lnot A_x(\underline{k})[\underline{\mathbf{k}}]^{*},A_x(t)[\underline{\mathbf{k}}]^{*} \]

    추론규칙 \((\lor)\) 에 의하여 다음이 성립한다.

    \[ \svdash{\alpha+1}{0} \lnot \bigand_{k < \omega }^{}A_x(\underline{k})[\underline{\mathbf{k}}]^{*}, A_x(t) [ \underline{\mathbf{k}}]^{*} \]

    \(\lor\)-가져오기에 의하여 다음이 성립한다.

    \[ \svdash{\alpha+3}{0} \lnot \bigand_{k < \omega }^{}A_x(\underline{k})[\underline{\mathbf{k}}]^{*} \lor A_x(t) [ \underline{\mathbf{k}}]^{*} \]

    이는 식 \(F[\underline{\mathbf{k}}]^{*}\) 과 같다. ▲

    \(\svdash{\alpha}{0}(A_x(t) \to \exists xA)^{*}\) 의 경우도 비슷하게 증명된다. ▲

  • 논리적 추론:

    • \(\operatorname{(mp)}\) 추론의 경우:

      귀납적 가정에 의하여 \(\svdash{\alpha_1}{m_1}A ^{*}\) 과 \(\svdash{\alpha_2}{m_2}\lnot A ^{*}\lor B ^{*}\) 를 만족하는 \(\alpha_1,\alpha_2 <\omega +\omega\) 와 \(m_1, m_2 < \omega\) 가 존재한다. 보조정리 10.5 와 구조적 규칙과 \(\lor\)-내보내기에 의하여 \(m := \max \{m_1,m_2,\operatorname{rk}(B ^{*}) + 1\}\) 에 대하여 \(\svdash{\alpha_2}{m}A ^{*},B ^{*}\) 와 \(\svdash{\alpha_2}{m}\lnot A ^{*},B ^{*}\) 를 얻는다. 이제 \(\alpha := \max \{\alpha _1,\alpha _2\} + 1 < \omega + \omega\) 에 대하여 절단 규칙에 의하여 \(\svdash{\alpha}{m}B ^{*}\) 이다. ▲

    • \((\forall)\) 추론의 경우:

      (귀납적 가정으로부터 시작하여 \(\lor\)-내보내기, \((\land)\) 추론 등을 사용하여 쉽게 증명된다.)

  • 동등성 공리:

    (\(\operatorname{(Ax1)}\) 에서 시작하여 \((\land)\) 추론, \(\lor\)-가져오기 등을 사용하여 쉽게 증명된다.)

  • 수학적 공리:

    (나머지 공리는 쉽게 증명된다.)

    귀납 공리 \(\operatorname{(IND)}^{*}\) 가 \(\mathsf{Z}_{\Omega}\) 에서 증명가능하다는 것만 보이자. 보조정리 10.17 귀납 보조정리에 의하여 모든 \(k < \omega\) 와 \(\alpha _k = 2(\operatorname{rk}F_x(\underline{0}) + n)\) 에 대하여 다음을 얻는다.

    \[ \svdash{\alpha_k}{0}\lnot A_x(\underline{0})^{*}, \lnot \forall y( A_x(y) \to A_x( \underline{Sy} ))^{*}, A_x( \underline{k})^{*} \]

    \((\land)\) 추론에 의하여 다음을 얻는다.

    \[ \svdash{\omega }{0}\lnot A_x(\underline{0})^{*}, \lnot \forall y( A_x(y) \to A_x( \underline{Sy} ))^{*}, ( \forall x A)^{*} \]

    그러면 \(\lor\)-가져오기에 의하여 \(\svdash{\omega +3}{0}\operatorname{(IND)}^{*}\) 이다. ■

Cut Elimination for \(\mathsf{Z} _{\Omega}\)✔

• 이 정리가 무한 체계의 무한 연역이 무의미한 연산이 아니라 자연수 구조 \(\N\) 의 진리를 도출해내는 연역임을 보장해준다.

• 증명

  정리 5.3 의 증명과 본질적으로 같다. \(\alpha\) 에 대한 귀납에 절단 규칙에 대한 것만 추가적으로 다루면 된다. 귀납적 가정에 의하여 \(\N \vDash \bigor \{F : F \in \Delta \} \lor A\) 이고 \(\N \vDash \bigor \{F : F \in \Delta \}\lor \lnot A\) 이므로 \(\N \vDash \bigor \{F : F \in \Delta \}\) 를 얻을 수 있다. ■

위 증명에서처럼 \(\svDash{}{\Omega}\) 의 건전성(정리 5.3), 완전성 정리(정리 5.4)에 의하면 체계 \(\mathsf{Z}_{\Omega}\) 에 절단 규칙이 불필요하다는 것을 알 수 있다. \(\mathsf{Z}_{\Omega} \svdash{\alpha}{\rho}F\) 로부터 \(\N \vDash F\) 를 얻을 수 있고, 이로부터 보조정리 9.2 에 의하여 \(\beta =|F|\) 에 대한 \(\svDash{\beta}{\Omega}F\) 를 얻을 수 있다. 그런데 보조정리 10.4 에 의하여 \(\svDash{\beta}{\Omega}\Delta\) 는 \(\svdash{\beta}{0}\Delta\) 를 함의한다. 그러므로 결국 \(\svdash{\alpha}{\rho}F\) 이면 어떤 \(\beta < \Omega\) 에 대하여 \(\svdash{\beta}{0}F\) 이다. 이는 \(\mathsf{Z}_{\Omega}\) 의 절단 규칙이 제거가능함을 보여준다. 따라서 \(\mathsf{Z}_{\Omega}\) 에 대한 절단 제거 정리를 얻을 수 있지만, 서수 \(\beta\) 의 크기에 대한 정보가 그것이 \(F\) 의 노름이라는 정보 말고는 너무 부족하다. 따라서 \(\mathsf{Z}_{\Omega}\) 에 대한 절단 제거 정리를 다른 방식으로 증명하려 한다. 이 증명은 제거 절차를 진행하면서 연역 트리의 길이를 통제하면서 이루어진다. \(\mathsf{Z}_1\) 을 \(\mathsf{Z}_{\Omega}\) 로 매장하는 것은 매장 보조정리(보조정리 11.2)에 의하여 길이가 \(\omega +\omega\) 보다 짧은 유한 절단 랭크의 연역 트리를 만든다. 결과적으로 절단 연역이 제거된 연역 트리는 \(\epsilon_0\) 보다 짧은 길이를 갖게 된다.

• 증명

  \(\alpha \hashtag \beta\) 에 대한 귀납으로 증명된다.

  \(F\) 또는 \(\lnot F\) 가 마지막 추론의 주요식이 아닌 경우:

  대칭성 때문에 \(F\) 의 경우만 고려해도 일반성을 잃지 않을 수 있다.

  \(\svdash{\alpha}{\rho}\Delta ,F\) 가 공리이면 \(\svdash{\alpha}{\rho}\Delta\) 도 공리이고 구조적 규칙과 보조정리 10.5 에 의하여 \(\svdash{\alpha \hashtag \beta }{\rho}\Delta ,\Gamma\) 를 얻는다. ▲

  \(\svdash{\alpha}{\rho}\Delta ,F\) 가 전제들이 \(\svdash{\alpha_i}{\rho}\Delta _i,F\) 인 추론 \(S\) 의 결론이면, 귀납적 가정에 의하여 \(\svdash{\alpha_i \hashtag \beta }{\rho}\Delta _i, \Gamma\) 이다. \(\alpha _i \hashtag \beta < \alpha \hashtag \beta\) 이므로 추론 \(S\) 에 의하여 \(\svdash{\alpha \hashtag \beta }{\rho}\Delta ,\Gamma\) 를 얻는다. ▲

  \(F\) 와 \(\lnot F\) 가 마지막 추론의 주요식인 경우:

  \(\operatorname{rk}(F) = 0\), 즉, \(F\) 가 원자식인 경우. 오직 공리가 주요식이 원자인 추론이므로 \(\svdash{\alpha}{\rho}\Delta ,F\) 와 \(\svdash{\beta}{\rho}\Gamma ,\lnot F\) 는 각각 주요식 \(F\), \(\lnot F\) 를 갖는 공리이다. 그렇다면 \(F\) 는 \(\N \vDash \underline{P}t_1, \dots, t_n\) 인 \(\underline{P}t_1, \dots, t_n\) 의 형태이거나 \(t \in X\) 의 형태인데, 전자라면 \(\lnot F\) 이 \(\N \vDash \lnot \underline{P}t_1, \dots, t_n\) 인 \(\lnot \underline{P}t_1, \dots, t_n\) 이 공리의 주요식이 된다. 이는 모순이다.

  대칭성에 의하여 일반적을 잃지 않고 \(F \equiv t \in X\) 라고 할 수 있다. 그렇다면 \(\Delta\) 는 \(s_1 ^{\N } = t ^{\N }\) 인 식 \(s_1 \not\in X\) 를 포함하고, \(\Gamma\) 는 \(s_2 ^{\N } = t ^{\N }\) 인 식 \(s_2 \in X\) 를 포함한다. 그러면 \(\Delta ,\Gamma\) 는 \(\operatorname{(Ax2)}\) 에 따른 공리이고, 이에 따라 \(\svdash{\alpha \hashtag \beta }{\rho}\Delta ,\Gamma\) 이다. ▲

  \(\operatorname{rk}(F) > 0\) 인 경우. 대칭성에 의하여 어떤 \(v \leq \omega\) 에 대하여 \(F \equiv \bigand_{i < v}^{}F_i\) 라고 할 수 있다. 그러면 다음과 같은 추론을 얻는다.

  1. 모든 \(i<v\) 에 대하여 \(\displaystyle \svdash{\alpha_i}{\rho}\Delta ,F_i \implies \svdash{\alpha_i}{\rho}\Delta ,F_i, \bigand_{i<v}^{}F_i \implies \svdash{\alpha}{\rho}\Delta ,\bigand_{i<v}^{}F_i\)
  2. \(\displaystyle \svdash{\beta_0}{\rho}\Gamma ,\lnot F_{i_0} \implies\svdash{\beta_0}{\rho}\Gamma ,\lnot F_{i_0}, \bigor_{i < v}^{}\lnot F_i \implies \svdash{\beta}{\rho}\Gamma ,\bigor_{i<v}^{}\lnot F_i\)

  그러면 귀납적 가정에 의하여 모든 \(i<v\) 에 대하여 \(\svdash{\alpha_i \hashtag \beta }{\rho}\Delta ,\Gamma ,F_i\) 이고 \(\svdash{\alpha \hashtag \beta _0}{\rho}\Gamma ,\Delta ,\lnot F _{i_0}\) 이다. \(\operatorname{rk}(F _{i_0}) < \operatorname{rk}(F) = \rho\) 이고 \(\alpha _{i_0} \hashtag \beta < \alpha \hashtag \beta\) 이고 \(\alpha \hashtag \beta _0 < \alpha \hashtag \beta\) 이므로 절단 랭크 \(\operatorname{rk}(F _{i_0})<\rho\) 의 \(\operatorname{(cut)}\) 에 의하여 \(\svdash{\alpha \hashtag \beta }{\rho}\Gamma ,\Delta\) 이다. ■

• 즉, \(\svdash{\alpha}{n}\Delta \implies \svdash{2_n(\alpha)}{0}\Delta\) 이다.

• 증명

  \(\alpha\) 에 대한 귀납으로 증명된다.

  마지막 추론이 랭크 \(\rho\) 의 절단 규칙 \(\operatorname{(cut)}\) 이 아닐 경우:

  \(\svdash{\alpha}{\rho+1}\Delta\) 가 공리이거나 \(i < v \leq \omega\) 에 대한 전제 \(\svdash{\alpha_i}{\rho+1}\Delta _i\) 를 갖는 추론이다. 공리의 경우 정의에 의하여 \(\svdash{2 ^\alpha}{\rho}\Delta\) 이고, 후자의 경우 귀납적 가정에 의하여 모든 \(i<v\) 에 대하여 \(\svdash{2^{\alpha_i}}{\rho}\Delta _i\) 를 얻는다. 이 추론이 랭크 \(\rho\) 의 절단 규칙이 아니므로 이 추론이 절단 규칙일 경우 랭크 \(< \rho\) 를 갖는 절단 규칙이다. 그러면 이제 \(\svdash{\alpha_i}{\rho+1}\Delta _i \implies \svdash{\alpha}{\rho +1}\Delta\) 과 같은 추론을 전제 \(\svdash{2^{\alpha_i}}{\rho}\Delta _i\) 에 적용하여 \(\svdash{2^\alpha}{\rho}\Delta\) 를 얻을 수 있다. ▲

  마지막 추론이 랭크 \(\rho\) 의 절단 규칙 \(\operatorname{(cut)}\) 인 경우:

  이 경우 \(\operatorname{rk}(A) = \rho\) 인 주요식 \(A\) 와 전제 \(\svdash{\alpha_1}{\rho+1}\Delta ,A\), \(\svdash{\alpha_2}{\rho+1}\Delta , \lnot A\) 를 얻는다. 그러면, 귀납적 가정에 의하여 \(\svdash{2^{\alpha_1}}{\rho}\Delta ,A\) 와 \(\svdash{2 ^{\alpha_2}}{\rho}\Delta ,\lnot A\) 이고, 제거 보조정리에 의하여 \(\svdash{2 ^{\alpha _1}\hashtag 2 ^{\alpha _2}}{\rho}\Delta\) 이다. \(\alpha _0 := \max \{\alpha _1,\alpha _2\}\) 로 잡으면, \(\alpha _0 < \alpha\) 이고 \(2 ^{\alpha _1}\hashtag 2 ^{\alpha _2} \leq 2 ^{\alpha _0}\hashtag 2 ^{\alpha _0} = 2 ^{\alpha '_0} \leq 2 ^{\alpha }\) 이다. 그러면 보조정리 10.5 에 의하여 \(\svdash{2^\alpha}{\rho}\Delta\) 이다. ■

• 이 정리로 \(\mathsf{Z}_1\) 이 도출하는 진리의 복잡도의 상계가 \(\epsilon_0\) 라는 것을 알 수 있다. 그에 비해 무한 체계는 \(\epsilon_0\) 를 넘어서서도 \(\svdash{(>\epsilon_0)}{0}\) 의 무한 연역을 계속 해내며 자연수 구조 \(\N\) 의 진리를 도출해낼 수 있다.

  그러면 \(\mathsf{Z}_1\) 은 불완전성 때문에 \(\epsilon_0\) 라는 연역의 상계를 가지는 것인가? 아직 이 사실을 더욱 견고하게 만드는 작업을 계속해야 한다.

• 증명

  \(\Pi_{1}^{1}\)-문장 \(F\) 에 대하여 \(\mathsf{Z}_1 \vdash F\) 이면, 보조정리 11.2 매장 보조정리에 의하여 \(\svdash{\alpha}{m}F ^{*}\) 를 만족하는 \(\alpha < \omega \cdot 2\) 와 \(m < \omega\) 가 존재한다. \(2_0(\alpha ) := \alpha, 2 _{n+1}(\alpha ):= 2 ^{2_n(\alpha )}\) 라고 정의하면 정리 12.3 첫번째 제거 정리에 의하여 \(\svdash{2_m(\alpha )}{0}F ^{*}\) 이다. 그런데 \(\omega + \omega < \omega ^{\omega } = \omega _3(0)\) 이고, 이는 모든 \(m < \omega\) 에 대한 \(2_m(\alpha ) < \omega _{3+m}(0)\) 을 함의한다. 가령, \(m=0\) 인 경우 \(\alpha < \omega + \omega = 2_0(\alpha ) < \omega _{3}(0)\) 이고, \(m=1\) 인 경우 \(2 _{1}(\alpha ) < \omega _{4}(0)\) 이고, 이런 식으로 계속된다. 그러므로 \(m\) 이 아무리 커봤자 \(< \omega\) 이므로 \(2_m(\alpha ) < \omega _{\omega }(0) = \epsilon_0\) 이다. ■

• 증명

  (정리 12.4 와 보조정리 10.4 에서 바로 나오는 따름정리이다.)

• \(\operatorname{SP}_{0}\) 를 기본 스펙트럼(basic spectrum)이라고도 한다. SP 는 스펙트럼의 약자, 아랫 첨자 0 은 기본의 의미이다.

• 증명

  (따름정리 12.5 의 결과이다.)

Formalization of Transfinite Induction✔

수론의 언어로 구성된 임의의 언어 \(\mathscr{L}\) 에서 다음의 결과들이 성립한다.

• \(\prec\)-노름은 \(\prec\) 의 길이나 크기의 척도가 되어 준다. \(|n|_{\prec}\) 은 \(\prec\) 의 역의 어떤 원소 \(n\) 의 길이 또는 크기를 말해준다. \(\left\| \prec \right\|\) 은 \(\prec\) 의 역의 모든 원소의 노름의 집합으로써 \(\prec\) 이라는 순서가 지니는 크기 또는 길이, 즉, 순서형을 말해준다.

  가령, \(\prec\) 의 역이 순서를 보존한채로 \(\operatorname{field}(\prec ) = \{7,70,700\}\) 이면 \(7 \prec 70 \prec 700\) 라는 관계를 이루고 있을 것이다. 그러면 \(|70|_{\prec}\) 은 서수 \(|70|_{\prec}=\{|7|_{\prec}\} = 1\) 가 되는 식으로 \(|7|_{\prec},|70|_{\prec},|700|_{\prec}\) 는 각각 서수 \(0,1,2\) 가 된다. \(\left\| \prec \right\|\) 은 서수 \(\left\| \prec \right\| = \{|7|_{\prec}, |70|_{\prec}, |700|_{\prec}\} = 3\) 가 된다.

  다음 정리가 \(|n|_{\prec}\) 과 \(\left\| \prec \right\|\) 이 실제로 서수라는 것을 보장한다.

• 증명

  서수의 추이적 집합은 그 자체로 서수이다.

  \(|n|_{\prec}\) 이 서수의 추이적 집합임을 보이면 된다. 이는 \(\prec\) 을 따른 귀납으로 증명된다.

  \(\alpha \in |n|_{\prec}\) 이면 어떤 \(m \prec n\) 에 대하여 \(\alpha = |m|_{\prec}\) 이다. 그러면 귀납적 가정에 의하여 \(\alpha \in \operatorname{On}\) 이다. 그러므로 \(|n|_{\prec}\) 은 서수 집합이다. \(\beta \in |m|_{\prec}\in |n|_{\prec}\) 이면 어떤 \(m_0 \prec m \prec n\) 에 대하여 \(\beta = |m_0|_{\prec}\) 이다. \(\prec\) 이 추이적이므로 \(m_0 \prec n\) 이고 이는 \(\beta \in |n|_{\prec}\) 을 의미한다. ▲

  한편, 위 증명 자체가 \(\left\| \prec \right\|\) 이 서수 집합임을 증명한다. 그러므로 \(\left\| \prec \right\|\) 이 추이적이라는 것만 보이자. \(\alpha \in \beta \in \left\| \prec \right\|\) 에 대하여 \(\beta = |m|_{\prec}\) 인 \(m \in \operatorname{field}(\prec )\) 이 존재한다. 그러면 어떤 \(m_0 \prec m\) 에 대하여 \(\alpha = |m_0|\) 이고, 이는 \(\alpha \in \left\| \prec \right\|\) 을 의미한다. ■

• 서수 \(|n|_{\prec}\) 과 \(\left\| \prec \right\|\) 의 관계를 알려준다.

• 증명

  (자명하다. 사실 어떤 서수 \(\alpha = \{\beta :\beta <\alpha \}\) 에 대해서도 \(\alpha = \sup \{\beta +1 : \beta \in \alpha \}\) 이다.)

• \(\prec _{\alpha}\) 는 노름이 \(\alpha\) 보다 작은 \(\operatorname{field}(\prec )\) 의 원소 집합이고, 따라서 \(\prec \restriction \alpha\) 는 노름이 \(\alpha\) 보다 작은 원소로 제한된 관계이다.

• 예시

  \(\prec\) 의 역이 순서를 보존한채로 \(\operatorname{field}(\prec ) = \{7,70,700\}\) 이면 \(\prec _{2} = \{7, 70\}\) 이고, \(\prec \restriction 2\) 은 원소들 \(7\) 과 \(70\) 로 제한된 관계가 된다.

• 즉, 노름이 \(\alpha\) 보다 작은 원소로 제한된 관계의 노름은 \(\alpha\) 이다. 사실 이는 서수에서 성립하는 본질적인 성질로써 자명하다.

• 증명

  \(n \in \prec _{\alpha}\) 이면 \(|n|_{\prec}<\alpha\) 이다. 즉, \(\prec \restriction \alpha\) 의 모든 원소의 노름은 \(\alpha\) 보다 작음으로 명백하게 \(\left\| \prec \restriction \alpha \right\| \leq \alpha\) 이다. ▲

  \(\beta <\alpha\) 이면 \(\beta = |m|_{\prec}\) 인 \(m \in \prec _{\alpha}\) 가 존재한다. 즉, \(\alpha\) 보다 작은 서수마다 \(\prec \restriction \alpha\) 에 포함되므로 \(\alpha \leq \left\| \prec \restriction \alpha \right\|\) 이다.

• i.h. 라는 약어는 귀납적 가정을 의미한다.

• \(F_X[S]\) 라는 표기는 \(X\) 에 어떤 할당 \(\Phi\) 에 의하여 \(S\) 를 할당했다는 것이다. \(F[X]\) 라는 표기는 \(F\) 에 자유변수 \(X\) 가 나타났다는 표기이다. \([]\) 라는 표기가 두 가지 의미로 사용된다.

• 증명

  \(\operatorname{rk}(F)\) 에 대한 귀납으로 증명된다.

  \(X\) 가 \(F\) 에서 나타나지 않으면 자명하게 성립한다. ▲

  \(F \equiv t \in X\) 이면 \(\N \vDash F_X[S] \implies t ^{\N } \in S \implies t ^{\N } \in T \implies \N \vDash F_X[T]\) 이다. ▲

  \(F \equiv \bigand_{}^{}\{A_i : i \in I\}\) 이면 \(\N \vDash F_X[S] \implies\) 모든 \(i \in I\) 에 대하여 \(N \vDash A_i \overset{\text{ i.h. }}{\implies}\) 모든 \(i \in I\) 에 대하여 \(\N \vDash A_i[T] \implies \N \vDash F_X[T]\) 이다. ▲

  \(F \equiv \bigor_{}^{}\{A_i : i \in I\}\) 이면 \(\N \vDash F_X[S] \implies\) 어떤 \(i \in I\) 에 대하여 \(N \vDash A_i \overset{\text{ i.h. }}{\implies}\) 어떤 \(i \in I\) 에 대하여 \(\N \vDash A_i[T] \implies \N \vDash F[T]\) 이다. ■

• \(\svdash{\alpha }{0}\) 로 연역된 식 \(\lnot \operatorname{Prog}(\prec ,X), t_1 \not\in X, \dots , t_n \not\in X, \Delta\) 는 다음을 의미한다.

  \[\left( \operatorname{Prog}(\prec ,X) \land t_1 \in X \land \dots \land t_n \in X \right) \to \Delta\]

• 증명

  \(\alpha\) 에 대한 귀납으로 증명된다.

  \(\svdash{\alpha }{0}\) 로 연역된 식이 \(\operatorname{(Ax1)}\) 을 따른 공리인 경우:

  이 경우 \(\Delta\) 는 참인 원자식을 포함한다. 그러므로 \(\N \vDash \bigor \Delta _X[\prec _{\gamma}]\) 이다. ▲

  \(\svdash{\alpha }{0}\) 로 연역된 식이 \(\operatorname{(Ax2)}\) 을 따른 공리의 경우:

  이 경우 \(\Delta\) 는 어떤 \(i \in \{1,\dots ,n\}\) 에 대하여 \(s ^{\N } = t_i ^{\N }\) 인 식 \(s \in X\) 를 포함한다. \(\beta _i = |t_i ^{\N }|_{\prec}\) 이면 \(\beta _i \leq \beta < \gamma\) 이므로 \(\prec _{\gamma}\) 의 정의(정의 13.5)에 의하여 \(\N \vDash (t_i \in X)[\prec _{\gamma}]\) 이다. 그러므로 \(\N \vDash \bigor \Delta _X[\prec _{\gamma}]\) 이다. ▲

  마지막 추론의 주요식이 \(\Delta\) 에 속한 경우:

  이 경우 \(X\)-포지티브 식만을 포함하는 \(\Delta _i\) 에 대한 전제 \(\svdash{\alpha _i}{0}\lnot \operatorname{Prog}(\prec ,X), t_1 \not\in X, \dots ,t_n \not\in X, \Delta _i\) 를 얻는다. 귀납적 가정에 의하여 \(\gamma _i = \beta +2 ^{\alpha _i}\) 에 대하여 \(\N \vDash \bigor \Delta _i[\prec _{\gamma_i}]\) 이다. 단조성 보조정리에 의하여 \(\N \vDash \bigor \Delta _i[\prec _{\gamma}]\) 이고, 모든 추론은 타당성을 보존하므로 \(\N \vDash \bigor \Delta [\prec _{\gamma}]\) 이다. ▲

  마지막 추론의 주요식이 \(\lnot \operatorname{Prog}(\prec ,X)\) 인 경우:

  먼저, \(\lnot \operatorname{Prog}(\prec ,X)\) 은 다음과 같다.

  \[ \lnot \left( \forall x(x \in \operatorname{field}(\prec )\land \forall y(y \prec x \to y \in X) \to x \in X) \right) \iff \]
  \[ \exists x \lnot ( \lnot ( x \in \operatorname{field}(\prec )\land \forall y(y \prec x \to y \in X)) \lor x \in X) \iff \]
  \[ \exists x(x \in \operatorname{field}(\prec )\land \forall y(y \prec x \to y \in X) \land x \not\in X) \]

  그러므로 이 경우 다음과 같은 전제를 얻는다. (이 전제의 \(t \in \operatorname{field}(\prec ) \land \forall y(\lnot y \prec t \lor y \in X) \land t \not\in X\) 에 \(\lor\)-추론을 적용하면 \(\exists \dots\) 을 얻는다.)

  \[ \begin{equation}\begin{split} \svdash{\alpha _0}{0} & \lnot \operatorname{Prog}(\prec ,X), t \in \operatorname{field}(\prec ) \land \forall y(\lnot y \prec t \lor y \in X) \land t \not\in X, \\ & t_1 \not\in X, \dots , t_n \not\in X, \Delta\\ \end{split}\end{equation} \tag*{} \]

  이로부터 정리 10.7 \(\land\)-역 규칙으로 \(\land t \not\in X\) 를 없애면 다음의 \((1)\) 를 얻고, 나머지를 없애면 다음의 \((2)\) 를 얻는다.

  \[ \begin{equation}\begin{split} \svdash{\alpha _0}{0}& \lnot \operatorname{Prog}(\prec ,X), t \in \operatorname{field}(\prec )\land \forall y(\lnot y \prec t \lor y \in X) ,\\ & t_1 \not\in X, \dots , t_n \not\in X, \Delta\\ \end{split}\end{equation} \tag{1} \]
  \[ \svdash{\alpha _0}{0}\lnot \operatorname{Prog}(\prec ,X), t \not \in X, t_1 \not\in X, \dots , t_n \not\in X, \Delta \tag{2} \]

  \(\N \not \vDash \bigor \Delta [\prec _{\gamma}]\) 라고 가정해보자. \((1)\) 에 귀납적 가정을 적용하면 \(\gamma _0 = \beta +2 ^{\alpha _0}\) 에 대하여 다음을 얻는다.

  \[ \N \vDash \bigor \{F:F \in \Delta \} \lor (t \in \operatorname{field}(\prec )\land \forall y(y \prec t \to y \in X))[\prec _{\gamma_0}] \tag{3} \]

  단조성 보조정리에 의하여 \(\N \not \vDash \bigor \Delta [\prec _{\gamma}]\) 는 \(\N \not \vDash \bigor \Delta [\prec _{\gamma_0}]\) 를 의미하고, 그러면 \((3)\) 의 \(\lor\) 의 선행부분이 거짓이 되므로 후행부분이 참이어야 한다. 그러므로 모든 \(y \prec t ^{\N }\) 에 대한 \(y \in \prec _{\gamma_0}\) 을 얻는다. 즉, \(|t ^{\N }| _{\prec}\leq \gamma _0\) 이다.

  \(\beta _0 := \max \{|t ^{\N }|, \beta \}\) 를 정의하면, \(\beta _0 \leq \gamma _0\) 를 얻는다. 이제 \((2)\) 에 귀납적 가정을 적용하면 \(\N \vDash \bigor \Delta [\prec _{\beta_0 + 2 ^{ \alpha _0}}]\) 를 얻는다. 그런데 \(\beta _0 \leq \gamma_0 = \beta +2 ^{\alpha _0}\) 이고 \(2 ^{\alpha _0} + 2 ^{\alpha _0} \leq 2 ^{\alpha }\) 이다. 그러므로 \(\beta _0 + 2 ^{\alpha _0} \leq \beta + 2 ^{\alpha _0} + 2 ^{\alpha _0} \leq \beta + 2 ^{\alpha } = \gamma\) 이고, 단조성 보조정리에 의하여 \(\N \vDash \bigor \Delta [\prec _{\gamma}]\) 이다. 이는 가정이 틀렸음을 보여준다. ■

• 증명

  \(|\operatorname{Fund}(\prec ,X)| \leq \alpha\) 이면 보조정리 10.4 에 의하여 다음이 성립한다.

  \[ \svdash{\alpha }{0} \operatorname{Tran}(\prec )\land (\operatorname{Prog}(\prec ,X) \to \forall x(x \in \operatorname{field}(\prec )\to x \in X)) \]

  \(\land\)-역 규칙에 의하여 다음을 얻는다.

  \[ \svdash{\alpha }{0} \lnot \operatorname{Prog}(\prec ,X) \lor \forall x\in \operatorname{field}(\prec)(x \in X) \]

  \(\lor\)-내보내기에 의하여 다음을 얻는다.

  \[ \svdash{\alpha }{0} \lnot \operatorname{Prog}(\prec ,X) ,\forall x\in \operatorname{field}(\prec)(x \in X) \]

  유계성 보조정리에 의하여 다음을 얻는다.

  \[ \N \vDash \forall x \in \operatorname{field}(\prec )(x \in X)[\prec _{2 ^{\alpha }}] \]

  이는 정의 13.5 에 의하여 다음과 같다.

  \[ \N \vDash \forall x \in \operatorname{field}(\prec )(|x| \leq 2 ^{\alpha }) \]

  그러므로 \(\left\| \prec \right\|\leq 2 ^{\alpha }\) 이다. ■

• 따름정리 13.11 에 의하여, 심지어, 정초성이 \(\mathsf{Z}_1\) 에서 증명가능한 모든 \(\mathscr{L}_1\)-정의가능한 순서 \(\prec\) 이 \(\epsilon_0\) 보다 작은 순서형을 갖는다.

  따름정리 13.11 은 형식 체계의 증명이론적 서수를 더욱 일반적으로 정의할 수 있게 해준다. 즉, 다음과 같이 정의할 수 있다.

  형식 체계 \(T\) 의 증명 이론적 서수는 정초성이 \(T\) 에서 증명가능한 모든 원시 재귀적 정의가능한 순서 관계의 순서형의 최소상계이다.

  따름정리 13.11 은 또한 \(\epsilon_0\) 가 이전의 방식으로 정의된 \(\mathsf{Z}_1\) 의 증명 이론적 서수의 상계라는 것을 말해준다.

Consistency of Systems✔

힐베르트 프로그램과 겐첸의 \(\mathsf{Z}_1\) 에 대한 무모순성 증명에 착안하여 형식 체계 \(T\) 의 증명 이론적 서수를 \(T\) 의 무모순성 증명에 필요한 최소 정렬순서의 순서형으로 정의할 수 있다. 그러나 이 정의는 정렬에 대한 귀납 이외의 방법에 의존하기 때문에 문제가 된다.

\(\epsilon_0\) 가 \(\mathsf{Z}_1\) 의 증명 이론적 서수의 상계라는 것을 확인해야 한다. 이를 위해 정의 8.7 에서 정의한 순서 \(\prec\) 을 따른 초한 귀납 외에는 \(\mathsf{Z}_1\) 에서 형식화될 수 있는 방법만을 사용하는 \(\mathsf{Z}_1\) 의 무모순성 증명을 보여야 한다. \(\prec\) 의 순서형이 \(\epsilon_0\) 이므로 \(\epsilon_0\) 이 \(\mathsf{Z}_1\) 의 증명 이론적 서수의 상계가 된다.

\(\mathsf{Z}_1\) 은 자연수 구조 \(\N\) 을 표준 모델로 가지므로 의미론적으로 무모순이다. 그렇지 않을 경우 정리 3.13 건전성 정리에 의하여 \(\mathsf{Z}_1 \vdash A \land \lnot A\) 가 \(\N \vDash A \land \lnot A\) 를 함의한다.

건정선 정리의 증명은 완전 귀납을 사용했다. 이 귀납은 원시 재귀적으로 정의될 수 있는 순서형 \(\omega\) 의 정렬순서를 따르는 귀납이다. 그러나 \(\mathsf{Z}_1\) 의 증명 이론적 서수를 \(\omega\) 라고 결론 내릴 수 없다. 건전성 정리 증명의 곳곳에 나타나는 \(\omega\) 까지의 귀납 때문에 이 증명은 전혀 유한하지 않다. 또한, 이론이 모델을 가진다는 것으로 무모순성 증명이 완료되었다고 말할 수 없다. 모델을 세우려면 집합론이 필요하므로 이는 수론의 무모순성을 집합론의 무모순성으로 환원시킨 것이다. 실제로 표준 모델 \(\N\) 의 타당성의 개념은 \(\mathsf{Z}_1\) 안에서 형식화할 수 없다. 모델의 타당성 개념을 구축하려면 집합론이 필요하다.

\(T\) 가 모델을 갖는다는 의미론적 무모순성 증명은 애시당초 힐베르트 프로그램에서도 받아들여지지 않았다. 이론 \(T\) 가 어떤 종류의 무한 공리를 포함하면 유한한 방법으로 \(T\) 가 모델을 가진다는 것을 증명할 수 없었기 때문이다. 무한 모델은 유한한 방법으로 구성될 수 없다. 유한한 방법이 무엇인지 정확하게 정의내리는 것은 어렵다. 하지만 \(\Sigma_{1}^{0}\)-식으로 제한된 귀납꼴 \(\operatorname{(IND)}\) 를 갖는 \(\mathsf{Z}_1\) 에서 형식화될 수 있는 증명을 유한하다고 할 수 있다. \(\Sigma_{1}^{0}\)-식은 산술 계층에 따라 양화사가 없는 \(A\) 에 대한 \((\exists x)A\) 의 형태의 식이다. 모델이 산술의 무모순성을 증명한다는 의미론적 무모순성 증명은 \(\mathsf{Z}_0 + \Sigma_{1}^{0}{\text-}\operatorname{IND}\) 안에서 증명될 수 없었다. 괴델의 두번째 불완전성 정리 때문에 이것이 원천적으로 불가능하다는 것이 밝혀졌다.

이런 이유로 수학자들은 무모순성 증명을 의미론적으로 접근하는 것이 아닌 구문론적으로 접근할 필요가 있었다.

• 어떤 체계에서 모든 식을 증명할 수 있으면 그것은 모순된 체계이다.

• \(\lnot A_1 \lor \dots \lor \lnot A_n \lor F\) 은 \((A_1 \land \dots \land A_n) \to F\) 을 의미한다. 즉, 문장적으로 닫혀있는 체계란 문장적으로 타당한 모든 함의 관계를 추론 규칙으로 허용하는 체계이다.

• 증명

  \(\implies\):

  의미론적으로 무모순인 체계는 \(A \land \lnot A\) 형태의 식을 도출하지 않는다. 이는 구문론적 무모순성을 보여준다. ▲

  \(\impliedby\):

  \(T\) 가 의미론적으로 모순적이면 \(T \vdash A \land \lnot A\) 인 식 \(A\) 가 존재한다. \(A \land \lnot A\) 는 의미론적으로 반드시 거짓이므로 모든 식 \(F\) 에 대하여 \(A \land \lnot A \to F\) 는 문장적으로 타당하다. \(T\) 가 문장적으로 닫혀있으므로 이 문장적으로 타당한 식이 유도하는 문장적 추론은 \(T\) 에서 허용된 추론이다. 따라서 결국 \(T \vdash F\) 을 얻는다. 임의의 식 \(F\) 를 증명해낼 수 있으므로 이는 구문론적 모순을 뜻한다. ■

• 증명

  모든 \(\alpha <\epsilon_0\) 와 \(n<\omega\) 에 대하여 \(\not \svdash{\alpha }{n}F\) 이고 랭크가 \(<\omega\) 인 식 \(F\) 가 존재한다는 것을 증명하자.

  \(\N \not \vDash F\) 인 닫힌 원자식 \(F\) 를 잡자.(자연수 구조 \(\N\) 의 타당성 개념을 가져와서 사용하는 증명이 되는 것이 아니다. "\(\N \not \vDash F\) 인 닫힌 원자식 \(F\) 를 잡자" 는 표현을 차라리 "\(0 = 1\) 를 식 \(F\) 라고 하자" 라고 생각하면 의미론의 힘을 빌리는 증명이 아니라는 것을 확신할 수 있을 것이다.) 어떤 \(\alpha <\epsilon_0\) 와 \(n < \omega\) 에 대하여 \(\svdash{\alpha }{n}F\) 라고 해보자. 그러면 제거 정리에 의하여 \(\svdash{2_n(\alpha )}{0}\) 이고 보조정리 10.5 에 의하여 \(\svdash{\omega _n (\alpha) }{0}F\) 을 얻는데 \(\omega _n( \alpha)\) 은 여전히 \(\epsilon_0\) 보다 작다.

  그런데 \(\beta\) 에 대한 귀납으로 \(\svdash{\beta }{0}F\) 일 수 없다는 것을 쉽게 증명할 수 있다. \(F\) 는 공리도 아니고, \(F\) 가 논리적 기호를 포함하게 되기 때문에 \((\land)\) 추론이나 \((\lor)\) 추론으로도 연역해낼 수 없다. ■

• 증명

  \(\lnot A_1 \lor \dots \lor \lnot A_n \lor F\) 가 랭크가 \(\omega\) 보다 작은 문장적으로 타당한 식이면, 정리 10.16 에 의하여

  \[\svdash{\alpha }{0}\lnot A_1, \dots , \lnot A_n, F\]

  을 만족하는 다음과 같은 \(\alpha\) 가 존재한다.

  \[\alpha < 2 \cdot \max \{\operatorname{rk}(A_1), \dots ,\operatorname{rk}(A_2), \operatorname{rk}(F)\} + \omega <\epsilon_0\]

  \(\svdash{\alpha _1}{\delta _1}A_1, \dots ,\svdash{\alpha _n}{\delta _n}A_n\) 인 서수 \(\alpha _1,\dots ,\alpha _n<\epsilon_0\) 와 \(\delta _1,\dots ,\delta _n<\omega\) 가 존재한다고 가정하면, 어떤 \(\beta < \max \{\alpha _1,\dots ,\alpha _n, \alpha \} + \omega < \epsilon_0\) 와 \(\delta := \max \{\delta _1,\dots ,\delta _n, \operatorname{rk}(A_1) + 1, \dots , \operatorname{rk}(A_n) + 1\} < \omega\) 에 대하여 절단에 의하여 \(\svdash{\beta }{\delta }F\) 를 얻는다. ■

• 증명

  (정리 14.5, 보조정리 14.6 에서 바로 나온다.)

• 증명

  \(\mathsf{Z}_1 \vdash A \land \lnot A\) 이면, 보조정리 11.2 매장 보조정리에 의하여 \(n < \omega\) 과 \(\alpha < \omega \cdot 2<\epsilon_0\) 에 대하여 \(\svdash{\alpha}{n}A ^{*}\land \lnot A ^{*}\) 가 성립한다. 보조정리 11.1 에 의하여 \(\operatorname{rk}(A ^{*})<\omega\) 인데, 이는 보조정리 14.7 과 모순이다. ■

이제 질문은 이것이다. 이 무모순성 증명이 건전성 정리를 통한 무모순성 증명에 비해 나을 것이 무엇인가? 이 무모순성 증명은 \(\epsilon_0\) 까지의 초한 귀납을 제외하고는 순전히 유한한 방법만을 사용했다. 유한한 방법은 최소한 \(\Sigma_{1}^{0}{\text-}\operatorname{IND}\), 즉, \(\mathsf{Z}_0 + \Sigma_{1}^{0}{\text-}\operatorname{IND}\) 에서 형식화될 수 있는 방법들을 뜻한다. 겐첸은 비유한한 증명의 방법을 한 점에 집중시켜서 \(\epsilon_0\) 귀납을 사용했다. 그 외의 부분은 모두 유한하여 \(\mathsf{Z}_1\) 에서 형식화될 수 있다.

이 무모순성 증명을 완전히 엄밀하게 형식적으로 증명하려면 귀납꼴 \(\operatorname{TI}(\epsilon_0 ,X)\) 이 추가된 체계 \(\mathsf{Z}_1\) 가 필요하다. 하지만 이것을 엄밀하게 증명하는 것은 번거롭다. 그러므로 무모순성 증명이 체계 \(\mathsf{Z}_1 +\operatorname{TI}(\epsilon_0 ,X)\) 에서 어떻게 형식화되는지 간략하게 살펴보자. 이는 무모순성 증명에서 사용하는 \(\mathsf{Z}_1\) 을 초월하는 방법이 오직 순서형 \(\epsilon_0\) 의 원시 재귀 정렬순서를 따르는 초한 재귀라는 것을 보여준다. 먼저, 매장 보조정리로부터 나온 증명 트리는 재귀 트리이다. 그리고 절단 제거 절차가 트리의 재귀성을 보존한다. 그런데 재귀 트리는 \(\mathsf{Z}_1\) 에서 형식화될 수 있다. 이들 형식화된 연역 트리의 정초성을 보장하기 위해서는 트리의 노드에 서수 코드를 할당해야 한다. 지금까지의 사실은 이 목적을 위해서는 \(\epsilon_0\) 아래의 서수들로도 충분하고, \(\mathsf{Z}_1\) 안의 서수를 정의 8.7 에서 살펴보았다. 그러면 숫자 변수 \(x\) 에 대한 다음과 같은 재귀 함수 \(f\) 를 얻는다.

\(\operatorname{Proof}_{\mathsf{Z}_1 }\) 은 \(\mathsf{Z}_1\) 에 대한 증명 술어이고 \(\left( x \svdash{\alpha}{0}\ulcorner F\urcorner \right)\) 은 다음의 문장의 형식화이다. "\(x\) 는 노드가 \(\mathscr{L} _{\Omega}\)-식과 루트에서 리프로 증가하는 서수에 대한 코드로 라벨링되는 재귀 트리의 인덱스이다. 단, 이 트리는 \(\mathsf{Z}_{\Omega}\) 의 추론 규칙에 대하여 국소적으로 옳고, 리프는 식 \(F ^{*}\) 와 서수 \(\alpha\) 에 대한 코드로 라벨링된다."

이제 다음을 쉽게 얻을 수 있다. 이는 모순을 의미하는 문장 \(0 = 1\) 을 도출하는 연역이 존재하지 않는다, 즉, 무모순성을 뜻한다.

그리고 \((1)\) 로부터 다음을 얻는다.

\((2)\) 와 \((3)\) 에서 최종적으로 다음을 얻고, 이는 \(\mathsf{Z}_1\) 의 구문론적 무모순성을 형식화한다.

이렇게 페아노 산술 \(\mathsf{PA}\), 즉, \(\mathsf{Z}_1\) 의 무모순성을 형식화할 수 있지만, 이러한 논의는 \(\mathsf{Z}_1\) 보다 강한 체계에 대하여 논의할 때 다루어진다.

Wellordering proof in \(\mathsf{Z}_1\)✔

이제 서수 \(< \epsilon_0\) 를 정의 8.7 의 산술화에 의하여 서술하자. 서수들 사이의 동등성과 순서관계가 원시 재귀 관계이기 때문에 이 서수들을 언어 \(\mathscr{L}_1\) 안에서 서술할 수 있다. 그럼에도 표기법은 유지한다. 즉, \(E\) 안의 서수에 대한 코드를 \(\alpha ,\beta ,\dots\) 로 표기하고, 원시 재귀 관계 \(\equiv\) 와 \(\prec\) 을 정의 8.7 에서 정의한 서수의 코드에 의하여 각각 \(\alpha =\beta\) 와 \(\alpha <\beta\) 로 표기한다.

• \(\mathsf{Z}_1\) 안에서 증명가능하다.

• 증명

  \(\alpha \leq \beta\) 인 경우 \(\delta =0,n=1\) 로 잡으면 된다. ▲

  \(\alpha > \beta\) 라고 가정하자. 그러면 \(\alpha =\beta +\alpha _0 < \beta + \omega ^{\mu }\) 인 \(\alpha _0\) 가 존재한다. \(\alpha _0\) 의 칸토어 표준형 \(\alpha _0 = \omega ^{\alpha _1}+\dots +\omega ^{\alpha _k} < \omega ^{\mu }\) 을 잡을 수 있다. 그러면 \(\alpha _1 < \mu\) 이고 \(\alpha _0 < \omega ^{\alpha _1} \cdot (k+1)\) 이다. 그러므로 \(\delta := \alpha _1, n:= k+1\) 로 잡으면 다음이 성립한다.

  \[ \alpha =\beta +\alpha _0 < \beta + \omega ^{\alpha _1} \cdot (k+1) = \beta + \omega ^{\delta } \cdot n \]

  ■

• 증명가능한 식 \(F\) 가 지니고 있는 집합 자유 변수 \(X\) 에 \(\{x:G(x)\}\) 를 입력한 형태의 식도 당연히 증명가능하다.

• 증명

  \(F\) 가 \(\mathsf{Z}_1\) 의 논리적 또는 수학적 공리이면, \(F_X(G)\) 는 같은 종류의 공리이다. ▲

  \(F\) 가 긍정 논법이나 양화 추론에 의하여 연역되었다면, 귀납적 가정에 의하여 정리의 주장을 쉽게 얻을 수 있다. 양화추론의 경우 추론의 고유변수에 대한 조건이 훼손되지 않았다는 것이 보장되어야 하는데, 이는 변수의 이름을 다시 설정하는 것으로 쉽게 해결된다. ■

• 그러면 \(\operatorname{Fund}(\alpha ,X)\) 는 관계 \(\prec \restriction \alpha\) 가 정초되었고 \(\operatorname{TI}(\alpha ,X)\) 는 \(\prec \restriction \alpha\) 가 정렬순서임을 의미한다.

• 정의 8.7 을 따라 정의한 \(\prec\) 은 \(E (=\epsilon_0)\) 에서 정의된 순서관계이다. 그러므로 지금의 목표는 정렬순서 \(\prec\) 의 모든 진 초기 절편을 따른 초한 귀납 \(\operatorname{TI}(\alpha ,X)\) 이 \(\mathsf{Z}_1\) 에서 증명가능하다는 것을 보이는 것이다. \(\mathsf{Z}_1\) 이 \(\operatorname{LO}(\prec )\) 을 증명한다는 것을 보이기는 쉽지만, 번거롭고, 이 증명에서 배울 점은 별로 없다. 그래서 이 증명은 생략하고, 모든 \(\alpha <\epsilon_0\) 에 대한 \(\operatorname{Fund}(\alpha ,X)\) 를 보이자.

  \(\operatorname{Fund}(0, X)\) 은 자명하게 성립하므로 다음 정리를 증명하면 모든 것이 완료된다.

• 이 정리에 의하여 \(\alpha <\epsilon_0 = \omega ^{\omega ^{\rddots }}\) 에 대한 \(\operatorname{Fund}(\alpha ,X)\) 가 \(\mathsf{Z}_1\), 즉, 페아노 산술 \(\mathsf{PA}\) 에서 증명된다는 것이 보장된다.

• 이 정리를 증명하기 위하여 준비가 더 필요하다.

• 이로써 \(\mathsf{Z}_1\) 이 \(\epsilon_0\) 아래의 서수에 대한 정렬순서의 정초성을 증명해낼 수 있다는 것이 밝혀졌다. 이는 \(\mathsf{Z}_1\) 의 증명이론적 서수가 \(\epsilon_0\) 라는 것이다. 이는 증명이론적 서수의 위키의 정의와도 같다.

  위에서 언급했듯이 \(\mathsf{Z}_1\) 이 \(\operatorname{LO}(\prec )\) 을 증명한다는 것을 보이기는 쉽다. 즉, \(\mathsf{Z}_1 \vdash \operatorname{LO}(\prec )\) 이다. 그러므로 이 정리는 모든 \(\alpha <\epsilon_0\) 에 대하여 다음을 의미한다.

  \[ \mathsf{Z}_1 \vdash \operatorname{TI}(\alpha ,X) \]

  그러나 정리 14.8에서 살펴본 \(\mathsf{PA}\), 즉, \(\mathsf{Z}_1\) 의 무모순성 증명은 \(\epsilon_0\) 까지의 초한 귀납을 포함한다. 따라서 \(\mathsf{Z}_1\) 안에서 증명될 수 없고, 괴델의 두번째 불완전성 정리를 위배하지 않는다.

• 증명

  \(\alpha <\epsilon_0\) 이면 \(\alpha <\omega _n(0)\) 인 \(n<\omega\) 가 존재한다. \(\mathsf{Z}_1 \vdash \forall x(\lnot x \prec 0)\) 이므로 \(\mathsf{Z}_1 \vdash \operatorname{Fund}(0, X)\) 이다.

  정리 15.3 을 n번 적용하면 \(\mathsf{Z}_1 \vdash \operatorname{Fund}(\omega _n(0), X)\), 즉, \(\mathsf{Z}_1 \vdash \operatorname{Prog}(\prec ,X) \to \forall x < \omega _n(0) (x \in X)\) 이다. \(\mathsf{Z}_1 \vdash \forall x(x < \alpha \to x<\omega _n(0))\) 이므로 \(\mathsf{Z}_1 \vdash \operatorname{Prog}(\prec ,X) \to \forall x < \alpha (x \in X)\), 즉, \(\mathsf{Z}_1 \vdash \operatorname{Fund}(\alpha ,X)\) 이다. ■

• 증명

  \(\operatorname{Fund}(\alpha ,\operatorname{Sp}(X))\) 는 \(\operatorname{Tran}(\prec ) \land (\operatorname{Prog}(\prec ,\operatorname{Sp}(X)) \to \forall \xi <\alpha (\xi \in \operatorname{Sp}(X)))\) 인데, 표기법에 따라 \(\operatorname{Tran}(\prec ) \land (\operatorname{Prog}(\prec ,X) \to \alpha \subset \operatorname{Sp}(X))\) 가 된다.

  그러므로 다음과 같은 가정으로 \(\omega ^{\alpha }\subset X\) 을 결론내려야 한다.

  \[ \operatorname{Prog}(\prec ,\operatorname{Sp}(X)) \to \alpha \subset \operatorname{Sp}(X) \tag{1} \]
  \[ \operatorname{Prog}(\prec ,X) \tag{2} \]

  \((2)\) 와 보조정리 15.6 에 의하여 다음이 성립한다.

  \[ \operatorname{Prog}(\prec ,\operatorname{Sp}(X)) \tag{3} \]

  \((3)\) 과 \((1)\) 로부터 \(\alpha \subset \operatorname{Sp}_{}(X)\) 을 얻고, 이로부터 \((3)\) 은 \(\alpha \in \operatorname{Sp}(X)\) 을 함의한다. 이제 \(\operatorname{Sp}_{}(X)\) 의 정의에서 \(\xi =0\) 라고 잡으면 \(\omega ^{\alpha }\subset X\) 이다. ■

• 증명

  \(\mathsf{Z}_1 \vdash \operatorname{Fund}(\alpha ,X)\) 이면 보조정리 15.2 에 의하여 \(\mathsf{Z}_1 \vdash \operatorname{Fund}(\alpha ,\operatorname{Sp}(X))\) 이고 보조정리 15.5 에 의하여 \(\mathsf{Z}_1 \vdash \operatorname{Fund}(\omega ^{\alpha} ,X)\) 이다. ■

• 증명

  다음을 가정하자.

  \[ \operatorname{Prog}(\prec ,X) \tag{1} \]

  이로부터 \(\operatorname{Prog}(\prec ,\operatorname{Sp}(X))\), 즉, \(\forall \beta (\beta \subset \operatorname{Sp}(X) \to \beta \in \operatorname{Sp}(X))\) 를 보여야 한다. 이를 위해 임의의 \(\beta\) 를 선택하고 다음을 가정하자.

  \[ \beta \subset \operatorname{Sp}(X) \tag{2} \]

  그리고 \(\beta \in \operatorname{Sp}(X)\), 즉, \(\forall \xi (\xi \subset X \to \xi + \omega ^{\beta } \subset X)\) 을 증명해야 한다.

  다음을 만족하는 어떤 서수(의 코드) \(\xi\) 를 잡자.

  \[ \xi \subset X \tag{3} \]

  \(\xi + \omega ^{\beta }\subset X\) 을 증명해야 한다. \(\eta <\xi +\omega ^{\beta }\) 를 잡자.

  1. \(\beta =0\) 이면 \(\eta \leq \xi\) 이다. \(\eta <\xi\) 이면 \((3)\) 에 의하여 \(\eta \in X\) 이다. \((1)\) 과 \((3)\) 에서 \(\xi \in X\) 가 나온다. \(\xi +1\) 보다 작은 원소가 모두 \(X\) 에 속하므로 \(\xi + 1 \subset X\) 이다.

  2. \(\beta >0\) 이면 보조정리 15.1 에 의하여 \(\eta <\xi +\omega ^{\beta _0} \cdot n\) 인 \(\beta _0<\beta\) 와 \(n < \omega\) 가 존재한다. 다음을 \(n\) 에 대한 귀납으로 보여야 한다.

     \[ \xi +\omega ^{\beta _0}\cdot n \subset X \tag{4} \]

     \(n=0\) 이면 이는 \((3)\) 이다. \(n = n_0'\) 이면 귀납적 가정에 의하여 다음을 얻는다.

     \[ \xi +\omega ^{\beta _0}\cdot n_0 \subset X \tag{5} \]

     \(\beta _0<\beta\) 이므로 \((2)\) 에 의하여 \(\beta _0 \in \operatorname{Sp}(X)\), 즉, \(\forall \xi (\xi \subset X \to \xi + \omega ^{\beta _0}\subset X)\) 이다. 그러므로 특히, \(\xi +\omega ^{\beta _0}\cdot n_0 \subset X \to \xi + \omega ^{\beta _0}\cdot n_0 + \omega ^{\beta _0}\subset X\) 이다.

     그러므로 \((5)\) 와 함께 다음을 얻는다.

     \[ \xi + \omega ^{\beta _0}\cdot n_0' \subset X \tag{6} \]

     그러므로 \(\xi +\omega ^{\beta }\) 보다 작은 \(\eta\) 마다 \(X\) 에 속한다는 것이다.

  이로써 귀납이 끝나고 증명이 끝났다. ■

이로써 정리 15.3 의 증명이 끝났다. 정리 15.3 의 증명의 본질적인 방법은 완전귀납꼴(scheme of complete induction, course of values induction)이다. 완전귀납이란 하나의 가정에서 시작하는 게 아니라 가정의 집합에서 시작하는 귀납으로써 \(P(1)\) 를 증명하고, \(k\) 보다 작은 모든 \(j\) 에 대하여 \(P(j)\) 이 성립한다는 가정 하에 \(P(k)\) 을 증명하여, 모든 \(n \in \N\) 에 대하여 \(P(n)\) 가 성립한다는 귀납법이다.

\(T\) 가 \(\mathsf{Z}_1\) 을 확장하는 임의의 형식 이론이면 정리 15.3 이 모든 정렬순서 \(\prec\) 에 대하여 성립한다. 이 정렬순서의 정의된 식은 \(T\) 에 대한 완전귀납꼴에 의하여 허용되고 15.1 이 \(T\) 안에서 증명가능하다.

• 증명

  (정리 15.4 의 따름정리이다.)

• 즉, \(\epsilon_0\) 보다 작은 어떠한 \(\alpha\) 를 잡아도 \(\mathsf{Z}_1\) 에서 증명할 수 있는 노름이 \(\alpha\) 보다 큰 문장이 존재한다.

• 증명

  \(\alpha <\epsilon_0\) 이면 \(2 ^{\alpha }+1<\epsilon_0\) 이다. 정리 15.4 에 의하여 \(\mathsf{Z}_1 \vdash \operatorname{Fund}(2 ^{\alpha }+1, X)\) 이다. 그런데 정리 13.10 유계성 정리에 의하여 \(\alpha <|\operatorname{Fund}(2 ^{\alpha }+1, X)|\) 이다.

  만약 \(|\operatorname{Fund}(2 ^{\alpha }+1,X)|\leq \alpha\) 이면 유계성 정리에 의하여 \(\left\| \prec \restriction 2 ^{\alpha }+1 \right\|\leq 2 ^{\alpha }\) 이다. \(\prec\) 의 정초성을 \(\operatorname{Fund}\) 식이 보장해주므로 보조정리 13.6 에 의하여 \(\left\| \prec \restriction 2 ^{\alpha }+1 \right\| = 2 ^{\alpha } + 1\) 이다. 따라서 \(2 ^{\alpha }+1 \leq 2 ^{\alpha }\) 가 되어 버린다. ■

\(|\mathsf{Z}_1 | = \epsilon_0\)✔

• 이 정리가 지금까지의 논의의 최종 결론이다. 페아노 산술의 증명의 능력 및 한계는 \(\epsilon_0 = \omega ^{\omega ^{\omega ^{\rddots }}}\) 이다. 괴델의 두번째 불완전성 정리에 의하여 체계는 자신의 무모순성을 스스로 증명해낼 수 없다. 따라서 페아노 산술 \(\mathsf{PA}\) 의 무모순성 증명은 \(\epsilon_0\) 안에서 증명 불가능하다. 실제로 \(\mathsf{Z}_1\) 의 무모순성을 보장해주는 정리 14.8은 \(\epsilon_0\) 까지의 초한 귀납을 포함한다. 그러나 정리 15.4 에 의하여 \(\mathsf{Z}_1\) 은 \(\epsilon_0\) 아래의 초한 귀납들은 증명 및 형식화 할 수 있고, 따름정리 12.5 에 의하여 \(\mathsf{Z}_1\) 에서 증명가능한 문장의 노름은 반드시 \(\epsilon_0\) 보다 작다.

  수리논리학에서 초보적으로 산술의 무모순성 증명을 보이고 단순하게 \(\mathsf{PA}\) 의 증명이론적 강도가 \(\epsilon_0\) 라고 하고 넘어갔는데, 여기서 이렇게 엄밀한 증명을 보인다.

• 증명

  정리 15.8 은 \(\epsilon_0\) 아래의 어떤 서수를 잡아도 그것보다 노름이 큰 증명가능한 문장 \(F\) 가 존재한다는 것을 말해준다. 정리 12.4 에서 노름 \(2 ^{2 ^{2 ^{\rddots }}}\) 을 갖는 문장을 생각했지만, 이것보다도 더 큰 노름을 갖는 문장을 찾을 수 있다는 것이다.

  그러나 정리 12.7 은 \(|\mathsf{Z}_1 | \leq \epsilon_0\) 임을 말해주었다. 이는 페아노 산술 \(\mathsf{PA}\) 의 증명의 강도의 상계를 말해주는 것이었다. 즉, \(\mathsf{Z}_1\) 에서 증명되는 문장의 노름이 아무리 커져도 반드시 \(\epsilon_0\) 보다는 작다. ■

이렇게 산술이 자기 자신의 무모순성을 증명할 수 없고, 상위 체계에 무모순성 증명을 맡겨야 한다는 것을 알아보았고, 산술의 증명의 능력과 한계를 엄밀하게 따져보았다. 그러면 이 모든 것들을 증명해낸 인간의 지능은 얼마나 상위에 있는 체계이고 얼마나 큰 체계인가? 인간의 뇌는 명백히 유한의 영역에 갇혀있는 존재이다. 여기에서 무한에 관한 이야기를 많이 했지만 이 무한들은 분명히 생각의 무한함을 의미하지 않았다. 무한한 생각이 요구되었다면, 인간의 수준에서 이러한 사실들을 밝혀낼 수 없다. 인간이 생각해낼 수 있는 사실들이 유한한 생각으로 도출될 수 있는 한 그것을 인공지능이 모방할 수 있다는 가능성은 열려있다.

인공지능의 끝은 기술 발전의 지능의 기계화이다. 현 시대까지의 기술 발전은 인간이 자연을 관찰하고, 자연으로부터 또는 인위적인 생각의 대상의 기계화로 이루어졌다. 그러므로 가능하다는 가정 하에 인류의 기술 발전의 마침표는 기술 발전을 수행하는 지능의 기계화이다. 하지만 이 마침표를 찍으려는 시도를 불완전성 정리, 튜링의 결정불가능성 정리 등등 많은 수학이 외치고 있는 한계들이 막으려는 것 같다. 그러나 인간의 뇌가 물리적으로 규명될 수 있는 구조를 갖고 있다면 뇌는 어떻게 이 모든 것을 위에서 내려다보며 불완전성과 결정불가능성 정리 등등 까지도 밝혀낼 수 있는가? 물리적으로 규명되면, 수학적으로 표현가능하고, 어떤 언어의 어떤 체계의 어떤 구조로 사상될 수 있다. 자연적 대상이 막상 수학적 대상으로 사상되면, 기계화 할 수 있는 가능성이 유의미하게 높아진다. 최종적으로는 이 모든 것을 포함하는 기계를 만들 수 있는지 여부가 관건이 된다.

그러므로 이 한계들을 보았을 때 이론적으로 인간이 인간과 같은 능력을 갖는 기계를 만들어내었다면 그것으로 충분하다고 보여진다. 체계는 체계 내에 갇혀있고, 기계도 기계 안에 갇혀있으므로 인간도 인간 안에 갇혀있다.

그러나 기계의 한계는 명백하게 스스로 선택할 수 있는 존재가 될 수 없다는 것이다. 반면 인간은 스스로 선택할 수 있는 존재이다. 인간이 스스로 선택할 수 없고 자신의 물리적 형태가 결정된 시점으로부터 모든 생각과 행동과 말들이 미리 정해져있다고 가정하자. 그러면 인간의 자유의지를 어떻게 설명하면 좋을까? 결정불가능성이 자유의지? 그러나 인간은 물리 세계에 독립적으로 선택하는 존재이다. 역사적으로 물리 세계에서의 고통을 개의치 않고 그것들을 거스르는 선택을 해온 인간들이 많다. 만약 인간이 물리 세계에 종속되는 선택을 할 수밖에 없는 존재라면 이러한 세상을 거스르는 선택을 했던 역사 속의 수많은 인간들을 설명할 수가 없다. 기계도 인간처럼 스스로 선택하는, 독립적인 선택을 내릴 수 있는, 최소한 물리 세계에 종속적이지 않은 선택을 내릴 수 있는 존재가 될 수 있는가?