AxiomaticSetTheory

NBG Axiom System✔

20세기 초에 집합론에 모순이 발견됨으로써 집합론의 모순과 직관적으로 여겨져서 엄밀한 정의를 보류해왔던 개념들을 제거해야 했다. 이에 따라 다양한 집합론이 제시되었는데 이들이 얼마나 다르든, 이들은 모두 공통적인 근본 이론을 가졌다.

폰 노이만(von Neumann)이 최초로 제시(1925, 1928)하고 이후에 로빈슨(1937)과 버네이즈(Bernays)(1937-1954)와 괴델(Godel)(1940)이 개정한 체계인 1차 이론 NBG 를 다루자. NBG 는 단일 술어 기호 \(A _{2}^{2}\) 를 갖고 함수 기호나 개별 상수는 갖지 않는다. 그리고 \(A _{2}^{2}(x, y)\) 를 \(x \in y\) 로 축약하고, \(\neg A _{2}^{2}(x, y)\) 를 \(x \not\in y\) 로 축약하자.

괴델의 표기법을 따라서 변수를 \(X_1, X_2, \dots\) 와 \(X, Y, Z\) 로 표기하자.

• 두 모임은 같은 멤버를 가질 때 서로 같다.

• \(X \subseteq Y\) 일 때 \(X\) 를 \(Y\) 의 부분모임(subclass)라고 한다. \(X \subset Y\) 일 때 \(X\) 를 \(Y\) 의 진부분모임(proper subclass)라고 한다.

• 증명

Set, Proper Class✔

• 즉, 어떤 모임이 다른 모임에 속하면 집합이라고 한다. 그렇지 않은 모임를 고유 모임이라고 한다.

• 이제 이로써 이전의 집합론에서 발생했던 모순들이 더 이상 모순이 아니라 단지 다양한 클래스가 집합이 아니라 고유 모임임을 말해준다는 사실을 알게 된다.

• 체계 NBG 는 개별 개체를 다루는 것이 아니라 오직 모임만을 다루도록 설계되었다. 왜냐하면 수학 자체가 개별 대상을 다룰 필요 없이 모임에 대하여서만 형식화될 수 있기 때문이다. 모임이 아닌 대상을 다루는 과학을 다룰 때 수학이 응용되어야 한다면 NBG 를 약간 변형하여 모임과 비모임 개체에 적용되는 체계를 사용해야 한다. 가령 체계 UR 이 있다.

  모임이 아닌 개별 개체를 허용한다면 동등성의 정의가 달라져야 한다. 모든 개별 개체는 아무것도 없는 똑같은 원소를 갖기 때문이다.

• 이제 소문자 \(x_1, x_2, \dots\) 와 \(x, y , z\) 를 집합에 대한 변수로써 사용한다.

  \((\forall x_j)B(x_j)\) 는 다음을 의미한다. 즉, \(B\) 가 모든 집합에 대하여 성립한다.

  \[ (\forall X)(\operatorname{M} (X) \implies B(X)) \]

  \((\exists x_j)B(x_j)\) 는 다음을 의미한다. 즉, \(B\) 가 어떤 집합에 대하여 성립한다.

  \[ (\exists X)(\operatorname{M} (X) \land B(X)) \]

Extensionality Principle✔

• 두 모임이 같다는 것은 두 모임이 같은 집합을 원소로 갖는다는 것과 동치이다.

• 증명

Axiom T✔

• 서로 같은 클래스들은 같은 클래스에 속한다.

• 증명

• 본 정리는 동등성의 치환성을 수반한다.

• 증명

Axiom P - Pairing Axiom✔

• 임의의 집합 \(x\) 와 \(y\) 에 대하여 오직 \(x\) 와 \(y\) 만을 멤버로 가지는 집합 \(x\) 가 존재한다.

  이 주장은 두 집합을 지닌 모임이 집합이라는 것을 선언해준다.

  공리는 이로써 집합을 생성하는 방법을 정해주는 역할, 무엇이 집합인지 특정해주는 역할을 한다.

Unordered Pair✔

• 이 정리는 오직 \(x\) 와 \(y\) 만을 갖는 집합 \(z\) 는 유일하다는 것을 말해준다.

• 증명

Axiom N - Null Set✔

• 원소를 갖지 않는 집합이 존재한다는 공리이다.

  이 공리는 공집합이 집합이라는 선언을 해준다.

• 공집합은 유일하다. 즉, \(\vdash (\exists _1x)(\forall y)(y \not\in x)\) 이다. 그러므로 공집합을 의미하는 상수 \(\varnothing\) 을 도입할 수 있다.

  \(\varnothing\) 이 집합이라는 것은 공리 N 과 문제 4.3 에 의하여 증명된다.

• 이 정의에 의하여 다음이 성립한다.

  \[ \begin{align}\begin{split} \vdash (\exists _1Z)(&[(\neg \operatorname{M} (X) \lor \neg \operatorname{M} (Y)) \land Z = \varnothing] \lor \\ &[\operatorname{M} (X) \land \operatorname{M} (Y) \land (\forall u)(u \in Z \iff u = X \lor u = Y)]) \\ \end{split}\end{align} \tag*{} \]

  이 결과는 다음 조건을 만족하는 항 \(\{X,Y\}\) 의 도입을 정당화해준다.

  \[ \begin{align}\begin{split} &[(\neg \operatorname{M} (X) \lor \neg \operatorname{M} (Y)) \land \{X,Y\} = \varnothing] \lor \\ &[\operatorname{M} (X) \land \operatorname{M} (Y) \land (\forall u)(u \in \{X,Y\} \iff u = X \lor u = Y)] \\ \end{split}\end{align} \tag*{} \]

  그러면 다음 두 결과가 성립한다.

  \[\vdash (\forall x)(\forall y)(\forall u)(u \in \{x, y\} \iff u = x \lor u = y)\]
  \[\vdash (\forall X)(\forall Y)\operatorname{M} (\{X, Y\})\]

• 집합 \(x\) 에 대하여 \(\{x\}\) 를 \(x\) 의 싱글톤이라고 한다. 이 집합은 오직 \(x\) 를 원소로 갖는다.

• 정리 2.28 은 \(\varnothing\) 이나 \(\{X, Y\}\) 같은 새로운 개별 상수나 함수 기호를 추가하는 것이 NBG 이론에 본질적으로 아무런 영향을 미치지 않는다는 것을 말해준다.

Ordered Pair✔

• 이 정의에 어떤 본질적인 직관적 의미가 존재하지 않는다. 이는 단지 순서쌍의 다음의 성질을 보이기 위하여 편의적인 방법으로 정의된 것이다.

• 동등성의 치환성에 의하여 이 정리의 역도 성립한다.

• 증명

• 즉, \(\left< X,Y,Z \right> = \left< \left< X, Y \right>, Z \right>\) 이고 \(\left< X, Y, Z, U \right> = \left< \left< \left< X, Y \right>, Z \right>, U \right>\) 이다.

Axiom B1 - B7✔

• 확장성의 원리를 사용하면 공리 \((B2), (B3), (B4)\) 의 \(Z\) 의 유일성을 증명할 수 있다. 즉, 다음이 성립한다.

  \[\vdash (\forall X)(\forall Y)(\exists_1 Z)(\forall u)(u \in Z \iff u \in X \land u \in Y)\]
  \[\vdash (\forall X)(\exists_1 Z)(\forall u)(u \in Z \iff u \not\in X)\]
  \[\vdash (\forall X)(\exists_1 Z)(\forall u)(u \in Z \iff (\exists v)(\left< u, v \right> \in X))\]

  이 결과는 새 함수 기호 \(\cap, -, \mathcal{D}\) 를 도입하는 것을 정당화해준다.

Intersection, Complement, Domain, Union, Universal Class, Difference✔

• 보편 집합 \(V\) 가 집합이 아닌 고유 모임이라는 것을 증명할 수 있다.

Predicative wff✔

• 예시

  \((\exists x_1)(x_1 \in Y_1)\) 은 술어적이지만, \((\exists Y_1)(x_1 \in Y_1)\) 은 술어적이지 않다.

Class Existence Theorem✔

• 증명

• 예시

  \(\phi (X, Y_1, Y_2)\) 를 \((\exists u)(\exists v)(X = \left< u,v \right> \land u \in Y_1 \land v \in Y_2)\) 라고 하자. \(\phi\) 에서 양화사가 오직 집합 변수를 지칭한다. 그러므로 모임 존재 정리에 의하여 다음이 성립한다.

  \[ \vdash (\exists Z)(\forall x)(x \in Z \iff (\exists u)(\exists v)(x = \left< u, v \right> \land u \in Y_1 \land v \in Y_2)) \]

  확장성 원리에 의하여 다음이 성립한다.

  \[ \vdash (\exists_1 Z)(\forall x)(x \in Z \iff (\exists u)(\exists v)(x = \left< u, v \right> \land u \in Y_1 \land v \in Y_2)) \]

  이 결과를 기반으로 새 함수 기호 \(\times\) 를 도입할 수 있다.

Cartesian Product, Relation✔

• \(V ^{2}\) 는 모든 순서쌍의 모임이다.

• 관계란 대상 간의 어떤 연결을 의미한다. 수학에서 관계는 순서쌍 \(\left< u,v \right>\) 로 표현된다.

Power Class, Sum Class, Identity Relation✔

• \(\phi (X, Y)\) 를 \(X \subseteq Y\) 라고 하자. 모임 존재 정리와 확장성 원리에 의하여 다음이 성립한다.

  \[\vdash (\exists _1Z)(\forall x)(x \in Z \iff x \subseteq Y)\]

  즉, \(Y\) 의 모든 부분집합을 원소로 갖는 유일한 모임 \(Z\) 가 존재한다. \(Z\) 를 \(Y\) 의 멱 모임이라 하고 \(\operatorname{P}(Y)\) 라고 표기한다.

• \(\phi (X, Y)\) 를 \((\exists v)(X \in v \land v \in Y)\) 라고 하자. 모임 존재 정리와 확장성 원리에 의하여 다음이 성립한다.

  \[ \vdash (\exists _1 Z)(\forall x)(x \in Z \iff (\exists v)(x \in v \land v \in Y)) \]

  즉, \(Y\) 의 원소의 원소를 모두 포함하는 유일한 모임 \(Z\) 가 존재하고, 이 \(Z\) 를 \(\bigcup_{}^{}Y\) 라고 표기한다.

• \(\phi (X)\) 를 \((\exists u)(X = \left< u,u \right>)\) 라고 하자. 모임 존재 정리와 확장성 원리에 의하여 다음을 만족하는 유일한 모임 \(Z\) 가 존재한다.

  \[ (\forall x)(x \in Z \iff (\exists u)(x = \left< u,u \right>)) \]

  \(Z\) 를 항등 관계라고 하고 \(I\) 라고 표기한다.

• 증명

Inverse Relation, Range✔

• 즉, 완전히 형식적으로 표현하면 다음과 같다.

  \[ (\forall u)(u \in \{\left< x_1, \dots, x_n \right> : \phi (x_1, \dots, x_n, Y_1, \dots, Y_m)\} \iff \\ (\exists x_1)\dots (\exists x_n)(u = \left< x_1, \dots, x_n \right> \land \phi (x_1, \dots, x_n, Y_1, \dots, Y_m))) \]

• 예시

  \(\phi\) 를 \(\left< x_2, x_1 \right> \in Y\) 라고 하자. \(\breve{Y}\) 를 \(\{\left< x_1, x_2 \right> : \left< x_2, x_1 \right> \in Y\}\) 의 축약이라고 하자. 그러면 다음이 성립한다.

  \[ \breve{Y} \subseteq V ^{2} \land (\forall x_1)(\forall x_2)(\left< x_1, x_2 \right> \in \breve{Y} \iff \left< x_2, x_1 \right> \in Y) \]

  \(\breve{Y}\) 를 \(Y\) 의 역관계(inverse relation)라고 한다.

• 예시

  \(\phi\) 를 \((\exists v)(\left< v,x \right> \in Y)\) 라고 하자. \(\mathcal{R}(Y)\) 을 \(\{x : (\exists v)(\left< v,x \right> \in Y)\}\) 라고 하자. 그러면 다음이 성립한다.

  \[ \vdash (\forall u)(u \in \mathcal{R}(Y) \iff (\exists v)(\left< v, u \right> \in Y)) \]

  \(\mathcal{R}(Y)\) 을 \(Y\) 의 치역(range)이라고 한다. 자명하게 \(\vdash \mathcal{R}(Y) = \mathcal{D}(Y)\) 이다.

공리 \((B1)-(B7)\) 은 정리 4.4 모임 존재 정리의 특수한 경우들이다. 그러므로 정리 4.4 의 공리꼴의 무한한 인스턴스 대신 유한한 공리꼴만을 가정해도 충분하다.

Axiom U - Sum Set✔

더욱 복잡도가 높은 집합의 존재성을 보장하기 위해서는 추가적인 공리들이 필요하다.

• 이 공리는 집합 \(x\) 의 합 모임 \(\bigcup_{}^{} x\) 이 집합임을 선언해준다. 이 공리에 의하여 다음이 성립한다.

  \[ \vdash (\forall x)\operatorname{M} \left(\bigcup x\right) \]

• 집합 \(x\) 안의 모든 집합의 합집합 \(\bigcup x\) 를 보통 다음과 같이 표기한다.

  \[ \bigcup_{v \in x}^{} v \]

Axiom W - Power Set✔

• 기존 집합에서 새로운 집합을 생성하는 방법 중 하나는 기존 집합의 부분집합의 집합을 취하는 것이다.

  이 공리는 집합 \(x\) 의 멱 모임 \(\operatorname{P} (x)\) 가 집합임을 선언해준다. 즉, 이 공리에 의해 다음이 성립한다.

  \[ \vdash (\forall x)\operatorname{M} (\operatorname{P} (x)) \]

Axiom S - Subsets✔

• 집합을 생성하는 더욱 일반적인 방법은 이 공리를 사용하는 것이다.

• 증명

• 증명

Function, Restriction, Injection✔

집합론을 완성하기 위해서는 공리 S 보다 더욱 강력한 공리가 필요하다. 먼저 편의상 다음을 정의하자.

• \(\left< y, z \right> \in X\) 를 만족하는 유일한 \(z\) 가 존재하면 \(z = X'y\) 이다. 그렇지 않은 경우 \(X'y = \varnothing\) 이다.

  \(X\) 가 함수이고 \(y\) 가 그것의 정의역의 집합일 경우 \(X'y\) 은 함수에 \(y\) 를 적용한 결과값이다. 그러므로 \(X'y\) 는 \(X(y)\) 로 표기한다.

  \(X\) 가 함수일 경우 \(X''Y\) 는 \(Y\) 로 제한된 \(X\) 의 치역이다.

Axiom R - Replacement✔

• 공리 R 은 \(Y\) 가 함수이고 \(x\) 가 집합이면 첫번째 성분이 \(x\) 에 속하는 \(Y\) 의 순서쌍의 두번째 성분의 모임은 집합이라는 것을 선언해준다.

  또는 그와 같은 말로, \(\mathcal{R}(x \mathord{\downharpoonright} Y)\) 은 집합이다.

Axiom I - Axiom of Infinity✔

• 무한집합의 존재성을 위해서는 본 공리가 필요하다.

• 공리 I 는 \(\varnothing\) 를 포함하고 어떤 집합 \(u\) 가 포함되면 \(u \cup \{u\}\) 도 포함하는 집합의 존재를 선언한다.

  즉, 이러한 집합 \(x\) 에 대하여 다음이 성립한다.

  \[ \{\varnothing\} \in x \]
  \[ \{\varnothing, \{\varnothing\}\} \in x \]
  \[ \{ \varnothing, \{\varnothing, \{\varnothing\}\}\} \in x \]
  \[ \vdots \]

  이는 페아노 공리에서 자연수 집합 \(\N\) 을 정의한 방법과 같다. 이제 \(\{\varnothing\}\) 을 \(1\) 으로 표기하고, \(\{\varnothing, \{\varnothing\}\}\) 을 \(2\) 로 표기하고, 각 집합에 순서대로 자연수 숫자를 부여하여 표기하자.

• 이것이 NBG 의 마지막 공리이다. 사실 공리 S 는 다른 공리에 의해 증명될 수 있지만 NBG 의 약한 부분이론에 대한 연구를 위하여 포함시켰다.

  이렇게 형성된 NBG 체계에 의한 집합론에서 러셀의 모순, 칸토어의 모순 등은 성립하지 않는다.

Ordinal Numbers✔

Order Relation, Well-Order✔

• 예시

  양의 정수 집합 \(P\) 위의 관계 \(<\) 는 정렬순서이다.

  정수 집합 \(\Bbb{Z}\) 위의 관계 \(<\) 는 전순서이고, 최소 원소가 없으므로 정렬순서가 아니다.

  정수 집합의 모든 부분집합의 집합 \(W\) 위의 관계 \(\subset\) 는 부분순서이고, 전순서가 아니다. 왜냐하면 \(\{1\}\not \subset \{2\}\) 이고 \(\{2\}\not \subset \{1\}\) 이기 때문이다.

Similar Order✔

• 순서 보존 사상을 생각하면 이해하기 쉽다.

• 순서 동형을 생각하면 이해하기 쉽다.

• 예시

  음이 아닌 정수 집합 \(A\) 위의 관계 \(<\) 을 \(r_1\) 이라고 하고, 양의 정수 집합 \(B\) 위의 관계 \(<\) 을 \(r_2\) 라고 하고, \(x \in A\) 에 대한 모든 순서쌍 \(\left< x, x+1 \right>\) 집합을 \(z\) 라고 하자.

  \(z\) 는 \(\left< r_1 , A \right>\) 를 \(\left< r_2 , B \right>\) 로 보내는 유사 사상이다.

Composition, Field, Total Order, Well-Ordering✔

Ordinal Class, Ordinal Number✔

• 위상 수학에서 정의한 순서형과 똑같이 정의된다.

• 특히, 수리논리학에서는 정렬순서 관계의 순서형에 큰 관심을 갖는다. \(\varnothing\) 의 순서형 \(\{\varnothing\}\) 을 제외하고 모든 순서형이 고유 모임이라는 것이 밝혀지기 때문에 \(W\) 의 유일한 원소에 대하여 모든 정렬순서가 유사한 정렬순서 구조의 모임 \(W\) 를 찾는 것이 좋다. 이는 순서수(ordinal number)의 개념으로 이어진다.

• 따라서 \(\vdash (\forall x)(x \in \operatorname{On}\iff \operatorname{Ord}(x))\) 이다.

• 9) 에 의하여 순서수가 아닌 유일한 순서수 모임은 \(\operatorname{On}\) 그 자체라는 것을 알 수 있다.

• 증명

• 따라서 순서수에 대하여 \(<_o\) 는 \(\in\) 와 같다. 그러므로 \(<_o\) 는 \(\operatorname{On}\) 을 정렬한다.

  특히, 정리 4.8 5) 에 의하여 임의의 순서수 \(x\) 는 그것보다 작은 순서수의 집합과 같다는 것을 알 수 있다.

Transfinite Induction✔

• 즉, 쉽게 말해서 이러하다.

  만약, 모든 서수 \(\beta\) 에 대하여 \(\beta\) 보다 작은 모든 서수가 \(X\) 에 속할 때 \(\beta\) 도 \(X\) 에 속한다면, 모든 서수가 \(X\) 에 속한다.

• 이 정리는 모든 서수가 주어진 성질 \(B(\alpha)\) 를 가진다는 것을 증명해야 할 때 사용된다. \(X = \{x : B(x) \land x \in \operatorname{On}\}\) 으로 두고 다음을 증명하면 된다.

  \[(\forall \beta)\left[ (\forall \alpha)(\alpha \in \beta \implies B(\alpha)) \implies B(\beta) \right]\]

• 증명

  \((\forall \beta)\left[ (\forall \alpha)(\alpha \in \beta \implies \alpha \in X) \implies \beta \in X \right]\) 를 가정하자.

  \(\operatorname{On}-X\) 에 포함되는 서수가 존재한다고 가정하자. \(\operatorname{On}\) 이 \(E\) 에 의하여 정렬되므로 \(\operatorname{On}-X\) 에 속하는 최소 서수 \(\beta\) 가 존재한다.

  그러면 \(\beta\) 보다 작은 모든 서수가 \(X\) 에 속한다. 그러면 가정에 의하여 \(\beta\) 는 \(X\) 에 속한다. 이는 모순이다. ■

• 증명

• \(\omega\) 를 직관적으로 자연수 집합 \(\N\) 의 서수라고 이해하면 편하다.

• 예시

  \[ \vdash \varnothing \in \omega \land 1 \in \omega \]

  (\(1 = \{\varnothing\}\) 임을 기억하자.)

• 증명

• \(\omega\) 의 원소, 즉, 자연수 \(0, 1, 2, 3, \dots\) 이 아닌 서수를 초한 서수라고 한다. \(\omega\) 가 최초의 초한 서수이다.

• \(\omega\) 는 \(\omega = \alpha'\) 인 서수 \(\alpha\) 를 갖지 않는데, 이러한 서수를 극한 서수라고 한다.

• 증명

• 집합론은 초한귀납법의 정의와 다음의 정리에 깊이 의존한다.

• 증명

• 이 정리를 통하여 초한 귀납법에 의한 새로운 함수 기호들을 도입할 수 있다.

• 예시

  서수 덧셈. 본 정리 2) 에 대하여 다음을 취하자.

  \[ x = \beta \quad X_1=\{\left< u,v \right> : v = u'\} \quad X_2 = \left\{\left< u,v \right> : v = \bigcup \mathcal{R}(u)\right\} \]

  그러면 각 서수 \(\beta\) 에 대하여 다음을 만족하는 유일한 함수 \(Y _{\beta }\) 가 존재한다.

  \[ Y _{\beta }'\varnothing =\beta \land (\forall \alpha )\Big (Y _{\beta }'(\alpha ') = (Y _{\beta }'\alpha )' \land \big [\operatorname{Lim}(\alpha )\implies Y _{\beta }'\alpha = \bigcup (Y _{\beta }'' \alpha ) \big ]\Big ) \]

  그러면 정의역 \((\operatorname{On})^{2}\) 위의 유일한 이항 함수 \(+_o\) 를 임의의 서수 \(\beta\) 와 \(\gamma\) 에 대하여 \(+_o(\beta ,\gamma )= Y _{\beta }' \gamma\) 와 같이 정의할 수 있다.

  관례를 따라 \(+_o(\beta ,\gamma )\) 를 \(\beta +_o \gamma\) 로 표기하자. 그러면 다음이 성립한다.

  \[ \beta +_o \varnothing = \beta \]
  \[ \beta +_o (\gamma ') = (\beta +_o \gamma )' \]
  \[ \operatorname{Lim}(\alpha ) \implies \beta +_o \alpha = \bigcup_{\tau <_o \alpha }^{}(\beta +_o \tau) \]

  특히, 다음이 성립한다.

  \[ \beta +_o 1 = \beta +_o (\varnothing ') = (\beta +_o \varnothing )' = \beta ' \]

• 예시

  서수 곱셈. 본 정리 2) 에 대하여 다음을 취하자.

  \[ x = \varnothing \quad X_1 = \{\left< u,v \right> : v = u +_o \beta \} \quad X_2 = \left\{\left< u,v \right> : v = \bigcup \mathcal{R}(u)\right\} \]

  그러면 위 예시와 같은 방식으로 다음의 성질을 가지는 함수 \(\beta \times _o \gamma\) 를 얻을 수 있다.

  \[ \beta \times _o \varnothing =\varnothing \]
  \[ \beta \times _o (\gamma ') = (\beta \times _o \gamma ) +_o \beta \]
  \[ \operatorname{Lim}(\alpha ) \implies \beta \times _o \alpha = \bigcup _{\tau<_o \alpha }(\beta \times _o \tau) \]

• 증명

Consistency Proof for Formal Number Theory(Schutte)✔

1차 수론 \(S\) 의 무모순성 증명은 최초로 겐첸(Gentzen, 1936, 1938)에 의하여 제시되었다. 이 내용을 \(\mathsf{PA}\) 의 서수 분석에서 엄밀하게 알아본다. 이후 아커만(Ackermann, 1940), Schutte(1951), Hlodovskii(1959) 등 다른 방식의 수론의 무모순성 증명이 제시되었고, 괴델의 두번째 불완전성 정리에서처럼 이 모든 증명들은 \(S\) 안에서 사용가능한 방법론을 사용하지 않았다. Schutte(1951)의 증명을 살펴보자.

무모순성 증명은 \(S\) 보다 강력한 체계 \(S _{\infty}\) 에 적용된다.

• 명백히 주어진 닫힌 원자 wff \(s = t\) 가 옳은지 틀린지 효과적으로 판정할 수 있다. 즉, 기계적으로 진행시킬 수 있는 절차가 존재한다.

• 예시

  다음은 \(S_{\infty}\) 의 공리이다.

  \[(0'') \cdot (0'') + 0'' = (0''') \cdot (0'')\]
  \[0' + 0'' \neq 0 ' \cdot 0''\]

• 예시

  다음과 같이 사이드 wff 를 생략할 수 있다.

  \(\dfrac{A \quad \neg A \lor D}{D}\) 는 절단이고 \(\dfrac{\neg A \quad \neg B}{\neg (A \lor B)}\) 는 드모르간의 법칙이다.

• 무한 귀납의 규칙이 \(S\) 에서의 증명의 개념보다 더 복잡하므로 \(S_{\infty}\) 에서의 증명의 개념을 더 정의해야 한다. 따라서 G-트리를 기반으로 증명트리를 정의할 필요가 있다.

• 예시

  

  \(A,B,C,D\) 가 초기점이고 \(E\) 가 종점이다.

• 예시

  

  \(A,B,C_1, C_2, \dots\) 가 초기점이고 \(E\) 가 종점이다.

• 예시

  

  \(A\) 가 유일한 초기점이고, \(E\) 가 종점이다.

• 서수의 열이 가산무한히 감소할 수 없으므로 스레드에 강한 규칙이나 절단이 오직 유한하게만 존재한다. 또한 주어진 wff 에 대하여 약한 규칙이 오직 유한하게 필요하다. 그러므로 증명 트리의 모든 스레드의 약한 규칙의 연속적인 적용은 오직 유한하다고 할 수 있다. 그러므로 증명 트리의 모든 스레드는 유한하다.

• 증명 트리의 wff 에 할당될 서수의 모임을 제한하면, 이는 증명 트리의 개념을 제한하고, 그러므로 더 작은 정리 집합을 얻게 된다.

  가산무한한 서수의 다양한 구성적인(constructive) 절편을 사용하면, 그렇게 얻게될 체계와 무모순성 증명에 사용될 방법들이 덜 또는 더 구성적이게 된다.

• 증명

  \(n\) 에 대한 귀납법을 수행하자.

  \(n = 0\):

  \(A\) 는 닫힌 원자 wff 이다. 그러면 \(A\) 가 옳거나 틀리므로 \(A\) 나 \(\neg A\) 가 공리이다. 그러면 다음과 같은 증명 트리를 만들 수 있다.

  	연역	근거
  1	\(A\)
  2	\(\neg A \lor A\)	희석(강)

  	연역	근거
  1	\(\neg A\)
  2	\(A \lor \neg A\)	희석(강)
  3	\(\neg A \lor A\)	교환(약)

  \(\neg A \lor A\) 의 증명이 서수 \(1\) 을 갖도록 서수를 부여할 수 있다.

  \(n\) 보다 작은 수에 대하여 성립한다고 가정:

  1. \(A\) 가 \(A_1 \lor A_2\) 인 경우. 귀납의 가정에 의하여 서수가 \(2(n-1) + 1 = 2n-1\) 보다 같거나 작은 \(\neg A_1 \lor A_1\) 와 \(\neg A_2 \lor A_2\) 의 증명이 존재한다. 그러면 각각에 대하여 강한 규칙 희석을 사용하여 서수 \(2n\) 을 갖는 \(\neg A_1 \lor A_2 \lor A_2\) 와 \(\neg A_2 \lor A_1 \lor A_2\) 의 증명을 얻을 수 있다. 그렇다면 이로써 강한 규칙 드모르간을 사용하여 서수 \(2n+1\) 을 갖는 \(\neg (A_1 \lor A_2)\lor A_1 \lor A_2\), 즉, \(\neg A \lor A\) 의 증명을 얻을 수 있다.

  2. \(A\) 가 \(\neg B\) 인 경우. 귀납의 가정에 의하여 서수 \(2n-1\) 의 \(\neg B \lor B\) 의 증명이 존재한다. 약한 규칙 교환에 의하여 서수 \(2n-1\) 의 \(B \lor \neg B\) 의 증명을 얻을 수 있고, 강한 규칙 부정에 의하여 서수 \(2n (\leq 2n+1)\) 의 \(\neg \neg B \lor \neg B\), 즉, \(\neg A \lor A\) 의 증명을 얻을 수 있다.

  3. \(A\) 가 \((\forall x)B(x)\) 인 경우. 귀납의 가정에 의하여 모든 자연수 \(k\) 에 대하여 서수가 \(2n-1\) 과 같거나 작은 \(\neg B(k) \lor B(k)\) 의 증명이 존재한다. 그러면 강한 규칙 양화에 의하여 각 \(k\) 에 대하여 서수 \(\leq 2n\) 의 \((\neg (\forall x)B(x)) \lor B(k)\) 증명이 존재한다. 그러므로 약한 규칙 교환에 의하여 서수 \(\leq 2n\) 의 \(B(\overline{k}) \lor \neg (\forall x)B(x)\) 의 증명이 존재한다. 강한 규칙 무한 귀납을 적용하면 서수 \(\leq 2n+1\) 의 \(((\forall x)B(x)) \lor \neg (\forall x)B(x)\) 의 증명을 얻을 수 있다. 약한 규칙 교환을 적용하면 서수 \(\leq 2n+1\) 의 \((\neg (\forall x)B(x)) \lor (\forall x)B(x)\), 즉, \(\neg A \lor A\) 의 증명을 얻는다.

  ■

• 증명

  일반적으로 \(S_{\infty}\) 에서 증명가능한 닫힌 wff \(B(t)\) 에 대하여 \(s\) 가 \(t\) 와 같은 값을 가지면 \(B(s)\) 도 \(S_{\infty}\) 에서 증명가능하다. \(s\) 가 \(t\) 와 \(\overline{n}\) 라는 같은 값을 가지면 보조정리 A.1 에 의하여 \(\neg A(\overline{n})\lor A(\overline{n})\) 이 증명가능하므로 \(\neg A(s) \lor A(t)\) 는 증명가능하다. 그러면 희석에 의하여 \(s \neq t \lor \neg A(s) \lor A(t)\) 는 증명가능하다. ▲

  \(s\) 와 \(t\) 가 다른 값을 가지면 \(s=t\) 는 틀리므로 \(s \neq t\) 는 공리이다. 그러면 희석과 교환에 의하여 \(s \neq t \lor \neg A(s) \lor A(t)\) 는 정리이다. ■

• 증명

  \(S\) 의 정리인 닫힌 wff \(A\) 를 잡자. 명백하게 \(S\) 의 모든 증명은 유한한 증명 트리로 표현가능하다. 이 증명 트리의 초기 wff 는 \(S\) 의 공리이고, 츄론규칙은 물론 MP 와 Gen 이다. \(A\) 의 증명트리의 서수를 \(n\) 이라고 하자.

  \(n = 0\) 이면 \(A\) 가 \(S\) 의 공리이다.

  1차 논리 공리 \((A1)\):

  \(A\) 가 \(B \implies (C \implies B)\), 즉, \(\neg B \lor (\neg C \lor B)\) 인 경우. 보조정리 A.1 에 의하여 \(S_{\infty}\) 에서 \(\neg B \lor B\) 는 증명가능하다. 그러면 희석과 교환에 의하여 \(\neg B \lor \neg C \lor B\) 이다. ▲

  1차 논리 공리 \((A2)\)

  \(A\) 가 \((B \implies (C \implies D)) \implies ((B \implies C) \implies (B \implies D))\), 즉, \(\neg (\neg B \lor \neg C \lor D) \lor \neg (\neg B \lor C) \lor (\neg B \lor D)\) 인 경우. 보조정리 A.1 에 의하여 \(\neg (\neg B \lor C) \lor \neg B \lor C\) 와 \((\neg B \lor \neg C \lor D) \lor \neg (\neg B \lor \neg C \lor D)\) 를 얻을 수 있다.

  그러면 다음과 같이 연역할 수 있다.

  	연역	근거
  1	\((\neg B \lor \neg C \lor D) \lor \neg (\neg B \lor \neg C \lor D)\)
  2	\(\neg (\neg B \lor \neg C \lor D) \lor (\neg B \lor \neg C \lor D)\)	1, 교환
  3	\(\neg (\neg B \lor \neg C \lor D) \lor (\neg B \lor D \lor \neg C)\)	2, 교환
  4	\(\neg (\neg B \lor C) \lor \neg B \lor C\)
  5	\(\neg B \lor C \lor \neg (\neg B \lor C)\)	4, 교환
  6	\(C \lor \neg B \lor \neg (\neg B \lor C)\)	5, 교환
  7	\(\neg (\neg B \lor \neg C \lor D) \lor \neg B \lor D \lor \neg B \lor \neg (\neg B \lor C)\)	3, 6, 절단
  8	\(\neg (\neg B \lor \neg C \lor D) \lor \neg B \lor D \lor \neg (\neg B \lor C)\)	7, 합병
  9	\(\neg (\neg B \lor \neg C \lor D) \lor \neg (\neg B \lor C) \lor (\neg B \lor D)\)	8, 교환

  ▲

  1차 논리 공리 \((A3)\):

  \(A\) 가 \((( \neg C) \implies (\neg B)) \implies (((\neg C) \implies B) \implies C)\), 즉, \(\neg (\neg \neg C \lor \neg B) \lor \neg (\neg \neg C \lor B) \lor C\) 인 경우. 먼저 보조정리 A.1 에 의하여 \(\neg C \lor C\) 이고, 부정에 의하여 \(\neg \neg \neg C \lor C\) 이며, 희석과 교환에 의하여 다음을 얻는다.

  \[ \neg \neg \neg C \lor \neg (\neg \neg C \lor B) \lor C \tag{a} \]

  같은 방식으로 \(\neg \neg \neg C \lor C \lor \neg \neg B\) 와 \(\neg B \lor C \lor \neg \neg B\) 을 얻고, 드모르간에 의하여 \(\neg (\neg \neg C \lor B) \lor C \lor \neg \neg B\) 이다. 그러면 교환에 의하여 다음을 얻는다.

  \[ \neg \neg B \lor \neg (\neg \neg C \lor B) \lor C \tag{b} \]

  \((a)\) 와 \((b)\) 에 대한 드모르간에 의하여 \(\neg (\neg \neg C \lor \neg B) \lor \neg (\neg \neg C \lor B)\lor C\) 이다. ▲

  1차 논리 공리 \((A4)\):

  \(A\) 가 \((\forall x_i)B(x_i) \implies B(t)\), 즉, \((\neg (\forall x)B(x)) \lor B(t)\) 인 경우. 보조정리 A.1 에 의하여 \(\neg B(t) \lor B(t)\) 이다. 양화 규칙에 의하여 \((\neg (\forall x)B(x)) \lor B(t)\) 이다. ▲

  1차 논리 공리 \((A5)\):

  \(A\) 가 \((\forall x)(B \implies C) \implies (B \implies (\forall x) C)\), 즉, \(\neg (\forall x)(\neg B \lor C(x)) \lor \neg B \lor (\forall x)C(x)\) 인 경우. 이때 \(x\) 는 \(B\) 의 자유변수가 아니다.

  보조정리 A.1 에 의하여 모든 자연수 \(n\) 에 대하여 \(\neg (\neg B \lor C(\overline{n})) \lor \neg B \lor C(\overline{n})\) 의 증명이 존재한다. 보조정리 A.1 에 의하여 이들 증명의 서수는 \(\neg B \lor C(x)\) 의 연결사와 양화사의 갯수 \(k\) 에 대하여 \(\leq 2k+1\) 이다.

  그러면 양화 규칙에 의하여 각 \(n\) 에 대하여 다음은 서수 \(\leq 2k + 2\) 인 증명을 가진다.

  \[\neg (\forall x) (\neg B \lor C(x)) \lor \neg B \lor C(\overline{n})\]

  그러면 무한 귀납에 의하여 다음은 서수 \(\leq 2k + 3\) 인 증명을 가진다.

  \[\neg (\forall x) (\neg B \lor C(x)) \lor \neg B \lor (\forall x) C(x)\]

  ▲

  수론 공리 \((S1)\):

  \(A\) 가 \(t_1 = t_2 \implies (t_1 = t_3 \implies t_2 = t_3)\), 즉, \(t_1 \neq t_2 \lor t_1 \neq t_3 \lor t_2 = t_3\) 인 경우.

  \(A(x)\) 를 \(x = t_3\) 로 두고, \(s\) 를 \(t_1\) 로 두고, \(t\) 를 \(t_2\) 로 두고 보조정리 A.2 를 적용하면 된다. ▲

  수론 공리 \((S2)\):

  \(x_1 = x_2 \implies x_1' = x_2'\), 즉, \(t_1 \neq t_2 \lor (t_1)' = (t_2)'\) 인 경우. \(t_1\) 와 \(t_2\) 가 같은 값을 가지면 \((t_1)'\) 와 \((t_2)'\) 도 그렇다. 그러므로 \((t_1)' = (t_2)'\) 는 옳고, 그러므로 공리이다. 그러면 희석에 의하여 \(t_1 \neq t_2 \lor (t_1)' = (t_2)'\) 을 얻는다.

  \(t_1\) 과 \(t_2\) 가 다른 값을 가질 경우 \(t_1 \neq t_2\) 이 공리이므로 희석과 교환에 의하여 \(t_1 \neq t_2 \lor (t_1)' = (t_2)'\) 이 증명가능하다. ▲

  수론 공리 \((S3)\):

  \(A\) 가 \(0 \neq t'\) 인 경우. \(0\) 과 \(t'\) 은 다른 값을 가지므로 \(0 \neq t'\) 은 공리이다. ▲

  수론 공리 \((S4)\):

  \(A\) 가 \((t_1)' = (t_2)' \implies t_1 = t_2\), 즉, \((t_1)' \neq (t_2)' \lor t_1 = t_2\) 인 경우. (쉽게 증명가능하다.) ▲

  수론 공리 \((S5)\):

  \(A\) 가 \(t_1 + 0 = t_1\) 인 경우. \(t+0\) 와 \(t\) 가 같은 값을 가지므로 \(t+0=t\) 는 공리이다. ▲

  수론 공리 \((S6)-(S8)\):

  닫힌 항의 값을 계산하는 재귀 식으로부터 곧바로 쉽게 증명된다. ▲

  수론 공리 \((S9)\):

  \(A\) 가 \(B(0) \implies \bigg ((\forall x)\Big (B(x) \implies B(x')\Big ) \implies (\forall x)B(x) \bigg )\), 즉, 다음과 같을 경우.

  \[ \neg B(0) \lor \neg (\forall x)\Big (\neg B(x) \lor B(x')\Big ) \lor (\forall x)B(x) \]

  먼저 보조정리 A.1 과 교환과 희석에 의해 다음은 증명가능하다.

  \[ \neg B(0) \lor \neg (\forall x)\left( \neg B(x) \lor B(x') \right) \lor B(0) \tag{1} \]

  한편, \(k \geq 0\) 에 대하여 다음 wff 가 증명가능하다는 것을 귀납적으로 증명하자.

  \[ \neg B(0) \lor \neg (\neg B(0) \lor B(\overline{1})) \lor \dots \lor \neg (\neg B(\overline{k})\lor B(\overline{k}'))\lor B(\overline{k}') \tag{2} \]

  1. \(k=0\) 인 경우 보조정리 A.1 과 희석과 교환에 의하여 \(\vdash _{S_{\infty} }\neg \neg B(0) \lor \neg B(0) \lor B(1)\) 이다. 비슷하게 \(\vdash _{S_{\infty} }\neg B(\overline{1})\lor \neg B(0) \lor B(\overline{1})\) 을 얻는다. 그러므로 드모르간에 의하여 \(\vdash _{S_{\infty} }\neg (\neg B(0) \lor B(\overline{1})) \lor \neg B(0) \lor B(\overline{1})\) 이고 교환에 의하여 다음을 얻는다.

     \[ \vdash _{S_{\infty} } \neg B(0) \lor \neg (\neg B(0) \lor B(\overline{1})) \lor B(\overline{1}) \]

  2. \(k\) 에 대하여 성립한다고 가정하면 다음이 성립한다.

     \[ \vdash _{S_{\infty} } \neg B(0) \lor \neg (\neg B(0) \lor B(\overline{1})) \lor \dots \lor \neg (\neg B(\overline{k})\lor B(\overline{k}'))\lor B(\overline{k}') \]

     교환, 부정, 희석에 의하여 다음이 성립한다.

     \[ \begin{align}\begin{split} \vdash _{S_{\infty} }&\neg \neg B(\overline{k}') \lor \neg B(0) \lor \neg (\neg B(0) \lor B(\overline{1})) \lor \dots \\ &\lor \neg (\neg B(\overline{k})\lor \neg B(\overline{k}')) \lor B(\overline{k}'') \\ \end{split}\end{align} \tag*{} \]

     한편, 보조정리 A.1 를 \(B(\overline{k}'')\) 에 적용하고, 희석과 교환을 적용하면 다음을 얻는다.

     \[ \begin{align}\begin{split} \vdash _{S_{\infty} }&\neg B(\overline{k}'') \lor \neg B(0) \lor \neg (\neg B(0) \lor B(\overline{1})) \lor \dots \\ &\lor \neg (\neg B(\overline{k})\lor \neg B(\overline{k}')) \lor B(\overline{k}'') \\ \end{split}\end{align} \tag*{} \]

     그러면 드모르간에 의하여 다음을 얻는다.

     \[ \begin{align}\begin{split} \vdash _{S_{\infty} }&\neg (\neg B(\overline{k}')\lor B(\overline{k}'')) \lor \neg B(0) \lor \neg (\neg B(0) \lor B(\overline{1})) \lor \dots \\ &\lor \neg (\neg B(\overline{k})\lor \neg B(\overline{k}')) \lor B(\overline{k}'') \\ \end{split}\end{align} \tag*{} \]

     여기에 교환을 적용하면 \(k+1\) 인 경우의 결론이 바로 나온다.

  이제 \((2)\) 에 양화를 적용하면 다음이 성립한다.

  \[ \vdash _{S_{\infty} } \neg B(0) \lor \neg (\forall x)(\neg B(x) \lor B(x')) \lor \dots \\ \lor \neg (\forall x) (\neg B(x)\lor B(x'))\lor B(\overline{k}') \]

  합병에 의하여 \(\vdash _{S_{\infty} }\neg B(0) \lor \neg (\forall x)(\neg B(x) \lor B(x')) \lor B(\overline{k}')\) 이다. 그러면 \((1)\) 에 의하여 모든 \(k \geq 0\) 에 대하여 다음이 성립한다.

  \[ \vdash _{S_{\infty} }\neg B(0) \lor \neg (\forall x)(\neg B(x) \lor B(x')) \lor B(\overline{k}) \]

  이제 무한 귀납을 적용하면 다음이 성립한다.

  \[ \vdash _{S_{\infty} }\neg B(0) \lor \neg (\forall x)(\neg B(x) \lor B(x')) \lor (\forall x) B(x) \]

  ▲

  그러므로 \(S\) 의 모든 닫힌 공리는 \(S_{\infty}\) 에서 증명가능하다. ▲

  \(n>0\) 을 가정하자.

  그러면 \(A\) 는 MP 의 결과이거나, Gen 의 결과이다.

  \(A\) 가 \(B\) 와 \(B \implies A\) 에 MP 를 적용하여 나온 결과이면 \(B\) 와 \(B \implies A\) 는 증명트리에서 \(n\) 보다 작은 서수를 갖고 있다. \(B\) 에 자유변수가 있어도 \(B\) 와 선행자에 있는 자유변수를 \(0\) 으로 대체할 수 있기 때문에 \(B\) 가 자유변수를 갖지 않는다고 가정해도 상관없다. 그러면 귀납적 가정에 의하여 \(\vdash _{S_{\infty} }B\) 와 \(\vdash _{S_{\infty} }B \implies A\), 즉, \(\vdash _{S_{\infty} }\neg B \lor A\) 이다. 그러면 절단에 의하여 \(\vdash _{S_{\infty} }A\) 이다.

  \(A\) 가 \(B\) 로부터 일반화된 결과 \((\forall x)B(x)\) 인 경우도 있다. 증명 트리에서 \(B(x)\) 를 역추적하여 자유변수 \(x\) 를 적절하게 \(\overline{n}\) 으로 바꿀 수 있다. 그러면 같은 서수의 \(B(\overline{n})\) 의 증명을 얻는다. 이는 모든 \(n\) 에 대하여 성립하므로 귀납적 가정에 의하여 모든 \(n\) 에 대하여 \(\vdash _{S_{\infty} }B(\overline{n})\) 이다. 그러면 무한 귀납에 의하여 \(\vdash _{S_{\infty} }(\forall x)B(x)\), 즉, \(\vdash _{S_{\infty} }A\) 이다. ■

• \(S_{\infty}\) 의 무모순성을 증명하면 자동으로 \(S\) 의 무모순성도 증명된다.

• 증명

  \(S\) 가 모순이면 \(\vdash _S0 \neq 0\) 이다. 보조정리 A.3 에 의하여 \(\vdash _{S_{\infty} }0 \neq 0\) 이다. 그러나 \(0=0\) 이 옳으므로 \(\vdash _{S_{\infty} }0 = 0\) 이다. 그러면 \(S_{\infty}\) 의 임의의 wff \(A\) 에 대하여 희석에 의하여 \(\vdash _{S_{\infty} } 0 \neq 0 \lor A\) 이고 \(\vdash _{S_{\infty} }0 = 0\) 과 함께 절단을 적용하면 \(\vdash _{S_{\infty} }A\) 을 얻는다. 즉, \(S_{\infty}\) 의 임의의 wff 가 증명가능하다. 그러므로 \(S_{\infty}\) 는 모순이다. ■

• 증명

  드모르간:

  \(A\) 가 \(\neg (B \lor E) \lor D\) 인 경우. \(A\) 의 증명을 취하자. \(A\) 에서부터 시작하여 증명 트리를 거슬러 올라가서 \(\neg (B \lor E)\) 를 부분식으로 갖는 모든 wff 들을 찾자. 이 과정은 모든 약한 규칙의 적용과 \(\neg (B \lor E)\) 를 사이드 wff 로 갖는 모든 강한 규칙의 적용의 결과를 추적함으로써 이루어진다. 이 과정은 오로지 희석 \(\dfrac{F}{\neg (B \lor E)\lor F}\) 을 만나거나 드모르간

  \[\dfrac{\neg B \lor F \quad \neg E \lor F }{\neg (B \lor E)\lor F}\]

  을 만나야만 끝난다. 이 과정을 통하여 \(\neg (B \lor E)\) 가 나타나는 wff 를 모은 집합을 \(\neg (B \lor E)\) 의 역사(history)라고 한다.

  \(\neg (B \lor E)\) 을 그것의 역사 속에서 \(\neg B\) 로 교체할 수 있다. 그러면 불필요해진 식들을 지우고 끝 wff 가 \(\neg B \lor D\) 인 증명 트리를 얻을 수 있다.

  마찬가지로 \(\neg (B \lor E)\) 을 \(\neg E\) 로 교체하면 \(\neg E \lor D\) 의 증명을 얻을 수 있다. ▲

  부정:

  \(A\) 가 \(\neg \neg B \lor D\) 인 경우. \(\neg \neg B\) 의 역사를 정의하고 역사 속의 모든 \(\neg \neg B\) 를 \(B\) 로 대체하면 \(B \lor D\) 의 증명을 얻을 수 있다. ▲

  무한 귀납:

  \(A\) 가 \(((\forall x) B(x))\) 인 경우. \((\forall x)B(x)\) 의 역사를 정의하고 \((\forall x)B(x)\) 를 그것의 역사 속에서 \(B(\overline{n})\) 으로 교체하면 \(B(\overline{n})\lor D\) 의 증명을 얻을 수 있다. ■

• 증명

  주어진 \(A\) 의 증명의 서수 \(\alpha\) 에 대한 초한 귀납법을 사용하자.

  \(\alpha = 0\) 인 경우 이 증명은 절단을 포함할 수 없고, 그러므로 차수가 \(0\) 이다. ▲

  모든 서수 \(< \alpha\) 에 대하여 정리가 증명되었다고 가정하자. 끝 wff \(A\) 에서부터 시작하여 약한 규칙이 아닌 규칙이 첫번째로 적용된 것을 찾자. 즉, 강한 규칙이나 절단이 적용된 것을 찾자.

  이것이 강한 규칙인 경우 각 전제는 서수 \(\alpha _1 (<\alpha)\) 를 갖는다. 귀납적 가정에 의하여 이들의 전제에 대하여 더 낮은 차수와 서수 \(2 ^{\alpha _1}\) 를 갖는 증명 트리가 존재한다. 원래의 증명 트리의 전제 위쪽부분을 이 증명트리로 교체하자. 그러면 \(A\) 의 서수가 모든 \(2 ^{\alpha _1}\) 보다 큰 \(2 ^{\alpha }\) 인 새로운 \(A\) 의 증명을 얻는다. ▲

  절단이 적용되었을 경우는 \(A\) 가 \(C \lor D\) 일 때 다음과 같다.

  \[ \frac{C \lor B \quad \neg B \lor D}{C \lor D} \]

  \(C \lor B\) 와 \(\neg B \lor D\) 의 서수를 각각 \(\alpha _1\) 와 \(\alpha_2\) 라고 하면 귀납적 가정에 의하여 이들의 증명 트리의 위쪽을 차수를 감소시키고 서수를 \(2 ^{\alpha _1}\) 와 \(2 ^{\alpha _2}\) 가 되도록 교체할 수 있다.

  이제 \(B\) 의 형태에 따른 조사를 해야 한다.

  1. \(B\) 가 원자 wff 인 경우.

     \(B\) 나 \(\neg B\) 는 반드시 공리이다. \(B\) 와 \(\neg B\) 중에 공리가 아닌 것을 \(K\) 라고 하자. 귀납적 가정에 의하여 \(K\) 를 포함하는 전제의 증명 트리 위쪽 부분을 더 작은 차수와 서수 \(2 ^{\alpha _i}\) (\(i=1\) 또는 \(i=2\))를 갖는 증명 트리로 교체할 수 있다.

     이 새로운 증명 트리에서 \(K\) 의 역사를 정의하고, 역사에서 \(K\) 를 모두 지우면 서수 \(2 ^{\alpha _i}\) 를 갖는 \(C\) 의 증명 트리 또는 \(D\) 의 증명 트리를 얻는다. 그러면 희석에 의하여 서수 \(2 ^{\alpha }\) 를 갖는 \(C \lor D\) 의 증명을 얻을 수 있고, 절단을 제거했으므로 이 증명 트리의 차수는 \(m\) 보다는 작다.

  2. \(B\) 가 \(\neg E\) 인 경우. \(\dfrac{C \lor \neg E \quad \neg \neg E \lor D}{C \lor D}\)

     차수가 \(<m\) 이고 서수 \(2 ^{\alpha _2}\) 를 갖는 \(\neg \neg E \lor D\) 의 증명이 존재한다. 보조정리 A.5 에 의하여 차수 \(<m\) 와 서수 \(2 ^{\alpha _2}\) 의 \(E \lor D\) 에 대한 증명 트리가 존재한다. 한편 귀납적 가정에 의하여 차수 \(<m\) 와 서수 \(2 ^{\alpha _2}\) 의 \(C \lor \neg E\) 에 대한 증명 트리가 존재한다.

     이제 다음을 고려하자.

     	연역	근거
     1	\(E \lor D\)
     2	\(D \lor E\)	1, 교환
     3	\(C \lor \neg E\)
     4	\(\neg E \lor C\)	3, 교환
     5	\(D \lor C\)	2, 4, 절단
     6	\(C \lor D\)	5, 교환

     위의 절단은 \(\neg E\) 의 차수이고 이는 \(\neg \neg E\) 보다 작으며, 그러므로 \(\leq m\) 이다. \(D \lor C\) 의 서수는 \(2 ^{\alpha _2}\) 가 되도록 잡을 수 있다. 그러므로 이 증명은 더 작은 차수와 서수 \(2 ^{\alpha }\) 이다.

  3. \(B\) 가 \(E \lor F\) 인 경우. \(\dfrac{C \lor E \lor F \quad \neg (E \lor F) \lor D}{C \lor D}\)

     더 작은 차수와 서수 \(2 ^{\alpha _2}\) 를 갖는 \(\neg (E \lor F) \lor D\) 에 대한 증명트리가 존재한다. 그러면 보조정리 A.5 에 의하여 차수가 \(<m\) 이고 서수가 \(2 ^{\alpha _2}\) 인 \(\neg E \lor D\) 와 \(\neg F \lor D\) 의 증명트리가 존재한다. 또한 차수가 \(<m\) 이고 서수가 \(2 ^{\alpha _1}\) 인 \(C \lor E \lor F\) 의 증명트리가 존재한다.

     	연역	근거
     1	\(C \lor E \lor F\)
     2	\(\neg F \lor D\)
     3	\(C \lor E \lor D\)	1, 2, 절단
     4	\(C \lor D \lor E\)	3, 교환
     5	\(\neg E \lor D\)
     6	\(C \lor D \lor D\)	4, 5, 절단
     7	\(C \lor D\)	6, 합병

     이 절단은 차수 \(<m\) 를 가지므로 새로운 증명트리는 차수 \(<m\) 를 가진다. \(C \lor E \lor D\) 의 서수는 \(2 ^{\max (\alpha _1,\alpha _2)}+_o1\) 로 잡을 수 있고 \(C \lor D \lor D\) 와 \(C \lor D\) 는 \(2 ^{\alpha }\) 로 잡을 수 있다.

  4. \(B\) 가 \((\forall x)E\) 인 경우. \(\dfrac{C \lor (\forall x)E \quad (\neg (\forall x)E) \lor D}{C \lor D}\)

     귀납적 가정에 의하여 \(C \lor (\forall x)E\) 의 증명 트리는 더 작은 차수와 서수 \(2 ^{\alpha _1}\) 를 갖는 증명 트리로 교체할 수 있다. 보조정리 A.5 와 일반적으로 \(S_{\infty}\) 에서 증명가능한 닫힌 wff \(B(t)\) 에 대하여 \(s\) 가 \(t\) 와 같은 값을 가지면 \(B(s)\) 도 \(S_{\infty}\) 에서 증명가능하다는 사실에 의하여 임의의 \(t\) 에 대하여 차수가 \(<m\) 이고 서수가 \(2 ^{\alpha_1 }\) 인 \(C \lor E(t)\) 의 증명을 얻을 수 있다.

     귀납적 가정에 의하여 \((\neg (\forall x)E)\lor D\) 도 더 작은 차수와 서수 \(2 ^{\alpha _2}\) 를 갖는 증명으로 교체될 수 있다. 이 증명에서 \(\neg (\forall x)E\) 의 역사는 다음과 같은 희석과 양화의 적용의 주요 wff 로써 종료된다.

     \[ \dfrac{\neg E(t_i) \lor g_i }{(\neg (\forall x)E) \lor g_i } \]

     그러한 양화의 적용을 다음과 같은 절단으로 교체할 수 있다.

     \[ \frac{C \lor E(t_i) \quad (\neg E(t_i)) \lor g_i}{C \lor g_i} \]

     역사에서 모든 \(\neg (\forall x)E(x)\) 를 \(C\) 로 교체하자. 그 결과는 끝 wff 가 \(C \lor D\) 인 증명트리이다.

     이 증명 트리는 \(\neg E(t_i)\) 의 차수가 \(\neg (\forall x)E\) 보다 작으므로 차수가 \(<m\) 이다.

     증명 트리에서 각각의 이전 서수 \(\beta\) 를 \(2 ^{\alpha _1} +_o \beta\) 로 교체하자. \(\beta\) 가 이전에 제거된 양화 규칙의 전제 \(\neg E(t_i) \lor g_i\) 의 서수이고, \(\gamma\) 가 결론 \((\neg (\forall x)E) \lor g_i\) 이면, 새로 도입된 절단에서 \(C \lor E(t_i)\) 가 서수 \(2 ^{\alpha _1}\) 를 갖고, \(\neg E(t_i) \lor g_i\) 가 서수 \(2 ^{\alpha _1} +_o \beta\) 를 갖고, 결론 \(C \lor g_i\) 는 서수 \(2 ^{\alpha _1}+_o \gamma >\max (2 ^{\alpha _1}, 2 ^{\alpha _1} +_o \beta )\) 를 갖는다.

     다른 모든 곳에서 결론의 서수는 전제의 서수보다 크다. 왜냐하면 \(\delta <_o \mu\) 가 \(2 ^{\alpha _1} +_o \delta <_o 2 ^{\alpha _1} +_o \mu\) 를 함의하기 때문이다.

     마지막으로 서수 \(\alpha _2\) 를 가졌던 오른쪽 전제 \((\neg (\forall x)E) \lor D\) 는 다음과 같은 서수 \(2 ^{\alpha _1} +_o 2 ^{\alpha _2}\) 를 갖는 \(C \lor D\) 로 넘어가게 된다.

     \[ 2 ^{\alpha _1} +_o 2 ^{\alpha _2} \leq 2 ^{\max (\alpha _1, \alpha _2)} +_o 2 ^{\max (\alpha _1, \alpha _2)} =\\ \qquad 2 ^{\max (\alpha _1, \alpha _2)} \times _o 2 = 2 ^{\max (\alpha _1, \alpha _2)} +_o 1 \leq 2 ^{\alpha } \]

     이것이 \(<_o 2 ^{\alpha }\) 이면 \(C \lor D\) 의 서수를 \(2 ^{\alpha }\) 까지 올릴 수 있다. ■

• 그러므로 모든 증명이 절단이 없는 증명으로 대체될 수 있다.

• 증명

  \((0 \neq 0) \lor (0 \neq 0) \lor \dots \lor (0 \neq 0)\) 의 형태를 갖는 wff \(A\) 를 잡자. \(A\) 의 증명이 존재하면 따름정리 A.7 에 의하여 절단이 존재하지 않는 \(A\) 의 증명이 존재한다.

  추론 규칙 중에서 오직 절단만이 식의 어떤 요소를 제거할 수 있다. 약한 규칙은 위치를 바꾸거나 무의미한 요소를 제거하는 것이고, 강한 규칙은 식에 요소를 추가하는 것이다.

  식에 어떤 요소를 제거할 수 있는 절단이 증명에 포함되지 않으므로 \(A\) 는 반드시 \((0 \neq 0) \lor (0 \neq 0) \lor \dots \lor (0 \neq 0)\) 의 형태의 wff 로부터 도출되어야 한다. 그러므로 증명의 공리는 이런 형태여야만 한다.

  그러나 이러한 형태의 공리는 존재하지 않는다. 그러므로 \(A\) 는 증명불가능하다. 그러므로 \(S_{\infty}\) 는 무모순이다. (체계가 모순적이면 모든 wff 가 증명 가능하다. 그러므로 체계의 무모순성은 증명불가능한 wff 의 존재성과 같다.) ■

• 서수 집합 \(\{\omega ,\omega ^{\omega }, \omega ^{\omega ^{\omega }},\dots \}\) 를 생각하자. 이 집합의 최소상계를 \(\epsilon_0\) 이라 정의한다.

  무모순성 정리의 가장 비구성적(non-constructive)인 측면은 보조정리 A.6 에서 사용된 초한귀납법이다. 주어진 서수까지의 초한귀납법의 원리는 겐첸과 Schutte 에 의하여 형식화되고 연구되었다. \(\epsilon_0\) 까지의 초한귀납법은 \(S\) 에서 도출될 수 없다.

  이 내용을 \(\mathsf{PA}\) 의 서수 분석에서 엄밀하게 알아본다.

  한편, 증명에 할당될 서수 모임에 대한 제한이 없으면 다음이 성립한다.

  1. \(S_{\infty}\) 는 \(\omega\)-무모순이다.
  2. 표준 모델에서 참인 \(S_{\infty}\) 의 모든 닫힌 wff 은 증명가능하다. 그러므로 \(S_{\infty}\) 는 완전하다.

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

  이 내용을 \(\mathsf{PA}\) 의 서수 분석에서 엄밀하게 알아본다.

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