AxiomaticSetTheory

Contents

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$ 로 표기하자.

모임(class)

모인은 특정한 성질을 만족하는 집합을 모은 것이다.

동등성(equality)

다음과 같이 정의한다.

$X = Y$ : $(\forall Z)(Z \in X \iff Z \in Y)$

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

포함(inclusion)

다음과 같이 정의한다.

$X \subseteq Y$ : $(\forall Z)(Z \in X \implies Z \in Y)$ (inclusion)
$X \subset Y$ : $X \subseteq Y \land X \neq Y$ (proper inclusion)

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

여기에서는 $\subset$ 를 진부분집합 관계를 뜻하는 용도로 사용하지만, 보통 $\subset$ 는 부분집합 관계를 뜻하는 용도로 사용된다.

NBG 집합론의 정리를 뜻하는 $\vdash _{\text{NBG}}$ 를 $\vdash$ 로 축약하여 사용하자.

정리 4.1

$\vdash X = Y \iff (X \subseteq Y \land Y \subseteq X)$
$\vdash X = X$
$\vdash X = Y \implies Y = X$
$\vdash X = Y \implies (Y = Z \implies X = Z)$

증명

Set, Proper Class✔

집합(set), 고유 모임(proper class)

$\operatorname{M} (X)$ : $(\exists Y)(X \in Y)$ ( $X$ 는 집합이다)
$\operatorname{Pr} (X)$ : $\neg \operatorname{M} (X)$ ( $X$ 는 고유 모임이다)

즉, 어떤 모임이 다른 모임에 속하면 집합이라고 한다. 그렇지 않은 모임를 고유 모임이라고 한다.
이제 이로써 이전의 집합론에서 발생했던 모순들이 더 이상 모순이 아니라 단지 다양한 클래스가 집합이 아니라 고유 모임임을 말해준다는 사실을 알게 된다.

문제 4.1

\vdash X \in Y \implies \operatorname{M} (X)

체계 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✔

문제 4.2 확장성 원리(extensionality principle)

\vdash X = Y \iff (\forall z)(z \in X \iff z \in Y)

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

Axiom T✔

공리 T(Axiom T)

X_1 = X_2 \implies (X_1 \in X_3 \iff X_2 \in X_3)

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

문제 4.3

\vdash \operatorname{M} (Z) \land Z = Y \implies \operatorname{M} (Y)

증명

정리 4.2

NBG 는 동등성을 지닌 1차 이론이다.

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

Axiom P - Pairing Axiom✔

공리 P(Axiom P - Pairing Axiom)

(\forall x)(\forall y)(\exists z)(\forall u)(u \in z \iff u = x \lor u = y)

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

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

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

Unordered Pair✔

문제 4.4 무순서쌍의 유일한 존재성(uniqueness existence of unordered pair)

\vdash (\forall x)(\forall y)(\exists _1z)(\forall u)(u \in z \iff u = x \lor u = y)

이때, $z$ 를 $\{x, y\}$ 라고 표기한다.

이 정리는 오직 $x$ 와 $y$ 만을 갖는 집합 $z$ 는 유일하다는 것을 말해준다.
증명

Axiom N - Null Set✔

공리 N(Axiom N - Null Set)

(\exists x)(\forall y)(y \not\in x)

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

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

공집합 상수(null set constant)

(\forall y)(y \not\in \varnothing)

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

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

문제 4.4 가 보장하는 $x$ 와 $y$ 의 무순서쌍에 새 함수 기호 $g(x, y)$ 를 도입할 수 있다. 관례를 따라 이것을 $\{x, y\}$ 라고 표기한다.

임의의 모임 $X$ 와 $Y$ 에 대한 $\{X, Y\}$ 의 유일한 값도 정의해야 한다. $X$ 가 집합이 아니거나 $Y$ 가 집합이 아닐 때 $\{X, Y\}$ 를 $\varnothing$ 이라고 한다.

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

$\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\})$

싱글톤(singleton)

$\{X, X\}$ 를 $\{X\}$ 라고 정의한다.

집합 $x$ 에 대하여 $\{x\}$ 를 $x$ 의 싱글톤이라고 한다. 이 집합은 오직 $x$ 를 원소로 갖는다.
정리 2.28 은 $\varnothing$ 이나 $\{X, Y\}$ 같은 새로운 개별 상수나 함수 기호를 추가하는 것이 NBG 이론에 본질적으로 아무런 영향을 미치지 않는다는 것을 말해준다.

Ordered Pair✔

순서쌍(ordered pair)

$\{\{X\},\{X,Y\}\}$ 를 $\left< X,Y \right>$ 라고 정의한다.

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

정리 4.3

\vdash (\forall x)(\forall y)(\forall u)(\forall v)(\left< x,y \right> = \left< u,v \right> \implies x = u \land y = v)

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

n-튜플(n-tuple)

\left< X \right> = X

\left< X_1, \dots, X_n, X _{n+1} \right> = \left< \left< X_1, \dots, X_n \right>, X _{n+1} \right>

즉, $\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✔

모임의 존재성 공리

$(B1) \quad (\exists X)(\forall u)(\forall v)(\left< u,v \right> \in X \iff u \in v)$ ( $\in$ -관계)

$(B2) \quad (\forall X)(\forall Y)(\exists Z)(\forall u)(u \in Z \iff u \in X \land u \in Y)$ (교집합)

$(B3) \quad (\forall X)(\exists Z)(\forall u)(u \in Z \iff u \not\in X)$ (여집합)

$(B4) \quad (\forall X)(\exists Z)(\forall u)(u \in Z \iff (\exists v)(\left< u, v \right> \in X))$ (정의역(domain))

$(B5) \quad (\forall X)(\exists Z)(\forall u)(\forall v)(\left< u, v \right> \in Z \iff u \in X)$

$(B6) \quad (\forall X)(\exists Z)(\forall u)(\forall v)(\forall w)(\left< u, v, w \right> \in Z \iff \left< v, w, u \right> \in X)$

$(B7) \quad (\forall X)(\exists Z)(\forall u)(\forall v)(\forall w)(\left< u, v, w \right> \in Z \iff \left< u, w, v \right> \in X)$

확장성의 원리를 사용하면 공리 $(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✔

교집합(intersection), 여집합(complement), 정의역(domain), 합집합(union), 보편 모임(universal class), 차집합(difference)

$X$ 와 $Y$ 의 교집합: $(\forall u)(u \in X \cap Y \iff u \in X \land u \in Y)$
$X$ 의 여집합: $(\forall u)(u \in \overline{X} \iff u \not\in X)$
$X$ 의 정의역: $(\forall u)(u \in \mathcal{D}(X) \iff (\exists v)(\left< u, v \right> \in X))$
$X$ 와 $Y$ 의 합집합: $X \cup Y = \overline{\overline{X} \cap \overline{Y}}$
보편적 모임: $V = \overline{\varnothing}$
$X$ 와 $Y$ 의 차집합: $X - Y = X \land \overline{Y}$

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

Predicative wff✔

술어적인 wff(predicative wff)

$X_1, \dots, X_n, Y_1, \dots, Y_m$ 중에서 변수를 갖는 wff $\phi (X_1, \dots, X_n, Y_1, \dots, Y_m)$ 에서 오직 집합 변수에만 양화사가 지칭되었다면 술어적인 wff 라고 한다.

예시

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

Class Existence Theorem✔

정리 4.4 모임 존재 정리(Class Existence Theorem)

술어적인 wff $\phi (X_1, \dots, X_n, Y_1, \dots, Y_m)$ 에 대하여 다음이 성립한다.

\vdash (\exists Z)(\forall x_1)\dots (\forall x_n)(\left< x_1, \dots, x_n \right> \in Z \iff \\ \phi (x_1, \dots, x_n, Y_1, \dots, Y_m))

증명
예시

$\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✔

데카르트 곱(Cartesian product), 관계(relation)

$Y_1$ 과 $Y_2$ 의 데카르트 곱 $Y_1 \times Y_2$ 을 다음과 같이 정의한다.

\begin{align}\begin{split} (\forall x)( &x \in Y_1 \times Y_2 \iff \\ & (\exists u)(\exists v)(x = \left< u, v \right> \land u \in Y_1 \land v \in Y_2))\\ \end{split}\end{align} \tag*{}

또한, 다음과 같이 정의한다.

$Y \times Y$ 를 $Y ^{2}$ 로 정의한다.
$n > 2$ 에 대하여 $Y ^{n-1} \times Y$ 를 $Y ^{n}$ 로 정의한다.
이항관계 $X$ 에 대하여 $X \subseteq V ^{2}$ 를 $\operatorname{Rel} (X)$ 로 정의한다.

$V ^{2}$ 는 모든 순서쌍의 모임이다.
관계란 대상 간의 어떤 연결을 의미한다. 수학에서 관계는 순서쌍 $\left< u,v \right>$ 로 표현된다.

Power Class, Sum Class, Identity Relation✔

멱 모임(power class)

다음을 만족하는 $\operatorname{P} (Y)$ 를 $Y$ 의 멱 모임이라 한다.

(\forall x)(x \in \operatorname{P} (Y) \iff x \subseteq Y)

$\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)$ 라고 표기한다.

합 모임(sum class)

$Y$ 의 합 모임 $\bigcup_{}^{}Y$ 를 다음과 같이 정의한다.

(\forall x)(x \in \bigcup_{}^{}Y \iff (\exists v)(x \in v \land v \in 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$ 라고 표기한다.

항등 관계(identity relation)

다음을 만족하는 모임 $I$ 를 항등 관계라고 한다.

(\forall x)(x \in I \iff (\exists u)(x = \left< u, u \right>))

$\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$ 라고 표기한다.

따름정리 4.5

$\phi (X_1, \dots, X_n, Y_1, \dots, Y_m)$ 이 술어적 wff 이면 다음이 성립한다.

\begin{align}\begin{split} &\vdash (\exists _1W)\bigg (W \subseteq V ^{n} \land (\forall x_1)\dots (\forall x_n)\Big (\left< x_1, \dots, x_n \right>\in W \iff \\ &\qquad \qquad \qquad \phi (x_1, \dots, x_n,Y_1, \dots, Y_m)\Big )\bigg ) \end{split}\end{align} \tag*{}

증명

Inverse Relation, Range✔

어떤 술어적인 wff $\phi (X_1, \dots, X_n, Y_1, \dots, Y_m)$ 에 대하여

\{\left< x_1, \dots, x_n \right> : \phi (x_1, \dots, x_n, Y_1, \dots, Y_m)\}

를 $\phi (x_1, \dots, x_n, Y_1, \dots, Y_m)$ 를 만족하는 모든 n-튜플 $\left< x_1, \dots, x_n \right>$ 의 모임으로 정의한다.

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

$(\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✔

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

공리 U(Axiom U - Sum Set)

(\forall x)(\exists y)(\forall u)(u \in y \iff (\exists v)(u \in v \land v \in x))

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

$\vdash (\forall x)\operatorname{M} \left(\bigcup x\right)$
집합 $x$ 안의 모든 집합의 합집합 $\bigcup x$ 를 보통 다음과 같이 표기한다.

$\bigcup_{v \in x}^{} v$

Axiom W - Power Set✔

공리 W(Axiom W - Power Set)

(\forall x)(\exists y)(\forall u)(u \in y \iff u \subseteq x)

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

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

$\vdash (\forall x)\operatorname{M} (\operatorname{P} (x))$

Axiom S - Subsets✔

공리 S(Axiom S - Subsets)

(\forall x)(\forall Y)(\exists z)(\forall u)(u \in z \iff u \in x \land u \in Y)

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

따름정리 4.6

$\vdash (\forall x)(\forall Y)\operatorname{M} (x \cap Y)$ (집합과 모임의 교집합은 집합이다.)
$\vdash (\forall x)(\forall Y)(Y \subseteq x \implies \operatorname{M} (Y))$ (집합의 부분모임은 집합이다.)
임의의 술어적인 wff $B(y)$ 에 대하여 $\vdash (\forall x)\operatorname{M} (\{y : y \in x \land B(y)\})$ .

증명

교집합(intersection)

$\bigcap X$ 를 다음과 같이 정의한다.

\{y : (\forall x)(x \in X \implies y \in x)\}

정리 4.7

$\vdash (\forall x)(x \in X \implies \bigcap X \subseteq x)$
$\vdash X \neq \varnothing \implies \operatorname{M} \left( \bigcap X\right)$
$\vdash \bigcap \varnothing= V$

증명

Function, Restriction, Injection✔

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

함수(function), 제한(restriction), 단사 함수(injection, one-to-one function)

$\operatorname{Fnc} (X)$ : $X$ 는 함수이다.

$\begin{align}\begin{split} \operatorname{Rel} (X) \land (\forall x)(\forall y)(\forall z)(& \left< x, y \right> \in X \land\\ & \left< x, z \right> \in X \implies y = z)\\ \end{split}\end{align} \tag*{}$
$X:Y \to Z$ : $X$ 는 $Y$ 에서 $Z$ 로 가는 함수이다.

$\operatorname{Fnc} (X) \land \mathcal{D}(X) = Y \land \mathcal{R}(X) \subseteq Z$
$Y \mathord{\downharpoonright} X$ : $X$ 의 정의역을 $Y$ 로 제한한 것.

$X \cap (Y \times V)$
$\operatorname{Fnc} _1(X)$ : $X$ 는 단사 함수이다.

$\operatorname{Fnc} (X) \land \operatorname{Fnc} (\breve{X})$
$X'Y = \begin{cases} z & (\forall u)(\left< Y, u \right> \in X \iff u = z)\\ \varnothing & \text{else} \\ \end{cases}$
$X''Y = \mathcal{R}(Y \mathord{\downharpoonright} X)$

$\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(Axiom R - Replacement)

\begin{align}\begin{split} &\operatorname{Fnc} (Y) \implies (\forall x)(\exists y)(\forall u)\big ( \\ & \qquad u \in y \iff (\exists v)(\left< v,u \right> \in Y \land v \in x)\big ) \\ \end{split}\end{align} \tag*{}

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

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

Axiom I - Axiom of Infinity✔

공리 I(Axiom I - Axiom of Infinity)

(\exists x)(\varnothing \in x \land (\forall u)(u \in x \implies u \cup \{u\}\in x))

무한집합의 존재성을 위해서는 본 공리가 필요하다.
공리 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✔

비반사(irreflexive), 추이적 관계(transitive), 부분순서(partially order), 연결 관계(connected relation), 전순서(totally order), 정렬순서(well-order)

각각 아래의 wff 를 다음과 같이 정의한다.

$X \operatorname{Irr}Y$ : $X$ 는 $Y$ 에 대한 비반사 관계이다.

$\operatorname{Rel} (X) \land (\forall y)(y \in Y \implies \left< y, y \right> \not\in X)$
$X \operatorname{Tr}Y$ : $X$ 는 $Y$ 에 대한 추이적 관계이다.

$\begin{align}\begin{split} \operatorname{Rel} (X) \land (\forall u)(\forall v)(\forall w)(& [u \in Y \land v \in Y \land \\ & w \in Y \land \left< u, v \right> \in X \land \left< v, w \right> \in X] \\ & \implies \left< u, w \right> \in X) \\ \end{split}\end{align} \tag*{}$
$X \operatorname{Part}Y$ : $X$ 는 $Y$ 에 대한 부분순서이다.

$(X \operatorname{Irr}Y) \land (X \operatorname{Tr}Y)$
$X \operatorname{Con}Y$ : $X$ 는 $Y$ 에 대한 연결 관계이다.

$\begin{align}\begin{split} \operatorname{Rel} (X) \land (\forall u)(\forall v)(& [u \in Y \land v \in Y \land u \neq v] \implies \\ & \left< u, v \right> \in X \lor \left< v, u \right> \in X) \\ \end{split}\end{align} \tag*{}$
$X \operatorname{Tot}Y$ : $X$ 는 $Y$ 에 대한 전순서이다.

$(X \operatorname{Irr}Y) \land (X \operatorname{Tr}Y) \land (X \operatorname{Con}Y)$
$X \operatorname{We}Y$ : $X$ 는 $Y$ 에 대한 정렬순서이다. 즉, 관계 $X$ 가 $Y$ 에 대하여 비반사이고, 공집합이 아닌 모든 $Y$ 의 부분모임이 $X$ 의 순서관계에 의한 최소 원소를 갖는다.

$\begin{align}\begin{split} (X \operatorname{Irr}Y) \land (\forall Z)\bigg (&[Z \subseteq Y \land Z \neq \varnothing] \implies (\exists y)\Big (y \in Z \land \\ &\enspace (\forall v)\big (v \in Z \land v \neq y \implies \\ & \qquad \left< y, z \right> \in X \land \left< v, y \right> \not\in X \big )\Big )\bigg ) \\ \end{split}\end{align} \tag*{}$

예시

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

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

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

Similar Order✔

유사성 사상(similarity mapping)

$\operatorname{Simp}(Z, W_1, W_2)$ : $Z$ 는 $x_1$ 위의 관계 $r_1$ 을 $x_2$ 위의 관계 $r_2$ 로 보내는 유사성 사상이다.

\begin{align}\begin{split} (\exists x_1)(\exists x_2)&(\exists r_1)(\exists r_2)( \operatorname{Rel} (r_1) \land \operatorname{Rel} (r_2) \land \\ & W_1 = \left< r_1, x_1 \right> \land W_2 = \left< r_2, x_2 \right> \land \\ & \operatorname{Fnc} _1(Z) \land \mathcal{D}(Z) = x_1 \land \mathcal{R}(Z) = x_2 \land \\ & (\forall u)(\forall v)(u \in x_1 \land v \in x_1 \implies \\ & \qquad \qquad (\left< u,v \right> \in r_1 \iff \left< Z'u , Z'v \right> \in r_2)))\\ \end{split}\end{align} \tag*{}

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

유사 순서 구조(similar ordered structure)

$\operatorname{Sim}(W_1, W_2)$ : $W_1$ 와 $W_2$ 는 유사 순서 구조이다.

(\exists z)\operatorname{Simp}(z, W_1, W_2)

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

음이 아닌 정수 집합 $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✔

합성(composition)

$X_1 \circ X_2$ : $X_2$ 와 $X_1$ 의 합성.

\{\left< u,v \right> : (\exists z)(\left< u, z \right> \in X_2 \land \left< z, v \right> \in X_1)\}

역(field), 전순서 관계(total order relation), 정렬 관계(well-ordering relation)

$\operatorname{Fld}(X)$ : $X$ 는 역이다.

$\mathcal{D}(X) \cup \mathcal{R}(X)$
$\operatorname{TOR}(X)$ : $X$ 는 전순서 관계이다.

$\operatorname{Rel} (X) \land (X \operatorname{Tot}(\operatorname{Fld}(X)))$
$\operatorname{WOR}(X)$ : $X$ 는 정렬 순서 관계이다.

$\operatorname{Rel} (X) \land (X \operatorname{We}(\operatorname{Fld}(X)))$

Ordinal Class, Ordinal Number✔

순서형(order type)

전순서 $x$ 에 대하여 $x$ 와 유사한 모든 전순서 모임을 $x$ 의 순서형이라고 한다.

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

포함 관계(소속 관계, membership relation), 추이적(transitive), 절단(section), 절편(segment)

$E$ : 포함 관계

$\{\left< x, y \right> : x \in y\}$
$\operatorname{Trans}(X)$ : $X$ 는 추이적이다.

$(\forall u)(u \in X \implies u \subseteq X)$
$\operatorname{Sect}_{Y}(X, Z)$ : $Z$ 는 $X$ 의 $Y$ -절단이다.

$\begin{align}\begin{split} Z \subseteq X \land (\forall u)(\forall v)(&[u \in X \land v \in Z \land \left< u,v \right> \in Y] \\ & \implies u \in Z)\\ \end{split}\end{align} \tag*{}$
$\operatorname{Seg}_{Y}(X, W)$ : $Z$ 는 $W$ 에 의한 $Y$ -절편이다.

$\{x : x \in X \land \left< x, W \right> \in Y \}$

순서수 모임(ordinal class), 순서수의 모임(class of ordinal number), 순서수(ordinal number)

$\operatorname{Ord}(X)$ : $X$ 는 순서수 모임이다. 즉, $\in$ -관계(포함 관계)가 $X$ 를 정렬하고, $X$ 의 임의의 원소가 $X$ 의 부분집합이다.

$E \operatorname{We}X \land \operatorname{Trans}(X)$
$\operatorname{On}$ : 모든 순서수의 모임.

$\{x : \operatorname{Ord}(x)\}$

집합인 순서수 모임을 순서수라고 한다.

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

이제 $\alpha,\beta,\gamma ,\delta,\tau,\dots$ 로 순서수를 나타내자. 즉, 다음과 같이 정의한다.

$(\forall \alpha)B(\alpha)$ 는 $(\forall x)(x \in \operatorname{On}\implies B(x))$ 의 축약이다.
$(\exists \alpha)B(\alpha)$ 는 $(\exists x)(x \in \operatorname{On}\land B(x))$ 의 축약이다.

정리 4.8

$\vdash \operatorname{Ord}(X) \implies (X \not\in X \land (\forall u)(u \in X \implies u \not\in u))$
$\vdash \operatorname{Ord}(X) \land Y \subset X \land \operatorname{Trans}(Y) \implies Y \in X$
$\vdash \operatorname{Ord}(X) \land \operatorname{Ord}(Y) \implies (Y \subset X \iff Y \in X)$
$\operatorname{Ord}(X) \land \operatorname{Ord}(Y) \implies [(X \in Y \lor X = Y \lor Y \in X) \land \neg (X \in Y \land Y \in X) \land \neg (X \in Y \land X = Y)]$
$\vdash \operatorname{Ord}(X) \land Y \in X \implies Y \in \operatorname{On}$
$\vdash E \operatorname{We}\operatorname{On}$
$\vdash \operatorname{Ord}(\operatorname{On})$
$\vdash \neg \operatorname{M} (\operatorname{On})$
$\vdash \operatorname{Ord}(X) \implies X = \operatorname{On}\lor X \in \operatorname{On}$
$\vdash y \subseteq \operatorname{On}\land \operatorname{Trans}(y) \implies y \in \operatorname{On}$
$x \in \operatorname{On}\land y \in \operatorname{On}\implies (x \subseteq y \lor y \subseteq x)$

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

다음과 같이 정의한다.

$x <_o y$ : $x \in \operatorname{On}\land y \in \operatorname{On}\land x \in y$
$x \leq _o y$ : $y \in \operatorname{On}\land ( x = y \lor x <_o y)$

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

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

Transfinite Induction✔

정리 4.9 초한귀납법(Transfinite Induction)

\vdash (\forall \beta)\big [ (\forall \alpha)(\alpha \in \beta \implies \alpha \in X) \implies \beta \in X \big] \implies \operatorname{On}\subseteq X

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

만약, 모든 서수 $\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$ 에 속한다. 이는 모순이다. ■

정리 4.10

$x'$ 를 $x \cup \{x\}$ 로 정의하자.

다음이 성립한다.

$\vdash (\forall x)(x \in \operatorname{On}\iff x' \in \operatorname{On})$
$\vdash (\forall \alpha)\neg (\exists \beta)(\alpha <_o \beta <_o \alpha')$
$\vdash (\forall \alpha)(\forall \beta)(\alpha' = \beta' \implies \alpha = \beta)$

증명

다음수 서수(successor ordinal), 제1종 서수(first kind ordinal)

$\operatorname{Suc}(X)$ : $X$ 는 다음수 서수이다.

$X \in \operatorname{On}\land (\exists \alpha)(X = \alpha')$
$K_1$ : 제1종 서수의 모임.

$\{x : x = \varnothing \lor \operatorname{Suc}(x) \}$
$\omega$ : 제1종 서수 $\alpha$ 에 대하여 $\alpha$ 보다 작은 모든 서수도 제1종일 때 모든 서수 $\alpha$ 의 모임.

$\{x : x \in K_1 \land (\forall u)(u \in x \implies u \in K_1)\}$

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

$\vdash \varnothing \in \omega \land 1 \in \omega$

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

정리 4.11

$\vdash (\forall \alpha)(\alpha \in \omega \iff \alpha' \in \omega )$
$\vdash \operatorname{M} (\omega )$
$\vdash \varnothing \in X \land (\forall u)(u \in X \implies u' \in X) \implies \omega \subseteq X$
$\vdash (\forall \alpha)(\alpha \in \omega \land \beta <_o \alpha \implies \beta \in \omega )$

증명

유한 서수(finite ordinal)

$\omega$ 의 원소를 유한 서수라고 한다.

또한, 다음과 같이 정의한다.

$1$ 을 $\varnothing'$ 으로 정의한다.
$2$ 를 $1'$ 으로 정의한다.
$3$ 를 $2'$ 으로 정의한다.
$\dots$

그러므로 $\varnothing \in \omega , 1 \in \omega , 2 \in \omega , \dots$ 이다.

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

극한 서수(limit ordinal)

$\operatorname{Lim}(x)$ : $x$ 는 극한 서수이다.

x \in \operatorname{On}\land x \not\in K_1

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

정리 4.12

$x$ 가 서수 집합이면, $\bigcup x$ 는 $x$ 의 최소 상계인 서수이다.

$\begin{align}\begin{split} \vdash (\forall x)&\Bigg (x \subseteq \operatorname{On}\implies \bigg [\bigcup x \in \operatorname{On}\land (\forall \alpha)\Big (\alpha \in x \implies \\ & \alpha \leq _o \bigcup x \Big ) \land (\forall \beta) \Big ((\forall \alpha ) \big (\alpha \in x \implies \\ & \alpha \leq _o \beta \big ) \implies \bigcup x \leq _o \beta \Big )\bigg ] \Bigg ) \\ \end{split}\end{align} \tag*{}$
$x$ 가 최대 원소가 없는 공집합이 아닌 서수 집합이면, $\bigcup x$ 은 극한 서수이다.

$\begin{align}\begin{split} \vdash (\forall x)\bigg (&x \subset \operatorname{On}\land x \neq \varnothing \land (\forall \alpha )\Big (\alpha \in x \implies \\ & (\exists \beta)\big (\beta \in x \land \alpha <_o \beta \big ) \Big ) \implies \operatorname{Lim}\Big (\bigcup x \Big )\bigg ) \\ \end{split}\end{align} \tag*{}$

증명

정리 4.13 초한귀납법: 두번째 형태(Transfinite Induction: Second Form)

$\vdash \Big [\varnothing \in X \land (\forall \alpha )(\alpha \in X \implies \alpha ' \in X) \land (\forall \alpha )\big (\operatorname{Lim}(\alpha ) \land \\ \qquad (\forall \beta )(\beta <_o \alpha \implies \beta \in X) \implies \alpha \in X \big )\Big ] \implies \operatorname{On}\subseteq X$
$\delta$ 까지의 귀납법

$\begin{align}\begin{split} & \vdash \Big [\varnothing \in X \land (\forall \alpha )(\alpha <_o \delta \land \alpha \in X \implies \alpha ' \in X) \land \\ &\qquad (\forall \alpha )\big (\alpha <_o \delta \land \operatorname{Lim}(\alpha )\land (\forall \beta )(\beta <_o \alpha \implies \\ &\qquad \beta \in X) \implies \alpha \in X \big )\Big ]\implies \delta \subseteq X \\ \end{split}\end{align} \tag*{}$
$\omega$ 까지의 귀납법

$\begin{align}\begin{split} \vdash & \varnothing \in X \land (\forall \alpha )(\alpha <_o \omega \land \alpha \in X \implies \alpha ' \in X) \\ & \implies \omega \subseteq X \\ \end{split}\end{align} \tag*{}$

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

정리 4.14

주어진 $X$ 에 대하여 $\alpha$ 에서 $Y$ 의 값이 $\alpha$ 보다 작은 서수 집합에 대한 $Y$ 의 제한을 적용한 $X$ 의 값이 되도록 모든 서수 위에서 정의된 유일한 함수 $Y$ 가 존재한다.

$\begin{align}\begin{split} \vdash (& \forall X)(\exists _1Y)\Big (\operatorname{Fnc} (Y) \land \\ & \mathcal{D}(Y) = \operatorname{On}\land (\forall \alpha )\big (Y'\alpha = X' (\alpha \mathord{\downharpoonright} Y) \big )\Big ) \\ \end{split}\end{align} \tag*{}$
$\vdash (\forall x)(\forall X_1)(\forall X_2)(\exists _1Y) \Big ( \operatorname{Fnc} (Y) \land \mathcal{D}(Y) = \operatorname{On}\land \\ Y'\varnothing =x \land (\forall \alpha )\big ( Y'(\alpha ') = X'_1 (Y'\alpha ) \big ) \land \\ (\forall \alpha )\big (\operatorname{Lim}(\alpha )\implies Y'\alpha =X'_2 (\alpha \mathord{\downharpoonright} Y)\big ) \Big )$
$\delta$ 까지의 귀납법

$\begin{align}\begin{split} \vdash (\forall x)(&\forall X_1)(\forall X_2)(\exists _1Y)\Big (\operatorname{Fnc} (Y) \land \mathcal{D}(Y) = \delta \land Y'\varnothing =x \land \\ &(\forall \alpha )\big (\alpha ' <_o \delta \implies Y'(\alpha ') = X'_1(Y'\alpha )\big ) \land \\ & (\forall \alpha) \big (\operatorname{Lim}(\alpha )\land \alpha <_o \delta \implies Y'\alpha = X'_2 (\alpha \mathord{\downharpoonright} Y)\big )\Big ) \\ \end{split}\end{align} \tag*{}$

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

서수 덧셈. 본 정리 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)$
증명

임의의 모임 $X$ 에 대하여 $E_X$ 를 $X$ 로 제한된 포함 관계라고 정의한다.

E_X = \{\left< u,v \right> : u \in v \land u \in X \land v \in X\}

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}$ 에 적용된다.

체계 $S_{\infty}$ (system $S_{\infty}$ )

$S_{\infty}$ 의 기호는 다음과 같이 정의된다. 이 기호의 정의에 의하여 $S$ 와 $S _{\infty}$ 는 같은 항을 갖고, 그러므로 같은 원자식(항 $s$ 와 $t$ 에 대한 식 $s=t$ )을 갖는다.

기호: $S _{\infty}$ 는 $S$ 처럼 개별 상수 $0$ 과 함수 기호 $+$ , $\cdot$ , $'$ 와 술어 기호 $=$ 를 갖는다.

$S_{\infty}$ 의 연결사와 wff 는 다음과 같이 정의된다. 이 정의에 의하여 $S$ 의 모든 wff 가 $S_{\infty}$ 의 wff 의 축약이 된다.

연결사: $S$ 가 기본 연결사로 $\implies$ 과 $\neg$ 을 가진 것에 비해 $S_{\infty}$ 의 원시 명제 연결사는 $\lor$ 과 $\neg$ 이다. $A \implies B$ 는 $(\neg A)\lor B$ 로 정의한다.
wff: $S_{\infty}$ 의 wff 를 유한하게 연결사 $\lor$ 와 $\neg$ 과 양화사 $(\forall x_i)$ 를 원자식에 적용하여 얻은 식으로 정의한다.

닫힌 원자 wff $s = t$ 에 대하여 $+$ 와 $\cdot$ 의 모든 재귀식을 풀어서 $s$ 와 $t$ 의 값을 계산했을 때 두 값이 같으면 $s = t$ 가 옳다(correct)고 하고, 그렇지 않으면 $s = t$ 가 틀리다(incorrect)고 하자.

다음을 $S_{\infty}$ 의 공리로 정의한다. $S_{\infty}$ 의 모든 공리가 닫힌 wff 이고, 추론 규칙은 닫힌 전제를 닫힌 결과로 보내기 때문에 $S_{\infty}$ 의 모든 정리는 닫힌 wff 이다.

공리:
1. 모든 옳은 닫힌 원자 wff
2. 모든 틀린 닫힌 원자 wff 의 부정

$S_{\infty}$ 는 다음과 같은 추론규칙을 갖는다. 선 위의 wff 들이 전제이고 선 아래의 wff 가 결론이다.

약한 규칙(weak rule)
1. 교환(exchange): $\dfrac{C \lor A \lor B \lor D}{C \lor B \lor A \lor D}$
2. 합병(consolidation): $\dfrac{A \lor A \lor D}{A \lor D}$
강한 규칙(strong rule)
1. 희석(dilution): 임의의 닫힌 wff $A$ 에 대하여 $\dfrac{D}{A \lor D}$
2. 드모르간(De Morgan): $\dfrac{\neg A \lor D \quad \neg B \lor D}{\neg (A \lor B) \lor D}$
3. 부정(negation): $\dfrac{A \lor D}{\neg \neg A \lor D}$
4. 양화(quantification): 닫힌 항 $t$ 에 대하여 $\dfrac{\neg A(t) \lor D}{(\neg (\forall x) A (x)) \lor D}$
5. 무한 귀납(infinite induction): 모든 자연수 $n$ 에 대하여 $\dfrac{A (\overline{n}) \lor D}{((\forall x) A(x)) \lor D}$
절단(cut): $\dfrac{C \lor A \quad \neg A \lor D}{C \lor D}$

wff $C$ 와 $D$ 를 사이드(side) wff 라고 하며, 사이드 wff 는 생략될 수 있다. wff $A$ 와 $B$ 들, 즉 사이드 wff 가 아닌 wff 를 주요(principal) wff 라고 한다.

절단의 주요 wff $A$ 를 절단 wff 라고 하고, $\neg A$ 안에서 연결사와 양화사의 갯수를 절단의 차수(degree)라고 한다.

명백히 주어진 닫힌 원자 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)}$ 는 드모르간의 법칙이다.

G-트리(G-tree)

G-트리를 다음과 같은 그래프로 정의하자.

단계 $0$ 에는 종점(terminal point)라고 불리는 단일 점이 있다.
각 단계 $i+1$ 의 점은 단계 $i$ 의 단 하나의 점과 연결된다.
단계 $i$ 의 각 점 $P$ 는 단계 $i+1$ 의 $0$ 개, 또는 $1$ 개, 또는 가산 무한히 많은 점과 연결된다. 이때, 단계 $i+1$ 의 점을 $P$ 의 선행자(predecessor)라고 한다.
단계 $i$ 의 각 점은 오직 단계 $i-1$ 나 $i+1$ 의 점과 연결된다.
선행자를 갖지 않는 점을 초기점(initial point)이라고 한다.

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

$A,B,C,D$ 가 초기점이고 $E$ 가 종점이다.
예시

$A,B,C_1, C_2, \dots$ 가 초기점이고 $E$ 가 종점이다.
예시

$A$ 가 유일한 초기점이고, $E$ 가 종점이다.

증명 트리(proof-tree), 증명(proof), 정리(theorem)

증명 트리로써 $S_{\infty}$ 의 wff 를 G-트리의 점에 다음과 같이 할당한다.

초기점에 할당되는 wff 는 $S_{\infty}$ 의 공리이다.
비초기점 $P$ 와 $P$ 의 선행자에 할당되는 wff 는 각각 어떤 추론 규칙의 결론과 전제이다.

(증명 트리의 차수) 증명 트리에서 나타나는 절단의 차수의 최댓값이 존재한다. 이 최댓값을 증명 트리의 차수라고 한다. 만약 절단이 나타나지 않으면 차수를 $0$ 이라고 정의한다.

다음과 같이 증명 트리의 wff 에 서수를 할당한다.

약한 규칙의 결론의 서수는 전제의 서수와 같다.
강한 규칙이나 절단의 결론의 서수는 전제의 서수보다 크다.

(증명 트리의 서수) 증명 트리의 종점에 할당되는 wff 를 끝 wff 라고 하자. 끝 wff 의 서수를 증명 트리의 서수라고 한다.

(증명 트리의 스레드) 증명 트리의 스레드(thread)는 유한 또는 가산무한의 wff 열 $A_1, A_2, \dots$ 이다. $A_1$ 는 끝 wff 이고, 각 wff $A _{i+1}$ 는 $A_i$ 의 선행자이다. 스레드의 각 wff 에 부여된 서수 $\alpha _1, \alpha _2, \dots$ 는 증가하지 않으며, 강한 규칙이나 절단이 적용된 단계에서 감소한다.

이제 $S_{\infty}$ 의 증명과 정리를 다음과 같이 정의한다.

증명 트리는 끝 wff 의 증명이다.
$S_{\infty}$ 의 정리는 증명 트리의 끝 wff 에 대한 wff 들로 정의된다.

서수의 열이 가산무한히 감소할 수 없으므로 스레드에 강한 규칙이나 절단이 오직 유한하게만 존재한다. 또한 주어진 wff 에 대하여 약한 규칙이 오직 유한하게 필요하다. 그러므로 증명 트리의 모든 스레드의 약한 규칙의 연속적인 적용은 오직 유한하다고 할 수 있다. 그러므로 증명 트리의 모든 스레드는 유한하다.
증명 트리의 wff 에 할당될 서수의 모임을 제한하면, 이는 증명 트리의 개념을 제한하고, 그러므로 더 작은 정리 집합을 얻게 된다.

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

보조정리 A.1

$n$ 개의 연결사와 양화사를 갖는 닫힌 wff $A$ 를 잡자. 그러면 절단이 사용되지 않고 서수가 $\leq 2n + 1$ 인 $\neg A \lor A$ 의 증명이 존재한다.

증명

$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$ 의 증명을 얻는다.
■

보조정리 A.2

임의의 닫힌 항 $t$ 와 $s$ , 그리고 오직 $x$ 를 자유변수로 갖는 임의의 wff $A(x)$ 에 대하여 wff $s \neq t \lor \neg A(s) \lor A(t)$ 는 $S_{\infty}$ 의 정리이고 절단 규칙 없이 증명가능하다.

증명

일반적으로 $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)$ 는 정리이다. ■

보조정리 A.3

$S$ 의 정리인 모든 닫힌 wff 는 $S_{\infty}$ 의 정리이다.

증명

$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}

$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})$
$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$ 이다. ■

따름정리 A.4

$S_{\infty}$ 가 무모순이면 $S$ 도 무모순이다.

$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.5

드모르간의 법칙, 부정, 무한 귀납은 가역이다. 즉, 어떤 전제의 귀결인 wff 의 증명으로부터 이들 규칙을 통하여 전제의 증명을 얻을 수 있다. 이 증명의 서수와 차수는 원래의 증명의 서수와 차수보다 크지 않다.

증명

드모르간:

$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.6 (Schutte 1951: Reduktionssatz)

$S_{\infty}$ 안에서 양의 차수 $m$ 과 서수 $\alpha$ 를 갖는 어떤 증명 $A$ 에 대하여 그것보다 낮은 차수와 서수 $2 ^{\alpha }$ 를 갖는 $S_{\infty}$ 안에서의 $A$ 의 증명이 존재한다.

증명

주어진 $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$ 의 형태에 따른 조사를 해야 한다.

$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$ 보다는 작다.

$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 }$ 이다.

$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 }$ 로 잡을 수 있다.

$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 }$ 까지 올릴 수 있다. ■

따름정리 A.7

서수 $\alpha$ 와 차수 $m$ 의 $A$ 의 모든 증명은 서수 $2 ^{2 ^{\rddots ^{2 ^{\alpha }}}}$ 와 차수 $0$ 을 갖는 증명으로 대체될 수 있다.

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

정리 A.8

$S_{\infty}$ 는 무모순이다.

증명

$(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$ 라는 것을 확인하자.

Mendelson, E. (2009). Introduction to mathematical logic. CRC Press.

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