ProofTheory Pohlers

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

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

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

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

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

힐베르트는 증명 이론(proof theory)안에서 무모순성 증명이 수행되어야 한다고 주장했다. 그에 따르면 증명 이론은 내용적인 추론만을 해야 하고, 이로써 의심과 비판에서 벗어나야 하며, 그러므로 오직 유한한(finitistic) 방법만을 사용해야 했다. 유한한 추론이란 유한한 영역 위에서의 조합적인 추론으로 해석된다. 아커만, 폰 노이만, 버네이즈 같은 그의 학생들은 곧바로 성과를 내기 시작했다. 그들은 먼저 기초 산술의 부분체계를 공략했고, 곧이어 완전 귀납꼴을 포함하지 않는 부분 체계에 대한 무모순성 증명을 얻어내었다. 그러나 완전귀납법을 포함하는 체계의 무모순성을 증명하기는 힘들었다.

이 실패는 그들이 부족해서가 아니라 괴델의 불완전성 정리에 의하여 근본적으로 불가능한 시도였음이 밝혀졌다.

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

그러나 괴델의 두번째 불완전성 정리가 힐베르트 프로그램에 치명상을 입혔다. 유한한 방법론은 반드시 수학 내에서 사용가능했기에 이 정리에 의하여 완전귀납꼴을 포함하는 모든 수학의 공리체계의 유한한 무모순성 정리는 존재하지 않는 것이 되기 때문이다.

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

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

1. 겐첸의 증명의 귀납법은 매우 제한된 복잡성의 식만을 필요로 한다. 또한, 그의 무모순성 증명은 배중률을 필요로 하지 않는다. 따라서 매우 낮은 복잡도의 식으로 제한된 귀납꼴에 대한 초한 서수형의 정렬에 대한 귀납꼴을 갖는 직관주의를 기반으로 하는 체계 \(T\) 에서도 형식화될 수 있다. 괴델의 두번째 정리에 의하여 체계 \(T\) 의 증명 이론적 강도는 수론의 그것을 초과했다.(증명 이론적 강도(proof theoretic strength)는 나중에 정의한다.) 그러나 \(T\) 의 귀납법을 제한하여 얻은 부분체계 \(T_0\) 는 오직 수론의 무모순성과 자신의 무모순성의 동치만을 증명할 수 있다. 따라서 겐첸의 증명은 수론의 무모순성을 개념적으로 수론보다 안전하게 여겨지는 \(T_0\) 의 무모순성으로 환원시킬 수 있었다. 이것이 환원적 증명 이론(reductive proof theory)의 예시이다. 환원적 증명 이론에서 이론 \(T_1\) 의 무모순성을 더 다루기 쉬운 \(T_2\) 의 무모순성으로 환원시킬 수 있다.
2. 정렬에 대한 귀납법이 겐첸의 증명에서 유일한 비유한한 방법이다. 여기에서 착안하여 형식 이론 \(T\) 의 증명 이론적 서수를 정의할 수 있다. 이 결과가 서수 분석(ordinal analysis)의 발전으로 이어졌다.

겐첸은 \(\epsilon_0\) 까지의 초한귀납법이 \(\mathsf{PA}\)(페아노 산술) 에서 형식화될 수는 있지만, \(\mathsf{PA}\) 에서 증명될 수는 없다는 것을 보였다. 반면 임의의 \(\alpha < \epsilon_0\) 까지의 초한귀납법은 형식화될 수 있을뿐만 아니라 \(\mathsf{PA}\) 에서 증명도 될 수 있다. 이 결과 자체가 \(\mathsf{PA}\) 의 무모순성을 증명한다. 왜냐하면 만약 수론이 모순적이라면 모든 것이 증명가능하기 때문이다.

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

이제부터 서수 분석의 기초적인 내용을 알아본다. 이로써 지능의 강도와 한계를 밝힐 수 있을까? 그러하다면 체계 내에서 증명 불가능한 사실들을 증명할 방법에 대한 단서를 얻을 수 있다. 이는 도달가능성이 결정불가능한 컴퓨팅 지점으로 도달할 수 있는 방법을 마련할 힌트를 줄 수 있고, 지능을 재귀적으로 발전시킬 수 있는 실마리도 될 수 있다. 지능이 이 모든 체계의 한계를 밝힐 수 있었는데, 지능의 한계는 어떻게 밝혀야 할까? 자기 자신에 대한 생각과 그것의 기계화가 생각의 끝이 될 수 있다.

Primitive Recursive✔

자연수는 \(0\) 부터 시작하는 카운팅으로 볼 수 있다. 그러므로 모든 자연수는 \(0\) 이거나 어떤 자연수의 다음수이다. 이 카운팅 절차가 원시 재귀 함수의 정의의 기초가 된다. 원시 재귀 함수는 자연수 위에서 효과적으로 계산가능한 함수의 부분모임이다.

• 수리논리학에서 정의한 치환 함수와 원시 재귀를 생각하면 이해가 쉽다.

Primitive Recursive Function✔

• 수론적 함수의 정의

• 증명

• 우리에게 익숙한 많은 수론적 함수들이 원시 재귀 함수이다. 원시 재귀 함수 \(F\) 에 대한 다음과 같은 유계 합(bounded summation)도 원시 재귀 함수이다.

  \[ \sum_{i=0}^{0}F(i) = F(0) \qquad \sum_{i=0}^{x+1}F(i) = F(x + 1) + \sum_{i=0}^{x}F(i) \]

  상계 \(x\) 를 갖는 유계 곱 \(\prod_{i=0}^{x}\) 도 원시 재귀 함수이다.

• 주요 원시 재귀 함수의 정의를 참고하자.

• 증명

Primitive Recursive Relation✔

• 유계 양화사의 정의

• 수리논리학 정리 3.18과 같은 정리이다.

• 증명

Coding✔

• \(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\) 은 \(*\) 로도 표기된다.

Course-of-values Recursion✔

• course-of-values 함수는 재귀 함수 \(f(y+1)\) 가 \(f(y)\) 의 값에만 의존하는 것이 아니라 \(u \leq y\) 에 대한 모든 \(f(u)\) 의 값에 의존하는 재귀 함수이다. 실제로 \([F](n+1) = \left< F(0), \dots , F(n) \right>\) 가 된다.

  자연수 \(n+1\) 을 집합 \(\{0, \dots, n\}\) 으로 볼 때, \(F\) 의 \(n+1\) 의 상(image)은 집합 \(F[n+1] = \{F(i) : i \leq n\}\) 이다. 따라서 \(n\) 이하의 \(F\) 의 값의 순서가 중요하지 않을 때 표기 \([F](n)\) 와 \(F[n]\) 을 혼용할 수 있다.

• 증명

  정의에 의하여 \(F\) 가 원시 재귀 함수일 때 \([F]\) 도 원시 재귀 함수이고, \(F(x) = ([F](x + 1))_x\) 이므로 그 역도 성립한다. ■

• 증명

• \(Q\) 가 관계 \(P_1, \dots, P_n\) 에 불 연산, 유계 양화사, 원시 재귀 함수에 대한 치환에 의하여 얻어졌다면, \(Q\) 는 \(P_1, \dots, P_n\) 안에서 원시 재귀이다.

• 증명

Lambda Function✔

• 유계 뮤 연산자와 같은 정의이다.

Ordinals✔

서수는 무한한 대상을 측정하고 무한한 절차를 실행할 때 필요하다.

서수는 유한한 서수(첫째, 둘째, 셋째, ...)를 초한까지 일반화한 개념이다. 자연수는 두 관점에서 볼 수 있다. 하나는 양을 측정하는 기수이다. 이 관점에서 자연수 \(n\) 은 유한집합이 \(n\)개의 원소를 갖는다고 할 수 있다. 또 다른 관점은 카운팅 절차를 나타내는 유한 서수이다. 집합을 카운팅하는 것은 어떤 방식에 의하여 원소의 순서를 정하는 것과 같다.

그러나 유한 집합에서는 기수와 서수 사이에 동형사상이 존재하여 유한 집합의 순서가 유일하므로 이 두 개념의 차이점이 보이지 않는다. 따라서 유한 집합을 카운팅하는 것은 같은 서수와 기수를 도출한다. 그러나 무한집합에서는 다르다. 가령 자연수 집합 \(0,1,\dots\) 을 세는 일반적인 방식을 생각하자. 그리고 \(1,2,\dots\) 를 세고 마지막으로 \(0\) 을 세는 방식을 생각하자. 이 두 방식은 명백하게 서로 동형이 아니다. 왜냐하면 일반적인 방식은 마지막 원소를 갖지 않지만, 후자는 마지막 원소를 갖기 때문이다. 오히려 \(0\) 아래의 절편 \(1,2,\dots\) 이 일반적인 방식과 동형이다. 따라서 후자의 방식이 일반적인 방식보다 하나 더 많은 원소를 갖는다.

이제 일반적인 방식의 \(\N\) 의 순서를 \(\omega\) 라고 하고, 후자의 방식을 \(\omega +1\) 라고 하자. 다음과 같이 순서를 세면 \(\omega +2\) 를 얻는다.

일반적으로 다음과 같은 순서를 \(\omega +n\) 라고 할 수 있다.

다음과 같이 짝수를 먼저 세고 홀수를 세면 \(\omega + \omega\) 를 얻는다.

이들 서수 집합 \(\omega ,\omega +1, \omega +2, \omega +n, \omega + \omega\) 의 기수는 모두 똑같다.

한편, 카운팅이 불가능한 순서도 있다. 가령 음이 아닌 유리수 집합 \(\Bbb{Q}^{+}\) 의 표준 순서를 카운팅한다고 생각하자. 처음에 \(0\) 을 세도 유리수의 조밀성(dense) 때문에 그 다음수가 존재하지 않는다. 그러므로 오직 가산적으로 많은 원소를 가지고 카운팅 되지 않은 나머지 집합이 최소 원소를 가지는 집합만이 카운팅 가능하다. 이러한 순서를 정렬순서(well-ordering)라고 한다.

well-ordering, well-foundedness✔

• 정초 관계에서는 귀납법을 사용할 수 있다. 관계 \((A, \prec )\) 에 대한 귀납은 다음과 같은 꼴이다.

  \[ (\forall x \in A)[(\forall y \prec x) F(y) \implies F(x)] \implies (\forall x \in A)F(x) \tag{3.1} \]

  \(X := \{x \in A : \lnot F(x)\}\) 로 잡았을 때 \((3.1)\) 은 정초성(well-foundedness)과 대우이다. 그러므로 관계의 정초성과 관계에서의 귀납가능성은 동치이다. 또한, 관계의 정초성은 감소하는 열의 유한성과도 동치이다. 즉, 관계 \((A, \prec )\) 가 정초되었다는 것은 무한히 감소하는 열 \(x_0 \succ x_1 \succ \dots \succ x_n \succ x _{n+1} \succ \dots\) 이 존재하지 않는다는 것이다.

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

Transitivity, Ordinal✔

두 순서 \((A_1, \prec _1)\) 와 \((A_2, \prec _2)\) 가 동등하다는 것은 \(A_1\) 에서 \(A_2\) 로 가는 순서 보존 사상이 존재한다는 것이다. 순서 동치류를 순서형(order type)이라고 한다. 카운팅 행위 자체가 집합을 정렬하고, 반대로 정렬된 집합은 카운팅 가능하다. 그러므로 정렬 순서의 동치류를 서수(ordinal)라고 부른다. 가령, 이전에 카운팅했던 \(\omega , \omega +n, \omega +\omega\) 는 서수이고, \(\{0,1,2\}\) 와 \(\{1,2,3\}\) 과 \(\{a,b,c\}\) 사이에는 순서 보존 사상이 존재하므로 둘 다 같은 순서형(순서 동치류)에 속하고, 똑같은 서수 \(3\) 으로 표현된다.

서수 \(\alpha\) 와 \(\beta\) 에 대하여 순서 관계 \(\alpha < \beta\) 를 다음을 만족하는 정렬순서 \((A, \prec _A) \in \alpha\) 와 정렬순서 \((B, \prec _B) \in \beta\) 가 존재한다는 것으로 정의한다.

• \((A, \prec _A)\) 이 \((B, \prec _B)\) 의 진 초기 절편(proper initial segment)과 동형이다. 즉, 다음을 만족하는 원소 \(b \in B\) 가 존재한다.

  • \((A, \prec _A)\) 가 \((B, \prec )\restriction b := (\{x \in B : x \prec _B b\}, \prec _B)\) 와 동형이다.

관계 \(<\) 는 모든 서수 모임 \(\operatorname{On}\) 을 정렬한다. 어떤 서수 \(\alpha \in \operatorname{On}\) 에 대하여 정렬 \((\operatorname{On},<)\restriction \alpha = (\{\xi : \xi<\alpha \}, <)\) 는 \(\alpha\) 를 나타낸다. 그러므로 \((\{\xi:\xi<\alpha \},<)\) 를 \(\alpha\) 의 표준적인 표현으로 선택할 수 있다.

그런데 이 접근은 집합론적 관점에서 문제가 된다. 일반적으로 정렬 순서의 순서형은 집합이 아니라 고유 모임이다. 이 문제를 해결하기 위해 서수를 \(\alpha := \{\xi:\xi<\alpha \}\) 로 정의할 수 있다. 그러면 서수는 집합이 된다. 이 정의를 위하여 서수가 포함 관계 \(\in\) 에 의하여 정렬되는 집합이라는 조건이 필요하다.

이 정의를 받아들이면 많은 기술적인 이점이 생기므로 이 집합론적 서수 정의를 수용하자.

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

• 증명

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

• 이는 \(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✔

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

Transfinite Induction✔

• 증명

  가정이 성립하는데 \(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)의 정의 같은 추가적인 사전지식이 필요하다. 그러나 이 사전지식을 모두 짚고 넘어가려면 집합론에 꽤 딥하게 들어가야만 한다. 따라서 증명을 생략하는 것이 낫다. 엄밀한 증명은 집합론에 대한 전공서적들에서 찾을 수 있다.)

Order-type, Collapsing Function✔

• 순서형 \(\operatorname{otyp}_{\prec}(s)\) 는 러프하게 가령 \(s\) 가 서수 \(0\) 과 순서동형이면

  \[ \operatorname{otyp}_{\prec}(s) = \sup \{\operatorname{otyp}_{\prec}(t) ' : t \prec 0\} = \sup \varnothing = 0 \]

  이고, \(s\) 가 서수 \(1\) 과 순서동형이면

  \[ \begin{align}\begin{split} \operatorname{otyp}_{\prec}(s) &= \sup \{\operatorname{otyp}_{\prec}(t) ' : t \prec 1\} \\ &= \sup \{\operatorname{otyp}_{\prec}(0)'\} = \sup \{1\} = 1 \\ \end{split}\end{align} \tag*{}\]

  이고, \(s\) 가 서수 \(2\) 과 순서동형이면

  \[ \begin{align}\begin{split} \operatorname{otyp}_{\prec}(s) &= \sup \{\operatorname{otyp}_{\prec}(t) ' : t \prec 2\} \\ &= \sup \{\operatorname{otyp}_{\prec}(0)', \operatorname{otyp}_{\prec}(1)'\} = \sup \{1, 2\} = 2 \\ \end{split}\end{align} \tag*{}\]

  가 된다고 생각하면 된다. 가령 정초 이항 관계 \(\prec\) 에서 \(s = \{a, b, c\}\) 라면 \(3\) 과 순서 동형이므로 \(\operatorname{otyp}_{\prec}(s) = 3\) 이 된다.

• 순서형 \(\operatorname{otyp}_{\prec}(s)\) 를 러프하게 \(s\) 와 순서동형인 서수로 생각하면 \(\operatorname{otyp}(\prec )\) 은 \(\operatorname{field}(\prec )\) 에 따라 다음과 같이 된다.

  \[ \begin{align}\begin{split} \operatorname{otyp}(\prec ) &= \sup \{\operatorname{otyp}_{\prec}(s)' : s \in \{0,1,2\}\} \\ &= \sup \{1,2,3\} = 3 \\ \end{split}\end{align} \tag*{} \]
  \[ \begin{align}\begin{split} \operatorname{otyp}(\prec ) &= \sup \{\operatorname{otyp}_{\prec}(s)' : s \in \omega \} \\ &= \sup \{1,2,\dots \} = \sup \omega = \omega \\ \end{split}\end{align} \tag*{} \]
  \[ \begin{align}\begin{split} \operatorname{otyp}(\prec ) &= \sup \{\operatorname{otyp}_{\prec}(s)' : s \in \omega+1 \} \\ &= \sup \{1,2,\dots,\omega +1 \} = \omega +1 \\ \end{split}\end{align} \tag*{} \]

• 증명 이론에서는 개념들이 더욱 추상적으로 정의되므로 선뜻 이해하기 힘들다. 위상 수학에서 정의한 순서형과 NBG 체계에서 정의한 순서형을 참고하자.

• 붕괴 함수는 러프하게 가령 다음과 같이 정의된다.

  \[ \pi _{\prec}(0) = \{\pi _{\prec}(t) : t \prec 0\} = \{\} \]
  \[ \pi _{\prec}(1) = \{\pi _{\prec}(t) : t \prec 1\} = \{\pi _{\prec}(0)\} \]
  \[ \pi _{\prec}(2) = \{\pi _{\prec}(t) : t \prec 2\} = \{\pi _{\prec}(0), \pi _{\prec}(1)\} \]

  순서가 보존된 역 \(\{a,b,c\}\) 에서는 다음과 같이 정의될 것이다.

  \[ \pi _{\prec}(a) = \{\pi _{\prec}(t) : t \prec a\} = \{\} \]
  \[ \pi _{\prec}(b) = \{\pi _{\prec}(t) : t \prec b\} = \{\pi _{\prec}(a)\} \]
  \[ \pi _{\prec}(c) = \{\pi _{\prec}(t) : t \prec c\} = \{\pi _{\prec}(a), \pi _{\prec}(b)\} \]

• 굳이 증명하지 않더라도 위 정의를 보고 직관적으로 정리가 성립한다는 것을 쉽게 알 수 있다.

• 증명

en: Enumerating function✔

• 함수 \(\operatorname{otyp}_{\prec}\) 이 \(\operatorname{field}(\prec )\) 의 원소를 입력하면 그 원소에 대응되는 서수를 출력했다면, \(\operatorname{en}_{\prec}\) 은 반대로 서수를 입력했을 때 그에 대응되는 \(\operatorname{field}(\prec )\) 의 원소를 출력해준다.

  가령, 어떤 정초 관계 \(\prec\) 의 역 \(\operatorname{field}(\prec )\) 이 순서가 보존된 형태로 \(\{a, b, c\}\) 라고 되어 있다면 열거 함수 \(\operatorname{en}_{\prec}\) 는 다음과 같이 된다. 이처럼 \(\operatorname{en}_{\prec}\) 이 정초 관계의 역의 원소를 증가시키며 열거하므로 열거 함수라고 하는 것이다.

  \[ \operatorname{en}_{\prec}(0) = a \]
  \[ \operatorname{en}_{\prec}(1) = b \]
  \[ \operatorname{en}_{\prec}(2) = c \]

• 열거 함수를 이렇게 정의할 수도 있다.

  \[ \begin{equation}\begin{split} f(\alpha ) \simeq g(\alpha ) : \iff &(\alpha \in \operatorname{dom} (f) \cap \operatorname{dom} (g) \land f(\alpha ) = g(\alpha )) \\ & \lor (\alpha \not\in \operatorname{dom} (f) \land \alpha \not\in \operatorname{dom} (g)) \\ \end{split}\end{equation} \tag*{} \]

  에 대한 다음과 같은 부분함수 \(\operatorname{OD}_M:\operatorname{On}\to M\) 를 재귀적으로(초한 재귀) 정의한다.

  \(\operatorname{OD}_M(0) \simeq \min M\)

  \(\operatorname{OD}_M(\alpha ') \simeq \min \{\xi \in M:\operatorname{OD}_M(\alpha )<\xi \}\)

  \(\lambda \in \operatorname{Lim}\) 에 대하여 \(\operatorname{OD}_M(\lambda) \simeq \min \{\xi \in M: \sup \{\operatorname{OD}_M(\eta ) : \eta < \lambda \} \leq \xi \}\)

  이때, \(M \subset \operatorname{On}\) 의 순서형을 \(\operatorname{otyp}(M) := \operatorname{dom} \operatorname{OD}_M\), 즉, \(\operatorname{otyp}(M) := \operatorname{dom} (\operatorname{en}_M)\) 로 정의할 수 있다.

  이제 \(\operatorname{ord}_M := \operatorname{OD}_M \restriction \operatorname{otyp}(M)\) 을 \(M\) 의 열거함수로 정의할 수 있다.

• 증명

  (증명은 보조정리 3.2.10 와 \(\operatorname{otyp}(\prec )\) 과 \(\pi _{\prec}\) 의 정의에 의하여 자명하다.)

• \(M \subseteq \operatorname{On}\) 을 잡으면 \((M, \in )\) 은 정렬 순서이다. 그러므로 순서형, 열거함수 등 이전 정의들이 \((M, \in )\) 에 적용된다.

• 증명

  \(\operatorname{otyp}(M)\) 이 유전적으로 추이적이므로 보조정리 3.2.4 에 의하여 바로 나온다. ■

• 증명

  \(f(\alpha )<\alpha\) 인 \(\alpha \in \operatorname{dom} (f)\) 가 존재하면 그러한 최소 \(\alpha\) 도 존재한다. 그런데 \(\operatorname{dom} (f)\) 이 추이적이므로 \(f(\alpha )\in \operatorname{dom} (f)\) 이고, \(f\) 가 순서 보존 함수이므로 \(f(f(\alpha )) < f(\alpha )\) 이다. 그렇다면 \(f(f(\alpha )) < f(\alpha ) < \alpha\) 이고 이는 \(\alpha\) 의 최소성과 모순이다. ■

• 본 정리의 특수한 경우로, 모임 \(M \subseteq \operatorname{On}\) 에 대하여 항상 \(\alpha \leq \operatorname{en}_M(\alpha )\) 이다.

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}\) 에서 무계이고, 따라서 고유 모임이라는 사실이 알려져있다.

Club✔

• 어떤 \(\alpha < \kappa\) 를 잡았을 때 \(\alpha\) 보다 큰 원소가 \(M \cap \kappa\) 에 존재하지 않으면, \(M\) 이 \(\kappa\) 에 천장을 만들었다, \(M\) 이 \(\kappa\) 의 유계를 이루었다고 할 수 있다. 그러나 그렇지 않으면 본 정의와 같이 \(M\) 이 \(\kappa\) 의 무계이다.

• 즉, 쉽게 말해서 이렇다. \(M \cap \kappa\) 에서 \(\kappa\) 보다 작지만 비어있지 않은 열을 뽑아냈을 때 그 열의 극한이 항상 \(M\) 에 속하면, \(M\) 이 \(\kappa\) 에서 닫혀있다고 한다.

• 예시

  가산 극한 서수 집합은 첫번째 비가산 서수 \(\omega _1\) 에 대하여 클럽 집합이다.

  \(\kappa\) 가 비가산 초기 서수이면 \(\alpha <\kappa\) 인 모든 극한 서수 \(\alpha\) 의 집합은 \(\kappa\) 에서 닫혀있고 무계이다.

  클럽 집합은 정규 함수, 즉, 증가하고 연속하는 함수의 치역(range)에 불과하다. 이 사실을 아래의 정리 3.2.19 에서 증명한다.

Normal Function✔

• 본 정의에는 정규 함수의 두 핵심 요소인 연속과 순증가가 드러나지 않기에 다음과 같은 위키의 정의를 참고하자.

  함수 \(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\) 는 정규함수이다.

• 증명

  \(\implies\):

  \(M\) 이 \(\kappa\)-클럽이라고 하자. 그러면 \(M\) 은 \(\kappa\) 의 무계이고, 이는 \(\operatorname{otyp}(M \cap \kappa ) = \kappa\) 를 의미한다. (서수 모임 \(M \subseteq \operatorname{On}\) 에 대한 순서형 \(\operatorname{otyp}(M)\) 은 보조정리 3.2.12 에서 다뤘다.) 그러므로 \(\kappa \subseteq \operatorname{dom} (\operatorname{en}_M)\) 이다.

  \(\overline{\overline{U}}<\kappa\) 인 \(U \subseteq \operatorname{dom} (\operatorname{en}_M) \cap \kappa\) 을 잡자. 그러면 \(\overline{\overline{\operatorname{en}_M[U]}} = \overline{\overline{U}} < \kappa\) 를 얻는다. \(\kappa\) 가 정칙이므로 \(\sup U < \kappa\) 와 \(\sup (\operatorname{en}_M[U])<\kappa\) 이다. 그러므로 \(\sup (\operatorname{en}_M[U]) = \operatorname{en}_M(\alpha )\) 를 만족하는 \(\alpha <\kappa\) 를 찾을 수 있다.

  \(\xi \in U\) 에 대하여 \(\operatorname{en}_M(\xi ) < \operatorname{en}_M(\alpha)\) 이고 이는 \(\xi <\alpha\) 를 함의한다. 그러므로 \(\sup U \leq \alpha\) 이다. \(\sup U < \alpha\) 라고 가정하자. 그러면 \(\operatorname{en}_M(\sup U) < \operatorname{en}_M(\alpha ) = \sup \operatorname{en}_M[U]\) 이고 \(\operatorname{en}_M(\sup U) < \operatorname{en}_M(\xi )\) 를 만족하는 \(\xi \in U\) 를 얻는다. 그러나 \(\sup U < \xi \in U\) 는 모순이다.

  ▲

  \(\impliedby\):

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

Ordinal Arithmetic✔

Addition✔

• \(\operatorname{On}_{\alpha }\) 가 \(\alpha\) 부터 증가하는 서수 모임이고, \(\operatorname{en}_{\operatorname{On}_{\alpha}}(\xi )\) 가 \(\operatorname{On}_{\alpha}\) 를

  \[ \operatorname{en}_{\operatorname{On}_{\alpha}}(0) = \alpha \]
  \[ \operatorname{en}_{\operatorname{On}_{\alpha}}(1) = \alpha + 1 \]
  \[ \operatorname{en}_{\operatorname{On}_{\alpha}}(2) = \alpha + 2 \]
  \[ \vdots \]

  와 같이 열거하는 함수이므로 서수 덧셈을 \(\operatorname{en}_{\operatorname{On}_{\alpha}}(\xi )\) 로 정의하는 것이다.

• 함수 \(\lambda \xi .\alpha +\xi\) 는 다음 재귀 식을 만족한다.

  \(\alpha +0=\alpha\)

  \(\alpha +\xi '=(\alpha+\xi )'\)

  \(\lambda \in \operatorname{Lim}\) 에 대하여 \(\displaystyle \alpha +\lambda = \sup _{\xi <\lambda }(\alpha +\xi )\)

  이는 자연수 덧셈을 초한까지 확장한 것이다.

• 증명

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

Principal Ordinal✔

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

• 예시

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

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

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

• 증명

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

• 증명

  \(\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 below Epsilon Number✔

• 엡실론 수의 직관적인 정의: 초한서수

• \(\epsilon_0\) 는 \(\Bbb{H}\) 에 속하고, \(\lambda \xi .\omega ^{\xi }\) 에 대하여 닫혀있다.

서수 \(\alpha <\epsilon_0\) 는 \(i = 1, \dots ,n\) 에 대하여 \(\alpha _i < \alpha\) 인 \(\alpha = _{NF} \omega ^{\alpha _1} + \dots + \omega ^{\alpha _n}\) 를 갖는다. 서수 \(\alpha \geq \epsilon_0\) 에 대해서는 \(\alpha_i = \alpha\) 일 수 있다.

즉, 모든 서수 \(< \epsilon_0\) 를 알파벳 \(\{0, +, \omega ^{\cdot }\}\) 에 의한 단어로 표현할 수 있다. 이 단어를 코딩하여, 즉, 자연수로 변환하여 \(\epsilon_0\) 아래의 서수에 대한 자연수 코드를 얻을 수 있다.

즉, 서수 코드의 집합 \(\operatorname{OT}\) 에 대하여 모든 코드 \(a \in \operatorname{OT}\) 에 서수 \(\left| a \right|\) 를 부여하는 함수 \(\left| \right| : \operatorname{OT}\to \operatorname{On}\) 을 다음과 같이 정의할 수 있다.

• 예시

  \(0 \in \operatorname{OT}\) 이므로 \(\left< 0 \right> \in \operatorname{OT}\) 이고 \(\left| \left< 0 \right> \right| = \omega ^{|0|} = \omega ^{0} = 1\) 이다.

  또한, \(\left< 0, 0 \right> \in \operatorname{OT}\) 이고 \(\left| \left< 0,0 \right> \right| = \omega ^{0} + \omega ^{0} = 2\) 이다. 이런 식으로 모든 유한 서수를 표기할 수 있다.

  편의상 \(\left< 0 \right> = 1\) 로 표기하자. 그러면 \(\left< 1 \right> \in \operatorname{OT}\) 이고 \(\left| \left< 1 \right> \right| = \omega ^{|1|} = \omega\) 이다.

  편의상 \(\left< 0, 0 \right> = 2\) 로 표기하자. 그러면 \(\left< 2 \right> \in \operatorname{OT}\) 이고 \(\left| \left< 2 \right> \right| = \omega ^{|2|} = \omega ^{2}\) 이다.

• 증명

  바로 위에서 \(\operatorname{OT}\) 와 \(\prec\) 을 course-of-values 재귀로 동시에 정의했고, 이로써 이 두 개념이 원시 재귀라는 것을 보였다. ▲

  \(\epsilon_0\) 는 \(\Bbb{H}\) 에 속했고 \(\lambda \xi .\omega ^{\xi }\) 에 대하여 닫혀있으므로 \(a\) 에 대한 귀납법으로 쉽게 \(|a|<\epsilon_0\) 를 얻을 수 있다. \(\omega ^{\alpha}\) 들을 아무리 더해도 그 결과는 \(\epsilon_0\) 이하이다. (초한서수에서 \(\epsilon_0\) 를 도출하는 과정을 보면 직관적으로 이해가 된다.)

  역으로 \(\alpha <\epsilon_0\) 에 대한 귀납법으로 \(|a| = \alpha\) 인 \(a \in \operatorname{OT}\) 가 존재한다는 것을 보여야 한다. \(\alpha =0\) 인 경우는 자명하다. \(\alpha \neq 0\) 인 경우 \(i=1,\dots ,n\) 에 대한 \(\alpha _i<\alpha\) 에 대하여 \(\alpha =_{NF}\omega ^{\alpha_1 }+\dots +\omega ^{\alpha _n}\) 를 얻는다. 귀납적 가정에 의하여 \(|a_i| = \alpha _i\) 인 \(a_1,\dots ,a_n \in \operatorname{OT}\) 가 존재한다. 그러면 \(|a _1| \geq |a _2| \geq \dots \geq |a _n|\) 이고, 이는 \(a: = \left< a_1, \dots, a_n \right>\in \operatorname{OT}\) 와 \(|a| = \omega ^{|a_1|}+\dots +\omega ^{|a_n|} = \omega ^{\alpha _1} + \dots + \omega ^{\alpha _n} = \alpha\) 를 함의한다. ■

• 증명

  \(\prec\) 이 정렬 순서이므로 보조정리 3.2.10 에 의하여 모든 \(a \in \operatorname{OT}\) 에 대하여 \(\operatorname{otyp}_{\prec}(a) = \pi _{\prec}(a)\) 이다.

  \(\prec\) 에 대한 귀납법으로 \(\left| a \right| = \pi _{\prec}(a)\) 를 보일 수 있다. 정리 3.3.17 에 의하여 모든 \(a \in \operatorname{OT}\) 에 대한 \(|a|\) 는 서수이므로 \(\left| a \right| = \{\left| b \right| : \left| b \right| < \left| a \right|\} = \{\left| b \right| : b \prec a\} = \{\pi _{\prec}(b) : b \prec a\} = \pi _{\prec}(a)\) 이다. ■

• 조합적 증명

Veblen Hierarchy✔

• 증명

  \(\operatorname{Fix}(f)\) 가 \(\kappa\)-무계임을 보이자. \(\alpha < \kappa\) 를 잡고 \(\beta _0 := \alpha + 1\) 와 \(\beta _{n+1} := f(\beta _n)\) 라고 정의하자.

  그러면 \(f\) 가 정규이므로 \(f\) 의 치역이 \(\kappa\)-무계이고, 어떠한 \(\alpha < \kappa\) 에 대해서도 \(\alpha < \beta \in \operatorname{rng}(f) \cap \kappa\) 가 존재한다. \(f\) 는 순증가하므로 어떠한 \(f(\beta _n)\) 도 \(\kappa\) 를 초과할 수 없다. 그러므로 \(\beta := \sup _{n \in \omega } \beta _n < \kappa\) 이다.

  또한, 정규함수의 조건에 의하여 \(f(\beta ) = f(\sup _{n \in \omega }\beta _n) = \sup _{n \in \omega }f(\beta _n) = \sup _{n \in \omega }\beta _{n+1} = \beta\) 이다. 그러므로 \(\alpha <\beta \in \operatorname{Fix}(f)\cap \kappa\) 이고 \(\operatorname{Fix}(f)\) 는 \(\kappa\) 에서 무계이다. ▲

  \(\operatorname{Fix}(f)\) 가 \(\kappa\) 에서 닫혀있음을 보이기는 쉽다. (책에 증명이 있다.) ■

• 증명

• 증명

Veblen Hierarchy✔

• \(\operatorname{Cr}(0)\) 는 \(\omega ^{\beta }\) 형태의 모든 서수 모임이다. 이 계층에서 베블런 함수는 \(\phi _{0}(\beta ) = \omega ^{\beta }\) 가 된다.

• \(\operatorname{Cr}(1)\) 는 \(\operatorname{Cr}(0)'\), 즉, \(\{\alpha \in \operatorname{Cr}(0) : \operatorname{en}_{\operatorname{Cr}(0)}(\alpha ) = \alpha \}\) 이다. 이는 \(\operatorname{Cr}(0)\) 을 나열했을 때 나열한 인덱스와 \(\operatorname{Cr}(0)\) 의 원소가 같은 것들의 모임이다. 최초의 \(\operatorname{Cr}(1)\) 의 원소는 최초로 \(\omega ^{\alpha } = \alpha\) 를 만족하는 수인 \(\epsilon_0 (= \omega ^{\omega ^{\omega ^{\rddots }}})\) 이다. 이 계층에서 베블런 함수는 \(\phi _{1}(\beta ) = \epsilon _{\beta}\) 가 된다. \(\phi _1(1) = \epsilon_1 = \epsilon_0 ^{\epsilon_0 ^{\epsilon_0 ^{\rddots }}}\) 은 두번째로 \(\omega ^{\alpha } = \alpha\) 를 만족하는 수이다.

• \(\operatorname{Cr}(2)\) 도 같은 방식으로 이해하면 되고, 최초의 \(\operatorname{Cr}(2)\) 의 원소는 초한서수에서 살펴본 것 같이 최초로 \(\epsilon _{\alpha}=\alpha\) 를 만족하는 수 \(\zeta _0= \epsilon _{\epsilon _{\epsilon _{\dots }}}\) 이다. 이 계층에서 베블런 함수는 \(\phi _2(\beta ) = \zeta _{\beta}\) 이다. \(\phi _2(1) = \zeta _1\) 는 두번째로 \(\epsilon _{\alpha}=\alpha\) 를 만족하는 수이다.

• 쉽게 생각해서 그냥 \(\operatorname{Cr}(0)\) 는 \(\omega ^{\beta }\) 형태의 서수 모임, \(\operatorname{Cr}(1)\) 는 \(\epsilon _{\beta }\) 형태의 서수 모임, \(\operatorname{Cr}(2)\) 는 \(\zeta _{\beta }\) 형태의 서수 모임이다.

  함수 \(\phi _{0}(\beta )\) 는 \(\operatorname{Cr}(0)\) 의 원소 \(\omega ^{\beta }\) 를 가져오기 위한 함수, \(\phi _{1}(\beta )\) 는 \(\operatorname{Cr}(1)\) 의 원소 \(\epsilon _{\beta}\) 를 가져오기 위한 함수, \(\phi _{2}(\beta )\) 는 \(\operatorname{Cr}(2)\) 의 원소 \(\zeta _{\beta}\) 를 가져오기 위한 함수이다.

• 증명

  따름정리 3.4.3, 보조정리 3.4.4, 정리 3.2.19 에서 바로 나온다. ■

• 증명

• 증명

• 증명

Critical Ordinal✔

• 여기에서 닫혀있다는 의미는 연산을 반복해도 반드시 \(\beta\) 보다 작다는 의미이다. 그런데 서수에서 \(<\) 는 \(\in\) 으로 이해할 수 있기 때문에 작다는 의미가 닫혀있다는 의미로 이해될 수 있다.

• 초한서수 에서 살펴보았듯이 \(\Gamma _0(= \phi _{\phi _{\phi \dots (0)}(0)}(0))\) 는 베블런 계층 \(\operatorname{Cr}\) 과 베블런 함수 \(\phi\) 자체에 대하여 부동점, 즉, \(\phi _{\Gamma _0}(0) = \Gamma _0\) 이고 최초의 강한 임계 서수이다.

• 증명

  1:

  자명하다.

  2:

  \(a \in \operatorname{SC}\) 는 어떤 \(\xi\) 에 대하여 \(\alpha =\phi _{\alpha}(\xi )\) 를 함의하고, \(\alpha \leq \phi _{\alpha}(0) \leq \phi _{\alpha}(\xi )=\alpha\) 는 \(\alpha =\phi _{\alpha}(0)\) 를 함의한다. 역방향은 자명하다. ■

• 증명

• 증명

Notation System below Gamma Number✔

• \(\epsilon_0\) 아래의 서수에 대한 표기 체계의 핵심이 칸토어 표준형 정리였듯이, \(\Gamma _0\) 아래의 서수에 대한 표기 체계의 핵심이 이 정리이다.

• 증명

보조정리 3.4.17 과 칸토어 표준형에 의하여 \(\Gamma _0\) 아래의 서수 \(\alpha\) 에 대하여

• \(i = 1,\dots ,n\) 에 대하여 \(\xi _i,\eta _i<\alpha\)

를 만족하는 표준형이 다음과 같이 유일하게 결정된다.

즉, 모든 서수 \(< \Gamma _0\) 를 알파벳 \(\{0, +, \phi _{\cdot }(\cdot )\}\) 에 의한 단어로 표현할 수 있다. 그러면 서수 표기의 집합 \(\operatorname{OT}\) 를 다시 정의할 수 있고, 평가 함수 \(||\) 와 함께 주요 서수에 대한 표기의 부분집합 \(\operatorname{PT}\) 을 정의할 수 있다.

• \(\operatorname{OT}\) 는 서수를 표기하기 위한 체계이고, \(\operatorname{PT}\) 는 주요 서수를 표기하기 위한 체계이다.

• 예시

  \(0 \in \operatorname{OT}\) 이므로 \(\left< 2, 0, 0 \right> \in \operatorname{PT}\) 이고 \(\left| \left< 2, 0, 0 \right> \right| = \phi _{\left| 0 \right|}(\left| 0 \right|) = \phi _{0}(0) = \omega ^{0} = 1\) 이다.

  편의상 \(\left< 2, 0, 0 \right>\) 을 \(1\) 로 표기하자. \(1 \in \operatorname{PT}\) 이므로 \(\left< 1, 1 \right> \in \operatorname{OT}\) 이고 \(\left| \left< 1, 1 \right> \right| = |1| = 1\) 이다. 또한, \(\left< 1, 1, 1 \right> \in \operatorname{OT}\) 이고 \(\left| \left< 1, 1, 1 \right> \right| = \left| 1 \right| + \left| 1 \right| = 2\) 이다. 이렇게 모든 유한 서수를 표기할 수 있고, 임의의 유한 서수 \(n\) 의 표기 \(\left< 1, \overbrace{1, \dots , 1}^{n} \right>\) 는 \(\operatorname{OT}\) 에 속한다.

  편의상 유한 서수 \(n\) 의 표기 \(\left< 1, \overbrace{1, \dots , 1}^{n} \right>\) 를 \(n\) 으로 표기하자. 그러면 \(n, m \in \operatorname{OT}\) 에 대하여 \(\left< 2, n, m \right> \in \operatorname{PT}\) 이고 \(\left| \left< 2, n, m \right> \right| = \phi _{|n|}(|m|) = \phi _{n}(m)\) 가 된다.

  이제 다시 이렇게 얻은 주요 서수 표기법으로 \(\omega\) 이상의 서수들의 표준형

  \[ \alpha = _{NF}\phi _{\xi_1}(\eta _1) + \dots + \phi _{\xi_n}(\eta _n) \]

  을 \(\left| \left< 1, a_1, \dots, a_n \right> \right| = \left| a_1 \right| + \dots + \left| a_n \right|\) 와 같이 표기할 수 있게 되는 것이다.

• 증명

Pure Logic✔

수학 연구의 목적은 러프하게 말해서 구조(structure)이다. 수학자의 목적은 그가 관심있는 구조에서 어떤 정리가 성립하는지 밝히는 것이다. 따라서 수학자는 먼저 정리를 형식화할 언어가 필요하다. 이 언어로는 보통 영어와 기술적인 용어들이 사용되지만, 오직 기술적 용어들만이 중요하고 영어는 생략될 수 있다. 핵심적인 요소만 남겨진 형식 언어를 만들 때 다음과 같은 기본 요소가 필요하다.

• 구조를 위한 기호: 상수 기호, 변수 기호
• 함수에 대한 기호
• 항들의 관계를 서술하는 술어 기호(술어 기호가 원시 명제를 형성한다)
• 명제를 합성할 논리 연결사
• 양화사

기본 기호로 다음 두 wf(well-formed) 표현식(expression)을 형성할 수 있다.

• 항(term): 함수 기호에 의하여 상수과 변수로 재귀적으로 형성된다.
• 식(formula): 논리 연결사와 양화사에 의하여 원시 명제로 재귀적으로 형성된다.

구조에 적절한 이렇게 형식 언어를 정의하면 문장(sentence)을 형식화 할 수 있다. 그 다음 문제는 어떤 문장이 구조에서 성립하는지 밝히는 것이다. 이 일은 순전히 직관에 의하여 진행될 수 있다. 그러나 문제는 우리의 직관이 다른 동료들에게는 자명하지 않을 수 있다는 것이다. 따라서 우리는 문장을 증명해야 한다.

그러므로 그 다음의 문제는 증명의 개념을 정의하는 것이다. 우리는 경험적으로 증명이 추론(inference)의 나열로 구성된다는 것을 안다. 그러므로 추론을 특징지어야 한다. 추론은 구조 속에서 진리인 문장들을 보존한다. 문장 \(F\) 가 구조 \(\mathfrak{S}\) 에서 성립한다는 것을 \(\mathfrak{S}\vDash F\) 로 표기하자. \(i = 1, \dots ,n\) 에 대하여 \(\mathfrak{S}\vDash A_i\) 가 \(\mathfrak{S}\vDash F\) 를 함의하면, 추론 \(A_1, \dots, A_n \vDash _{\mathfrak{S}}F\) 가 구조 \(\mathfrak{S}\) 에서 적절하다(adequate)고 한다.

그러나 개별 구조 속의 적절성은 아무런 진전을 주지 못한다. 구조 \(\mathfrak{S}\) 에서 추론 \(A_1, \dots, A_n \vDash _{\mathfrak{S}}F\) 가 적절한 것을 보장하기 위해서는 \(\mathfrak{S}\vDash F\) 를 보장해야 한다. 그러나 이것이 우리가 목표로 하던 것이고, 그러므로 전제 \(A_i\) 에 대한 \(\mathfrak{S}\vDash A_i\) 를 확인하는 것도 완전히 불필요하다.

그러므로 특정 구조들과 독립적일 수 있도록 추론의 개념을 넓혀야 한다. 즉, 가능한 모든 구조에서 적절한 추론을 다뤄야 한다. 다음과 같이 모든 구조에서 진리를 보존하는 논리적 추론(logical inference)을 정의하자.

수리논리학계의 가장 큰 성과 중 하나는 1차 논리 언어에서 논리적 추론 \(\vDash _L\) 의 개념을 형식 규칙(formal rule)의 집합으로 교체할 수 있다는 것을 보인 것이다. 형식 규칙은 형식 언어의 식의 유한 집합 \(F_1, \dots, F_n,G\) 에 대하여 다음과 같은 구문론적 형태로 주어진다.

\(F_1, \dots, F_n \vdash G\) 는 \(F_1, \dots, F_n\) 에서 형식 규칙을 유한번 적용하여 \(G\) 를 연역 할 수 있다는 것을 의미한다. 1차 논리에서 논리적 추론과 연역가능성을 연결하는 정리가 건전성 정리와 완전성 정리이다.

형식 규칙이 구문론적으로 정의되었으므로 형식 규칙이 올바르게 적용되었는지 결정가능하다. 따라서 형식 추론의 유한열이 올바른지도 결정가능하다. 구조 \(\mathfrak{S}\) 에서 자명하게 참인 문장 집합 \(A_1, \dots, A_n\) 에서 \(A_1, \dots, A_n \vdash F\) 를 추론해냈다면, \(\vdash\) 를 \(\vDash _L\) 로 바꾸고 \(\mathfrak{S}\vDash F\), 즉, \(F\) 가 \(\mathfrak{S}\) 의 정리라는 사실을 얻을 수 있다. 이런 증명이 올바르다는 것, 즉, 규칙이 올바르게 적용되었는지도 결정가능하다. 이것이 수학이 널리 사용될 수 있게 하는 매우 중요한 특징이다. 증명된 정리의 진리는 기계적으로 확인가능하고, 이는 특정 소수 집단에서나 존재하던 관례나 규제에 대한 지식으로부터 독립적이다!

물론, 수학자들은 기계적으로, 형식적으로 작업하지 않는다. 수학자는 매우 고도의 직관과 매우 추상적이고 자유로운 사고 공간에서 뛰어놀면서 아이디어를 실험하면서, 증명을 찾는다. 지금까지 수학 공부를 하면서 보아온 증명들은 매우 고도화된 직관 속에서 번뜩이는 아이디어들을 수학의 형식 언어로 재기술한 것이다. 수학자들은 처음부터 수학의 형식 언어를 이리저리 조합하면서 기계처럼 바보같이 증명을 찾지 않는다.

그러나 직관적인 아이디어를 증명으로 적는 과정은 문법적으로 형식화 가능하고, 따라서 결정가능하다. 그렇지 않다면 다른 사람이 증명의 옳음을 검증할 수 없을 것이다.

문장 \(F\) 가 모든 구조에서 참이면 논리적으로 타당하다(logically valid)고 말하고 \(\vDash F\) 라고 표기한다. 논리적 추론의 정의를 따라 문장이 논리적으로 타당한 것은 그 문장을 공집합인 전제 집합에서 도출할 수 있다는 것을 뜻한다. 즉, \(\vDash F \iff \vDash _L F\) 이다. 논리적 추론의 정의에서 곧바로 도출되는 결론 중 하나는 다음과 같은 연역정리이다.

연역 정리에 의해 다음을 얻는다.

논리적 타당성과 논리적 연역가능성은 모든 적합한 구조에 의존하므로 우리는 개별 구조에 대한 정보를 논리적으로는 얻어낼 수 없다. 특정 구조에 대한 어떤 것을 증명하고 싶다면 그 구조의 특성의 기초 사실을 예상해야 하는데, 이 기초 사실이 공리를 이룬다. 그러나 충분히 복잡한 구조에서는 본질적으로 불완전성이 내재되어 있어서 그 구조를 완전히 특정지을 수 있는 공리들을 식별해내는 것은 불가능하다.

이 불완전성은 두 측면을 가진다. 먼저, 동형사상 때문에 1차 논리 공리 집합으로 무한 구조를 특징짓는 것이 불가능하다. 구조 \(\mathfrak{S}\) 에서 참인 모든 문장을 공리로 취해도, 항상 \(\mathfrak{S}\) 와 동형이 아니지만 똑같은 1차 논리 문장을 만족시키는 구조가 존재한다. 이는 1차 논리 문장의 무한 집합 \(M\) 이 구조에서 만족가능한 것은 \(M\) 의 모든 유한 부분집합이 만족가능하다는 것과 동치라고 말하는 1차 논리의 콤팩트성 정리의 결과이다.

완전 2차 논리(full second-order logic)에서는 자연수 구조를 특징짓는 공리 체계가 존재하지만 2차 논리에 대한 완전한 연역 형식화가 존재하지 않는다. 일반적으로 2차 논리에서는 1차 논리에서 성립하던 완전성, 콤팩트성, 스콜렘-뢰벤하임 정리가 성립하지 않는다. 그러므로 2차 논리의 증명의 옳음은 기계적으로 확인 불가능하다. 그러나 2차 논리 언어에서 건정성이 성립하는 형식 계산(formal calculi)는 존재한다. 그런데 논리적 관점에서 이 계산은 2차 논리 계산이 아닌 두 종류의 1차 논리 계산이다.

우리가 수학적 증명의 기계적 검증가능성을 고집한다면, 구조의 모든 타당한 1차 논리 문장을 공리로 채택하면 안된다. 왜냐하면 일반적으로 어떤 문장이 구조에서 타당한지는 결정불가능하기 때문이다. \(A_1, \dots, A_n \vdash F\) 가 올바른 증명인지 검증하려면 \(A_1, \dots, A_n\) 가 공리인지 검증해야 한다. 그러므로 공리는 반드시 결정가능해야 한다. 이때 괴델의 첫번째 불완전성 정리가 나온다. 결정가능한 공리 집합으로부터 구조의 모든 1차 논리 정리를 연역할 수 없다.

결정가능한 공리 체계의 연역가능성의 능력의 한계를 밝히는 것이 지금의 궁극적인 목표이다.

First-Order, Second-Order Logic✔

• 논리언 언어가 있어야 구조를 서술할 수 있다. 논리에 대한 형식 언어에서 논리적 기호와 비논리 기호를 구분해야 한다. 논리적 기호가 모든 언어에서 공통되지만, 비논리 기호는 의도한 구조마다 달라진다.

  가령, 산술에서의 비논리 기호는 \(0\), \('\), \(+\), \(\cdot\), \(=\) 이다.

• 예시

  산술에서의 비논리 기호는 \(0\), \('\), \(+\), \(\cdot\), \(=\) 에서 상수 집합 \(\mathscr{C}\) 의 원소는 \(0\), 관계 기호 집합 \(\mathscr{R}\) 의 원소는 \(=\), 나머지는 함수 기호 집합 \(\mathscr{F}\) 에 속한다.

• \(\operatorname{FV}_{}(F)\) 와 \(\operatorname{BV}_{}(F)\) 는 식 \(F\) 의 자유, 종속 1차 논리 변수 집합이고, \(\operatorname{FV}_{2}(F)\) 와 \(\operatorname{BV}_{2}(F)\) 는 자유, 종속 2차 논리 변수 집합이다.

• 편의상 \(\Phi ^{1}(u)\) 대신 \(\Phi (u)\) 라고 쓰고, \(\Phi _{n}^{2}(U)\) 대신 \(\Phi (U)\) 라고 쓴다. 할당 함수 \(\Phi\) 는 자유변수에 \(S\) 의 원소를 대입해주는 역할을 한다.

• 상수 \(c\) 는 할당 \(\Phi\) 가 필요 없다. 할당은 자유변수를 구체화시키는 역할을 하기 때문이다.

• \(\operatorname{FV}_{}(F) \subseteq \{v_1, \dots, v_n\}\) 를 \(F(v_1, \dots, v_n)\) 라고 표기한다. 그러나 이것이 \(\operatorname{FV}_{}(F) = \{v_1, \dots, v_n\}\) 를 의미하는 것은 아니다. 2차 논리 변수에 대해서도 같은 표기를 사용한다.

• \(\{x_1, \dots, x_n : A _{u_1, \dots, u_n}(x_1, \dots, x_n)\}\) 형태의 모임 항(class term)은 형식 언어의 구성요소가 아니다. 그러나 다음과 같은 형태를 식 \(A _{u_1, \dots, u_n}(t_1, \dots, t_n)\) 로 표기한다.

  \[ (t_1, \dots, t_n) \ein \{x_1, \dots, x_n : A _{u_1, \dots, u_n}(x_1, \dots, x_n)\} \]

• 식 \(F\) 와 \(A\) 에 대하여 \(F\) 에서 나타난 모든 \((U t_1, \dots, t_n)\) 를 \(A _{u_1, \dots, u_n}(t_1, \dots, t_n)\) 로 치환했다는 것을 다음과 같은 식으로 표기한다.

  \[ F_U(\{x_1, \dots, x_n : A _{u_1, \dots, u_n}(x_1, \dots, x_n)\}) \]

  이것을 편의상 \(F_U(A)\) 또는 \(F(A)\) 라고 표기하기도 한다.

• 증명

• 이 연역정리 덕분에 전제에 있는 식에 부정을 붙여서 결론부로 가져올 수 있다. \(A \to B\) 가 \(\lnot A \lor B\) 이기 때문이다. 앞으로 전제에 있는 식에 부정을 붙여서 결론부로 가져오고, 결론부에 있는 식에 부정을 붙여서 전제로 보내는 연산을 자주 사용한다.

• 증명

  정리 4.2.9 에서 바로 나온다. ■

TAIT Calculus✔

\(M \cup \{F\}\) 이 1차 논리식 집합이면 \(M \vDash _LF\) 에 대한 완전하고 건전한 형식 계산(formal calculi) 1차 술어 계산이 존재한다. 한편, 증명 이론적 연구에 적합하게 설계된 계산도 있다.

겐첸은 논리적 추론을 형식화 하기 위해 시퀸트 계산(sequent calculus)을 만들었다. 시퀸트는 1차 논리식 \(A_i\) 와 \(B_j\) 에 대하여 \(A_1, \dots, A_m \vdash B_1, \dots, B_n\) 의 형태를 가진다. 이 시퀸트의 의도된 의미는 \(\{A_1, \dots, A_m\}\vDash _L B_1 \lor \dots \lor B_n\) 이다. \((A_1, \dots, A_m)\) 을 선행자(antecedent)라고 하고 \((B_1, \dots, B_n)\) 를 시퀸트의 후행자(succedent)라고 한다.

겐첸의 주요한 결과는 변화에서 자유로운 건전하고 완전한 시퀸트 계산이 존재한다는 Hauptsatz 이다. 변화에서 자유롭다는 것은 추론의 결론에서 나타나는 모든 식이 그것의 전제에서 나타난다는 것이다. 가령 다음과 같은 절단 규칙은 절단식 \(F\) 를 통한 변화를 결론으로부터 복구할 수 없다.

다음은 시퀸트 계산의 규칙의 예시이다.

(\(\land\)-규칙) \(\dfrac{\Delta ,A \vdash \Gamma }{\Delta ,A \land B \vdash \Gamma } \qquad \dfrac{\Delta _1 \vdash \Gamma _1,A \quad \Delta _2 \vdash \Gamma_2, B}{\Delta _1,\Delta _2 \vdash \Gamma _1, \Gamma _2, A \land B}\)

(\(\lor\)-규칙) \(\dfrac{\Delta _1,A \vdash \Gamma _1 \quad \Delta _2,B \vdash \Gamma_2}{\Delta _1,\Delta _2,(A \lor B) \vdash \Gamma _1, \Gamma _2}\qquad \dfrac{\Delta \vdash \Gamma ,A}{\Delta \vdash \Gamma ,A \lor B}\)

이 예시는 모든 논리적 기호에 대하여 선행자에 대한 추론과 후행자에 대한 추론이 필요하다는 것을 보여준다. 선행자와 후행자는 다음과 같은 부정기호로 연결된다.

• 타이트(W. TAIT)는 기본 명제 연결사에서 부정기호를 제거함으로써 시퀸트에서의 선행자와 후행자의 구별이 없어도 된다는 것을 발견했다. 이로써 추론 규칙의 수를 절반으로 줄일 수 있었다.

  부정을 논리적 기호에 포함시키지 않아도 되는 것은 드모르간의 법칙에 의하여 정의가능하기 때문이다.

• 이 정의에 의하여 임의의 \(\mathcal{L}\)-구조 \(\mathfrak{M}\) 과 임의의 \(\mathfrak{M}\)-할당 \(\Phi\) 와 임의의 \(\mathcal{L}_T\)-식 \(F\) 에 대하여 다음이 성립한다.

  \[ \mathfrak{M}_T \vDash \ssim F[\Phi _T] \iff \mathfrak{M}\vDash \lnot F[\Phi ]\tag{4.3} \]

  따라서 \(\lnot\) 이 \(\mathcal{L}_T\) 의 기본 연결사에 없지만 \(\lnot F\) 과 \(\ssim F\) 를 동일한 것으로 간주하여 사용할 수 있다.

• \(\lnot\) 을 \(\ssim\) 으로 바꿔서 언어 \(\mathcal{L}\) 을 그것의 타이트 언어 \(\mathcal{L}_T\) 로 보내는 변환 \(F \mapsto F ^{T}\) 을 얻을 수 있다. 그러나 보통 \(\mathcal{L}\)-식 \(F\) 와 그것의 타이트 변환 \(F ^{T}\) 을 동일한 것으로 간주하여 사용한다.

• 일반성을 위하여 유한집합 \(\Delta\) 가 붙어있지만, 편의상 \(\Delta =\varnothing\) 으로 두면 이해하기 쉽다.

• 구조적 규칙은 \(m\) 에 대한 귀납법으로 쉽게 증명가능하다.

• 증명

  \(\mathcal{L}\)-구조 \(\mathfrak{M}\) 과 \(\mathfrak{M}\)-할당 \(\Phi\) 를 잡자. 다음을 \(m\) 에 대한 귀납으로 보여야 한다.

  \[ \svdash{m}{\mathsf{T}} \Delta \text{ 이면 }\mathfrak{M}\vDash \bigor \Delta [\Phi ] \text{ 이다 }\tag{1} \]

  \((1)\) 의 가정부가 \(\operatorname{(AxL)}\) 에 의하여 성립하면 \(\Delta\) 는 식 \(A\) 와 \(\ssim A\) 를 포함한다. 그러면 \((4.3)\) 에 의하여 \(\mathfrak{M}\vDash (A \lor \ssim A)[\Phi ]\) 이고 이는 \(\mathfrak{M}\vDash \bigor \Delta [\Phi ]\) 를 함의한다. ▲

  추론 규칙 \((\forall)\) 의 경우만을 살펴보자. 만약 \(\mathfrak{M}\not \vDash (\forall x)A_u(x)[\Phi ]\) 이면 정의 4.2.7 에 의하여 \(\mathfrak{M}\not \vDash A[\Psi ]\) 를 만족하는 할당 \(\Psi \ssim _u \Phi\) 가 존재한다. 추론 규칙 \((\forall)\) 의 가정부 \(\svdash{m_0}{\mathsf{T}}\Delta ,A\) 에 대하여 귀납적 가정에 의하여 \(\mathfrak{M}\vDash (\bigor \Delta \lor A)[\Psi ]\) 가 성립한다. 그러므로 \(\mathfrak{M}\vDash \bigor \Delta [\Psi ]\) 이다. \(u\) 가 \(\Delta\) 에서 나타나지 않으므로 이는 \(\mathfrak{M}\vDash \bigor \Delta [\Phi ]\) 와 동치이다. 그러므로 \(\mathfrak{M}\vDash ( \bigor \Delta \lor (\forall x)A_u(x)) [\Phi ]\) 이다. ▲

  나머지 규칙들도 타당성을 보존한다는 것을 보이면 된다. ■

Tree, Completeness of TAIT✔

• 본 정리를 증명하기 위해서는 Schutte 의 탐색 트리(search 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)}\) 의 증명은 트리 관계에 따른 초한 재귀의 특수한 경우가 된다. ■

• \(s\) 가 리프면 \(\operatorname{otyp}_T(s) = \sup \varnothing = 0\) 이다.

  \(s\) 가 리프 \(s'\) 의 선행자이면 \(\operatorname{otyp}_T(s) = \sup \{\operatorname{otyp}_T(s \concat \left< s' \right>)+1 \}\) 이다. \(\operatorname{otyp}_T(s \concat \left< s' \right>) = \sup \varnothing = 0\) 이므로 \(\operatorname{otyp}_T(s) = \sup \{1 \} = 1\) 이다.

  \(s\) 가 \(s'\) 의 선행자이고, \(s'\) 이 리프 \(s''\) 의 선행자라고 하자. \(\operatorname{otyp}_T(s) = \sup \{\operatorname{otyp}_T(s \concat \left< s' \right>)+1 \}\) 이다. \(\operatorname{otyp}_T(s \concat \left< s' \right>) = \sup \{\operatorname{otyp}_T(s \concat \left< s' \right> \concat \left< s'' \right>) + 1\} = \sup \{0 + 1\} = 1\) 이므로 \(\operatorname{otyp}_T(s) = \sup \{2 \} = 2\) 이다.

  만약, 노드 \(s\) 가 여러 리프로 갈 수 있다면 \(\sup\) 에 의하여 가장 멀리 떨어져있는 리프의 거리로 순서형이 책정될 것이다. 즉, \(s\) 의 순서형 \(\operatorname{otyp}_T(s)\) 는 노드 \(s\) 에서 가장 멀리 떨어져 있는 리프와의 거리이다.

  그러므로 \(\operatorname{otyp}(T) = \operatorname{otyp}_T(\left< \right>)\) 도 루트에서부터 가장 멀리있는 리프까지의 거리라고 이해하면 된다.

• 가령, \(\left< \Delta \right> = \left< A_1, \dots, A_n \right>\) 가 될 것이다.

• 레덱스는 원자식이 아니므로 \(\bigor_{}^{}A\) 나 \(\bigand_{}^{}A\) 나 \((\forall x)A\) 나 \((\exists x)A\) 형태의 식이 된다.

• 탐색 트리는 이진 트리이다. \(S _{\left< \Delta \right>}^{M}\) 가 wf 이면 \(S _{\left< \Delta \right>}^{M}\) 는 쾨니그의 보조정리(Konig’s lemma)에 의하여 유한하고, 그러므로 \(S _{\left< \Delta \right>}^{M}\) 의 모든 노드는 유한 순서형을 가진다.

• 증명

  \(S _{\left< \Delta \right>}^{M}\) 에 대한 선 귀납으로 증명하자.

  \(s\) 가 \(S_{\left<\Delta\right>}^{M}\) 의 리프인 경우:

  \(s\) 가 \(S_{\left<\Delta\right>}^{M}\) 의 리프이면 \((S _{Id})\) 부터 \((S _{\exists })\) 까지의 조항 중 어떤 것도 적용되지 않는다. 그러므로 집합으로 볼 수 있는 \(\delta (s)\) 는 \(\operatorname{(AxL)}\) 에 따른 공리이다. 즉, \(\delta (s)\) 는 \(\Delta ,A,\ssim A\) 의 형태이다. 그러므로 \(\svdash{0}{\mathsf{T}}\delta (s)\) 를 얻을 수 있고 \(\Gamma _s := \varnothing\) 를 선택하면 된다. ▲

  \(\delta (s)\) 가 \(\operatorname{(AxL)}\) 에 따른 공리가 아닌 \(s \in S_{\left<\Delta\right>}^{M}\) 를 가정하자. 즉, 리프가 아닌 \(s\) 를 생각하자.

  \(R(\delta (s)) = \varnothing\) 인 경우:

  \(R(\delta (s)) = \varnothing\) 이면 \(s \concat \left< 0 \right>\in S_{\left<\Delta\right>}^{M}\) 이고 귀납적 가정에 의하여 \(\svdash{\operatorname{otyp}\left( s \concat \left< 0 \right>\right)}{\mathsf{T}}\lnot \Gamma _{s \concat \left< 0 \right>}, \delta (s \concat \left< 0 \right>)\) 를 만족하는 유한집합 \(\Gamma _{s \concat \left< 0 \right>}\) 가 존재한다. 그런데 \(\delta (s \concat \left< 0 \right>) = \delta (s)\) 이거나 어떤 식 \(G_i \in M\) 에 대하여 \(\delta (s \concat \left< 0 \right>) = \delta (s), \lnot G_i\) 이다. 그러므로 전자의 경우 \(\Gamma _s:=\Gamma _{ s \concat \left< 0 \right>}\) 로 잡고, 후자의 경우 \(\Gamma _s := \Gamma _{s \concat \left< 0 \right>}\cup \{G_i\}\) 로 잡으면 \(\svdash{\operatorname{otyp}\left( s \right)}{\mathsf{T}}\lnot \Gamma _{s}, \delta (s )\) 를 얻는다. ▲

  \(R(\delta (s)) \neq \varnothing\) 인 경우 \(R(\delta (s))\) 의 형태에 따라 경우가 나뉜다.

  \(R(\delta (s))\) 가 식 \(A_0 \land A_1\) 인 경우:

  \(i = 0, 1\) 에 대하여 \(s \concat \left< i \right> \in S_{\left<\Delta\right>}^{M}\) 이고, 귀납적 가정에 의하여 \(\delta (s \concat \left< i \right>) = \delta (s)^{r}, A_i\) 에 대하여 \(\svdash{\operatorname{otyp}\left( s \concat \left< i \right> \right)}{\mathsf{T}}\lnot \Gamma _{s \concat \left< i \right>}, \delta (s \concat \left< i \right>)\) 이다. 그러면 이 두 관계에 추론 규칙 \(\operatorname{(STR)}\) 과 \((\land)\) 을 적용하여 \(\Gamma _s:=\Gamma _{s \concat \left< 0 \right>}\cup \Gamma _{s \concat \left< 1 \right>}\) 에 대한 \(\svdash{\operatorname{otyp}(s)}{\mathsf{T}}\lnot \Gamma _s, \delta (s)\) 을 얻는다. ▲

  \(R(\delta (s))\) 가 식 \((\forall x) A_v(x)\) 인 경우:

  \(s \concat \left< 0 \right>\in S_{\left<\Delta\right>}^{M}\) 이고 귀납적 가정에 의하여 \(u\) 가 나타나지 않는 \(\delta (s)\) 와 \(\Gamma _{s \concat \left< 0 \right>}(\subseteq M)\) 에 대하여 \(\svdash{\operatorname{otyp}\left( s \concat \left< 0 \right> \right)}{\mathsf{T}}\lnot \Gamma _{s \concat \left< 0 \right>},\delta (s)^{r}, A_v(u)\) 를 얻는다. \(\Gamma _s:=\Gamma _{s \concat \left< 0 \right>}\) 로 잡으면 \((\forall)\) 에 의하여 \(\svdash{\operatorname{otyp}(s)}{\mathsf{T}}\lnot \Gamma _s, \delta (s)\) 이다. ▲

  \(R(\delta (s))\) 가 식 \(A_0 \lor A_1\) 인 경우:

  \(s \concat \left< 0 \right> \in S_{\left<\Delta\right>}^{M}\) 이고 귀납적 가정에 의하여 어떤 \(i \in \{0,1\}\) 와 어떤 식 \(G_j \in M\) 에 대하여 \(\svdash{\operatorname{otyp}\left( s \concat \left< 0 \right> \right)}{\mathsf{T}}\lnot \Gamma _{s \concat \left< 0 \right>}, \delta (s), \lnot G_j\) 또는 \(\svdash{\operatorname{otyp}\left( s \concat \left< 0 \right> \right)}{\mathsf{T}}\lnot \Gamma _{s \concat \left< 0 \right>}, \delta (s), A_i, \lnot G_j\) 이다. \(\Gamma _s:=\Gamma _{s \concat \left< 0 \right>}\cup \{G_j\}\) 로 두자. 전자의 경우 \(\operatorname{(STR)}\) 에 의하여 \(\svdash{\operatorname{otyp}(s)}{\mathsf{T}}\lnot \Gamma _s, \delta (s)\) 이다. 후자의 경우 \((\lor)\) 를 사용하여 \(A_0 \lor A_1\) 를 만들면 \(\delta (s)\) 로 흡수되어 \(\svdash{\operatorname{otyp}(s)}{\mathsf{T}}\lnot \Gamma _s, \delta (s)\) 를 얻는다. ▲

  \(R(\delta (s))\) 가 식 \((\exists x) A_v(x)\) 인 경우:

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

  ■

• 증명

• 증명

  가산 \(M\), 유한 \(\Delta\) 를 잡자. 모든 \(m \in \omega\) 와 모든 유한 부분집합 \(\Gamma \subseteq M\) 에 대하여 다음과 같이 가정하자.

  \[\not \svdash{m}{\mathsf{T}}\lnot \Gamma ,\Delta\]

  그러면 \(S _{\left< \Delta \right>}^{M}\) 은 구문론적 주요 보조정리에 의하여 wf 가 아니다. 그러면 의미론적 주요 보조정리에 의하여 \(\mathfrak{M}\vDash M[\Phi ]\) 이지만 \(\mathfrak{M}\not \vDash \bigor \Delta [\Phi ]\) 인 모델 \(\mathfrak{M}\) 과 \(\mathfrak{M}\)-할당 \(\Phi\) 를 찾을 수 있다. 그러므로 \(M \not \vDash _L \bigor \Delta\) 이다. 이는 모순이다. ■

• 이것은 건전성과 완전성 정리를 조합한 정리이다.

• 정리 4.4.1 에서 \(M = \varnothing\) 으로 두면 정리 4.4.1 는 유한 집합 \(\Delta\) 에 대하여 \(\vDash _L \bigor \Delta\) 일 때 \(\svdash{m}{\mathsf{T}}\Delta\) 를 만족하는 \(m \in \omega\) 가 존재한다는 것이 된다.

  정리 4.3.3 는 정확히 이것의 역을 주장한다. 그러므로 다음이 성립한다.

  \[ \vDash _L \bigor \Delta \iff \svdash{m}{\mathsf{T}}\Delta \]

• 즉, 어떤 \(m \in \omega\) 에 대하여 다음이 성립한다.

  \[ \vDash F \iff \svdash{m}{\mathsf{T}}F \]

• 증명

  \(M= \varnothing\) 와 \(\Delta =\{F\}\) 로 잡고 정리 4.4.6 을 적용하면 된다. ■

• 동등성이 없는 순수 술어 논리를 전개하여 사용했지만, 이제 항상 언어가 동등 기호 \(=\) 를 갖고, 언어 \(\mathcal{L} = \mathcal{L} (\mathscr{C} ,\mathscr{F} ,\mathscr{R} )\) 에서 형식화된 모든 이론이 \(=\) 에 대하여 정의된 공리를 갖는다고 가정하자.

• \(\svdash{m}{\mathsf{T}}\lnot A_1,\dots ,\lnot A_n,\Delta\) 를 만족하는 동등성 공리를 포함하는 \(T\) 의 유한한 공리 \(A_1, \dots, A_n\) 가 존재한다는 것을 \(T \svdash{m}{\mathsf{T}}\Delta\) 라고 표기하자.

• 증명

  \(M \vDash _LF\) 이면 정리 4.4.6 에 의하여 유한 부분집합 \(N \subseteq M\) 에 대하여 \(\svdash{m}{\mathsf{T}}\lnot N, F\) 이다. 그러면 정리 4.3.3 에 의하여 \(\vDash \bigor \lnot N,F\) 이다. 이제 정리 4.2.10 에 의하여 \(N \vDash _L F\) 이다. ■

• 정리 4.2.9 를 사용하여 본 콤팩트성 정리를 익숙한 보통의 콤팩트성 정리로 변환할 수 있다.

  이론 \(T \cup \{\lnot F\}\) 가 모델을 갖지 않는다. \(\iff\)

  \(T \vDash _LF \iff\)

  어떤 유한 집합 \(N \subseteq T\) 에 대하여 \(N \vDash _LF \iff\)

  \(N \cup \{\lnot F\}\) 가 모델을 갖지 않는 유한 부분집합 \(N \subseteq T\) 가 존재한다.

  이제 참인 문장 \(F\) 를 선택하고 위의 대우를 취하면 된다.

• 비가산 이론에서도 콤팩트성은 성립한다. 그러나 증명을 조금 수정해야 한다.

Hauptsatz for First-Order Logic✔

• 1차 논리 타이트 계산의 완전성 정리의 한 결과가 절단 규칙에 대한 허용가능성이다.

• 증명

  타이트 계산의 건전성에 의하여 임의의 모델의 임의의 할당에서 \(\bigor \Delta \lor F\) 와 \(\bigand \Delta \lor \lnot F\) 가 타당하다. 그러면 임의의 모델의 임의의 할당에서 \(\bigor \Delta\) 가 타당해야 한다. 그러면 타이트 계산의 완전성에 의해 \(\svdash{k}{\mathsf{T}}\bigor \Delta\) 를 만족하는 \(k\) 가 존재한다. 그러면 \(k\) 에 대한 귀납법으로 \(\svdash{k}{\mathsf{T}}\Delta\) 임을 쉽게 보일 수 있다. ■

• 순수 논리에서는 정리 4.5.1 만 있으면 되지만 무한 체계에서는 본 정리가 필요하다.

• 증명

  (준형식 계산(semi-formal calculus)에 대한 절단 제거(cut-elimination)를 정의한 다음에야 증명 가능하다)

• 1951년에 Schutte 가 Reduktionssatz를 보였다.

Second-Order Logic✔

2차 논리는 완전하지 않다. 이는 2차 논리에서 산술에 대한 범주적 공리 체계(categorical axiom system)이 존재하기 때문이다. 공리 체계가 범주적이라는 것은 그것에 대하여 본질적으로 구별되는 표현이 유일하게 존재한다는 것이다. 공리 체계가 범주적이 아니라는 한 예시는 다음 4가지 공리로 표현되는 기하학이다.

1. 점 5개가 존재한다.
2. 각 선은 5개의 점의 부분집합이다.
3. 선 2개가 존재한다.
4. 각 선은 최소한 2개의 점을 포함한다.

이 공리 체계는 다음과 같은 근본적으로 다른 두 모델을 갖는다. 한 모델은 교집합을 갖지만 다른 모델은 갖지 않으므로 이 두 모델은 근본적으로 다르며, 동형이 아니다.

1. 각각 두 점을 포함하는 두 서로소 선(disjoin line)과 어느 선에도 있지 않은 점.
2. 한 점에서 겹치는 세 점을 포함하는 두 선.

그러나 산술에 대한 2차 논리 공리 체계 \(\mathsf{PA}^{2}\) 는 \(\N\) 에 대하여 범주적이다(문제 7.1.1). 즉, \(\mathsf{PA}^{2}\) 의 모든 모델은 자연수의 표준 구조 \(\N\) 과 동형이다.

공리 체계 \(T\) 와 새로운 상수 \(c\) 를 잡자. 그러면 모든 유한 부분집합 \(T' := T \cup \{c \neq \underline{n} : n \in \N \}\) 은 모델을 갖는다. 이러한 모델로는 그냥 \(T\) 의 모델 \(\N\) 을 잡고, 새로운 상수 \(c\) 는 유한 부분집합에서 나타나는 모든 \(\underline{n}^{\N }\) 과 다른 자연수로 해석하면 된다. 2차 논리에서 콤팩트성 정리가 성립하면 모델 \(n \in \N\) 에 대하여 \(c ^{\mathcal{N}}\neq \underline{n}^{\N } = n\) 이 성립하여 \(\N\) 과 동형이 아닌 2차 논리 모델 \(\mathcal{N}\vDash T'\) 을 얻는다. 이는 모순이다. 그런데 이전에 살펴보았듯이 완전성 정리가 콤팩트성 정리를 함의하므로 2차 논리에서 완전성은 성립할 수 없다.

그러나 2차 논리에서 건전성이 성립하는 계산은 존재한다.

• 증명

• 이러한 2차 논리 계산은 매우 약한 형태이다. 보통은 더 강한 계산이 고려된다.