OrdinalAnalysis Arai

부정표준형(negation normal form)

부정표준형인 식이란 \(\implies\) 가 나타나지 않고 \(\neg\) 이 오직 원자식(atomic formula)에만 적용되어 있는 식이다.

리터럴(literal)

리터럴이란 원자식을 뜻한다. 즉, 항 \(t_1, \dots, t_n\) 에 대한 식 \(R(t_1, \dots, t_n)\), \(\overline{R}(t_1, \dots, t_n)\) 이다.

부정(negation)

식 \(A\) 에 대한 부정 \(\neg A\) 을 다음과 같이 드모르간의 법칙과 이중 부정 제거에 의하여 재귀적으로 정의한다.

1. 리터럴 \(L\) 에 대하여 \(\neg L : \equiv \overline{L}\).

2. \(\neg (A \lor B) : \equiv \neg A \land \neg B\)

   \(\neg (A \land B) : \equiv \neg A \lor \neg B\)

3. \(\neg \exists xA(x) : \equiv \forall x \neg A(x)\)

   \(\neg \forall xA(x) : \equiv \exists x \neg A(x)\)

R-positive, R-negative

술어 \(R\) 에 대하여 positive 인 식, 또는 \(R\)-positive 인 식을 \(\overline{R}\) 이 나타나지 않은 식으로 정의한다.

\(R\) 이 나타나지 않은 식은 \(R\)-negative 라고 정의한다.

시퀀트(sequent)

식의 유한 집합 \(\{A_0, \dots, A _{n-1}\}\) 을 시퀀트(sequent)라고 한다. 이는 \(\bigvee_{i<n}^{}A_i\) 를 뜻한다. 따라서 빈 시퀀트는 거짓을 뜻한다.

시퀀트 \(\Gamma\) 와 \(\Delta\), 식 \(A\) 에 대하여 다음과 같이 정의한다.

• \(\Gamma,\Delta := \Gamma \cup \Delta\)
• \(\Gamma,A := \Gamma \cup \{A\}\)

\(\bm{G}_1\): 일방적 시퀀트 계산(one-sided sequent calculi)

고전 1차 논리에 대한 일방적 시퀀트 계산 \(\bm{G}_1\) 은 약한 규칙(교환, 합병)이 없는 시퀀트 계산이다. \(\bm{G}_1\) 을 다음과 같이 정의한다.

• 공리: 임의의 시퀀트 \(\Gamma\) 와 리터럴 \(L\) 에 대하여 다음과 같다.

  \[ \Gamma ,\overline{L},L \]

• 명제 연결사 \(\lor ,\land\) 에 대한 추론규칙:

  \[ \dfrac{\Gamma,A_0 \lor A_1, A_i}{\Gamma,A_0 \lor A_1}\enspace (\lor )_i \quad (i = 0,1)\]
  \[ \dfrac{\Gamma,A_0 \land A_1, A_0 \quad \Gamma,A_0 \land A_1,A_1}{\Gamma,A_0 \land A_1}\enspace (\land )\]

  규칙 \((\lor )\) 를 규칙 \((\lor )_i\) 중 하나를 뜻하는 것으로 표현하자. 그러므로 \((\lor )\) 를 두번 적용하면 다음이 성립한다.

  \[ \dfrac{\Gamma,A_0 \lor A_1, A_0,A_1}{\Gamma,A_0 \lor A_1}\enspace (\lor ) _{01}\]

• 양화사 \(\exists ,\forall\) 에 대한 추론규칙:

  \[ \dfrac{\Gamma,\exists xA(x), A(t)}{\Gamma,\exists xA(x)}\enspace (\exists ) \]
  \[ \dfrac{\Gamma,\forall xA(x), A(a)}{\Gamma,\forall xA(x)}\enspace (\forall ) \]

  \((\forall )\) 에서 자유변수 \(a\) 가 하시퀀트(lower sequent) \(\Gamma,\forall xA(x)\) 에서 나타나지 않는데, 이를 추론규칙 \((\forall )\) 의 고유변수(eigenvariable) 라고 한다.

하시퀀트의 식을 주요식(principal formula)이라고 한다. 각각 \(A_0 \lor A_1\), \(A_0 \land A_1\), \(\exists xA(x)\), \(\forall xA(x)\) 가 주요식이다.

상시퀀트(upper sequent)의 식을 보조식(auxiliary formula)이라고 한다. \((\lor)\) 와 \((\land )\) 에서 \(A_i\) 가 보조식이다. \((\exists)\) 에서 \(A(t)\) 가 보조식이고 \((\forall)\) 에서 \(A(a)\) 가 보조식이다.

• \(\bm{G}_1\) 의 추론규칙이 아닌 절단(cut) 규칙:

  \[ \dfrac{\Gamma,\neg C \quad C,\Delta}{\Gamma,\Delta}\enspace (cut) \]

  \(C\) 를 절단식(cut formula)이라고 한다.

시퀀트 계산 \(\bm{G}\) 의 증명

\(\bm{G}\) 를 두 계산 \(\bm{G}_1 (+(cut))\), 즉, 절단이 있는 \(\bm{G}_1\) 과 없는 \(\bm{G}_1\) 중 하나라고 하자. \(\bm{G}\) 의 증명은 \(\bm{G}\) 의 공리와 추론규칙으로 형성되는 쉬퀸트의 유한 이진 트리이다.

증명이란 이진트리의 끝시퀸트(endsequent) \(\Gamma\) 의 증명이고, 이 경우 \(\bm{G} \vdash \Gamma\) 라고 표기한다.

\(\bm{G}_1 +(cut)\) 안에서의 증명에 절단이 없으면 cut-free 라고 한다.

명제 1.1 \(\bm{G}_1+(cut)\) 의 건전성(soundness)

\(\bm{G}_1 +(cut)\) 안에서 증명가능한 시퀸트는 타당하다.

정의 1.1 차수(degree)

식 \(A\) 의 차수 \(\operatorname{dg} (A)\) 를 다음과 같이 정의한다.

1. 리터럴 \(L\) 에 대하여 \(\operatorname{dg} (L) = 0\).
2. \(\operatorname{dg} (A_0 \lor A_1) = \operatorname{dg} (A_0 \land A_1) = \max \{\operatorname{dg} (A_i) : i = 0, 1\} + 1\).
3. \(\operatorname{dg} (\exists xA(x)) = \operatorname{dg} (\forall xA(x)) = \operatorname{dg} (A(a)) + 1\).

보조정리 1.1

각 시퀀트 \(\Gamma\) 와 식 \(A\) 에 대하여 \(\vdash \Gamma,\neg A,A\) 이다.

정의 1.2 부분식(subformula)

식 \(A\) 의 부분식 집합 \(Sbfml(A)\) 을 다음과 같이 정의한다.

1. 리터럴 \(L\) 에 대하여 \(Sbfml(L) = \{L\}\).
2. \(A \in \{A_0 \lor A_1, A_0 \land A_1\}\) 에 대하여 \(Sbfml(A) = \{A\} \lor \bigcup \{Sbfml(A_i) : i = 0, 1\}\)
3. \(A \in \{\exists xB(x), \forall xB(x)\}\) 에 대하여 \(Sbfml(A) = \{A\} \lor \bigcup \{Sbfml(B(t)) : t \text{ 는 항이다}\}\)

보조정리 1.2 절단이 없는 증명의 부분식 성질

\(\bm{G}_1\) 에서 절단이 없는 증명에서 나타나는 임의의 식은 끝시퀸트에서 나타나는 식의 부분식이다.

보조정리 1.3 약화 보조정리(Weakening Lemma)

정의 1.3 순수 변수 조건(pure variable condition)

변수가 추론의 고유변수일 때(가령, 논리 계산 \(\bm{G}_1 +(cut)\) 에 대한 \((\forall )\) 의 고유변수) 자유변수가 추론의 상시퀀트에서 나타나고 하시퀀트에서 나타나지 않으면 증명 \(P\) 가 순수 변수 조건을 가지고 있다고 한다.

정의 1.4

1. 반복(iterate): \(f ^{(x)}\) 를 다음과 같이 정의된 \(\N\) 위의 단항 함수 \(f\) 의 \(x\)번째 반복이라고 정의한다.

   \[ f ^{(0)}(y) = y \qquad f ^{(x+1)}(y) = f(f ^{(x)}(y)) \]

2. Grzegorczyk 함수: \(n\)번째 Grzegorczyk 함수 \(F_n\) 는 다음과 같이 정의된 정수 위의 함수이다.

   \[ F_0(x) = x + 1 \qquad F _{n+1}(x) = F _{n}^{(x)}(x) \]

정의 1.5

1. 초기 함수 모임(class of initial function): 영함수 \(\operatorname{zero}\), 다음수 함수 \(S\), 함수 \(x \dotdiv y = \max \{x-y, 0\}\), 최대함수 \(\max\), 사영함수 \(I _{i}^{k}(x_1, \dots, x_k) = x_i\) 에 대한 다음의 모임 \(\mathscr{B}\) 을 초기 함수 모임이라고 한다.

   \[\mathscr{B} = \{\operatorname{zero} , S, x \dotdiv y, \max \} \cup \{I _{i}^{k} : 1 \leq i \leq k, k > 0\}\]

2. 합성(composition): \(\mathbf{x} = x_1, \dots, x_n\) 에 대하여 \(f\) 가 다음과 같으면 \(f\) 를 \(h, g_1, \dots, g_m\) 로부터 합성에 의하여 정의되었다고 한다.

   \[ f(\mathbf{x} ) = h(g_1(\mathbf{x} ),\dots ,g_m(\mathbf{x} )) \]

3. 원시 재귀(Primitive Recursion): 다음이 성립하면 \(f\) 가 \(g,h\) 로부터 원시 재귀에 의하여 정의되었다고 한다.

   \[ f(\mathbf{x} ,0) = g(\mathbf{x} ) \qquad f(\mathbf{x} , y + 1) = h(\mathbf{x} , y , f(\mathbf{x} ,y )) \]

4. 합(Summation): 정의 \(\displaystyle \sum_{i<0}^{}g(\mathbf{x} ,i) := 0\) 에 대하여 다음이 성립하면 \(f\) 가 \(g\) 로부터 합에 의하여 정의되었다고 한다.

   \[ f(\mathbf{x} ,y) = \sum_{i<y}^{}g(\mathbf{x} ,i) \]

5. 곱(Product): 정의 \(\displaystyle \prod_{i<0}^{}g(\mathbf{x} ,i) := 1\) 에 대하여 다음이 성립하면 \(f\) 가 \(g\) 로부터 곱에 의하여 정의되었다고 한다.

   \[ f(\mathbf{x} ,y) = \prod_{i<y}^{}g(\mathbf{x} ,i) \]

6. 기본 폐포(elementary closure): \(\N\) 위의 함수의 모임 \(\mathscr{F}\) 의 기본 폐포는 다음을 만족하는 가장 작은 모임 \(\mathscr{G}\) 이다.

   • \(\mathscr{B} \cup \mathscr{F} \subset \mathscr{G}\)
   • \(\mathscr{G}\) 는 합성, 합, 곱에 대하여 닫혀있다.

7. Grzegorczyk 계층(Grzegorczyk hierarchy): \(3 \leq n \leq \omega\) 라고 하자. Grzegorczyk 계층에서 \(n\)번째 모임 \(\mathscr{E}^{n}\) 을 함수들 \(\{F_m:m<n\}\) 의 기본 폐포라고 정의한다.

   기본 재귀 함수 모임(class of elementary recursive functions): \(\mathscr{E} ^{3}\) 을 기본 재귀 함수들의 모임이라고 한다.

8. \(\mathsf{PRIM}\) 은 모든 원시 재귀 함수의 모임이다. 즉, \(\mathsf{PRIM}\) 은 다음을 만족하고 합성과 원시 재귀에 대하여 닫혀있는 가장 작은 모임 \(\mathscr{G}\) 이다.

   \[ \{\operatorname{zero} ,S\} \cup \{I _{i}^{k}:1 \leq i \leq k, k>0\} \subset \mathscr{G} \]

9. 함수 모임 \(\mathscr{G}\) 에 대하여 \(\mathscr{G} _{*}\) 는 자신의 특성 함수가 \(\mathscr{G}\) 에 속하는 관계들의 모임이다.

명제 1.2

함수 모임 \(\mathscr{F}\) 의 기본 폐포 \(\mathscr{E} (\mathscr{F} )\) 에 대하여 다음이 성립한다.

1. 동등 관계 \(x=y\) 는 \(\mathscr{E} (\mathscr{F} )_{*}\) 에 속하고, \(\mathscr{E} (\mathscr{F} )_{*}\) 는 불 연산(boolean operation)과 유계 양화사(bounded quantification)에 대하여 닫혀있다. 즉, \(R\) 이 \(\mathscr{E} (\mathscr{F} )_{*}\) 에 속하면 \(\exists z < yR(z, \mathbf{x} )\) 도 그러하다.
2. \(\mathscr{E} (\mathscr{F} )\) 는 유계 최소화(bounded minimization)에 대하여 닫혀있다. 즉, \(R\) 이 \(\mathscr{E} (\mathscr{F} )_{*}\) 에 속하면 \(f(y, \mathbf{x} ) = \min \{z : (z < y \land R(\mathbf{x} , z)) \lor z = y\}\) 는 \(\mathscr{E} (\mathscr{F} )\) 에 속한다.
3. 각 \(f(\mathbf{x} )\in \mathscr{E} (\mathscr{F} )\) 에 대하여 그것의 그래프 \(R = \{(\mathbf{x} ,y) : f(\mathbf{x} ) = y\}\) 는 \(\mathscr{E} (\mathscr{F} )_{*}\) 에 속한다. 역으로 \(f(\mathbf{x} )\) 의 그래프가 \(\mathscr{E} (\mathscr{F} )^{*}\) 에 속하고 \(j(\mathbf{x} )\in \mathscr{E} (\mathscr{F} )\) 에 대하여 \(f(\mathbf{x} )\leq j(\mathbf{x} )\) 이면 \(f(\mathbf{x} )\) 가 \(\mathscr{E} (\mathscr{F} )\) 에 속한다.

4. 각각의 다음 함수는 기본적(elementary)이다. 즉, 기본 재귀 함수이다.

   • \(n\)번째 소수 \(p_n\) 에 대한 함수 \(n \mapsto p_n\)
   • \((x_0, \dots, x _{n-1}) \mapsto \left< x_0, \dots, x _{n-1}\right> := \prod_{i<n}^{}p _{i}^{1+x_i}\)
   • \(y|x : \iff \exists z \leq x(yz = x)\) 에 대한 \(exp(x, i) = \max \{y \leq x : p _{i}^{y}|x\}\)
   • \((x)_i = exp(x, i)\dotdiv 1\)
   • \(lh(x) = \min \{i \leq x : exp(x, i) = 0\}\)

5. \(\mathscr{E} (\mathscr{F} )\) 는 한정된 재귀(Limited Recursion)에 대하여 닫혀있다. (함수 \(f\) 가 \(g, h \in \mathscr{E}(\mathscr{F})\) 로부터 원시 재귀에 의하여 정의되었다고 하자. \(j(\mathbf{x} ,y) \in \mathscr{E}(\mathscr{F})\) 에 대하여 \(f(\mathbf{x} ,y) \leq j(\mathbf{x} ,y)\) 이면 \(f(\mathbf{x} ,y) \in \mathscr{E}(\mathscr{F})\) 이다.)

명제 1.3

1. \(x>0\) 에 대하여 \(F_n(x) > x\)
2. \(F _{n}^{(y)}(x) \geq x\)
3. \((x, y)\mapsto F _{n}^{(y)}(x)\) 는 \(x>0\) 와 \(y\) 에서 순증가(strictly increasing)한다.
4. \(x \geq 2\) 에 대하여 \(F _{n+1}(x) > F_n(x)\)

보조정리 1.4

임의의 \(\mathbf{x} =x_1, \dots, x_k\) 와 각 원시 재귀 함수 \(f(\mathbf{x} )\) 에 대하여 다음을 만족하는 \(n\) 이 존재한다.

• \(f(\mathbf{x} )\leq F_n(\max \{\mathbf{x} ,2\})\) 가 성립한다.

따름정리 1.1

정의 1.6

먼저 다음과 같이 산술 체계의 언어를 정의한다.

• 기본 (재귀) 산술(elementary (recursive) arithmetic) 의 언어 \(\mathcal{L} (\mathsf{EA})\): \(\mathscr{E} ^{3}\) 에 대한 기본 (재귀) 산술 \(\mathsf{EA}\) 는 함수 \(exp(x) = 2 ^{x}\) 에 대한 언어 \(\mathcal{L} (\mathsf{EA}) = \{=, \leq ,0,S, +, \cdot ,exp\}\) 안에서의 1차 논리 산술의 부분이다.

• \(\mathsf{EA}^{4}\) 의 언어 \(\mathcal{L} (\mathsf{EA}^{4})\): \(\mathsf{EA}^{4}\) 는 함수 \(tower(x) = 2_x = exp ^{(x)}(1)\) 에 대한 확장된 언어 \(\mathcal{L} (\mathsf{EA}^{4}) = \mathcal{L} (\mathsf{EA}) \cup \{tower\}\) 안에서의 1차 논리 산술의 또 다른 부분이다.

• 원시 재귀 산술의 언어 \(\mathcal{L} (\mathsf{PRA})\): \(\mathcal{L} (\mathsf{PRA}) = \{=, \leq \} \cup \{\mathsf{f} : f \in \mathsf{PRIM}\}\) 은 각 원시 재귀 함수 \(f \in \mathsf{PRIM}\) 을 함수 기호 \(\mathsf{f}\) 로 갖는 원시 재귀 산술 \(\mathsf{PRA}\) 에 대한 언어이다.

다음은 함수 기호와 관계 기호에 따르는 공리들이다.

• 함수 기호에 대한 공리:

  • \(x + 0 = x\), \(x + S(y) = S(x + y)\)
  • \(x \cdot 0 = 0\), \(x \cdot S(y) = x \cdot y + x\)
  • \(exp(0) = 1 := S(0)\), \(exp(S(x)) = exp(x) \cdot 2\), \((2 := S(1))\)

  • \(tower(0) = 1\), \(tower(S(x)) = exp(tower(x))\)

  • \(f\) 가 \(h, g_1, \dots, g_m\) 로부터 합성에 의하여 정의되었다면 \(\mathsf{f}(\mathbf{x} ) = \mathsf{h}(\mathsf{g}_1(\mathbf{x}) ,\dots ,\mathsf{g}_m(\mathbf{x} ))\) 가 그것의 공리이다.

  • \(f\) 가 \(g,h\) 로부터 원시 재귀에 의하여 정의되었다면 \(\mathsf{f}(\mathbf{x} ,0) = \mathsf{g}(x)\) 와 \(\mathsf{f}(\mathbf{x} ,S(y)) = \mathsf{h}(\mathbf{x} ,y,\mathsf{f}(\mathbf{x} ,y))\) 가 그것의 공리이다.

• 이산 순서(discrete order) \(\leq\) 에 대한 공리: \(0 \leq x\), \(x \leq S(y) \iff x \leq y \lor x = S(y)\), \(x \leq x\), \(x \leq y \leq z \implies x \leq z\), \(x \leq y \lor y \leq x\), \(x \leq y \leq x \implies x = y\)

이항 관계 기호 \(\leq\) 를 갖는 언어 \(\mathcal{L}\) 에 대하여 다음과 같이 정의한다.

1. \(\mathcal{L}\) 의 식이 유계(bounded)라는 것은 그 식에 있는 모든 양화사가 \(\mathcal{L}\) 의 항에 의하여 유계, 즉, \(\exists x \leq t\), \(\forall x \leq t\) 라는 것이다. 유계 양화사는 \(\exists x \leq tA(x) : \equiv (\exists x(x \leq t \land A(x)))\) 와 같이 정의된다.
2. \(\Delta_0(\mathcal{L} ) = \Sigma_0(\mathcal{L} ) = \Pi _0(\mathcal{L} )\) 은 언어 \(\mathcal{L}\) 안에서의 유계 식의 모임을 나타낸다.
3. \(\Sigma_n(\mathcal{L} )\) 은 \(\mathcal{L}\) 안에서의 \(\Sigma_n\)-식의 모임을 뜻한다. \(\Sigma_n\) 식은 \(B \in \Delta_0(\mathcal{L} )\) 이고 \(n\) 이 짝수일 때 \(Q = \forall\) 이고 그렇지 않을 때 \(Q = \exists\) 인 \(\exists x_1 \forall x_2 \dots Qx_nB\) 형태의 식이다.

4. \(\{=, \leq , 0, S\} \subset \mathcal{L} \subset \mathcal{L} (\mathsf{PRA})\) 라고 두자. \(\text{I}\Sigma _n(\mathcal{L} )\) 은 언어 \(\mathcal{L}\) 안에서의 1차 논리 산술의 부분을 뜻한다. 이것의 공리는 페아노 공리로써 다음과 같다.

   • \(\forall x(S(x) \neq 0)\)
   • \(\forall x,y(S(x) = S(y) \implies x=y)\)
   • \(\mathsf{f}\in \mathcal{L}\) 에 대한 함수 기호 \(\mathsf{f}\) 에 대한 정의된 공리
   • 이산 순서(discrete order) \(\leq\) 에 대한 공리

   • 다음과 같은 \(\Sigma_n(\mathcal{L} )\)-식 \(A\) 에 대한 완전 귀납꼴(complete induction schema)이다.

     \[ A(0) \land \forall x(A(x) \implies A(S(x))) \implies \forall xA(x) \]

이제 산술 체계를 다음과 같이 정의한다.

• 페아노 산술(Peano arithmetic, 1차 논리 산술, first-order arithmetic): 위에서 정의한 언어 \(\mathcal{L}\) 에 대하여 \(\mathsf{PA}(\mathcal{L} ):= \text{I}\Sigma _{\omega }(\mathcal{L} ):= \bigcup_{n < \omega }^{}\text{I}\Sigma_n(\mathcal{L} )\)

• 기본 산술(elementary arithmetic): \(\mathsf{EA}:= \mathsf{EA}^{3}:= \text{I}\Sigma_0(\mathcal{L} (\mathsf{EA}))\)

• \(\mathsf{EA}^{4} := \text{I}\Sigma_0(\mathcal{L} (\mathsf{EA}^{4}))\)

• 원시 재귀 산술(primitive recursive arithmetic): \(\mathsf{PRA}:= \mathsf{EA} ^{\omega } := \text{I}\Sigma_0 (\mathcal{L} (\mathsf{PRA}))\)

명제 1.4

\(0 < n \leq \omega\) 을 잡자. \(\{\mathsf{f}: f \in \mathscr{E}^{3}\} \subset \mathcal{L} \cap \mathcal{L} '\) 과 \(\mathcal{L} \cup \mathcal{L} ' \subset \mathcal{L} (\mathsf{PRA})\) 을 만족하는 임의의 언어 \(\mathcal{L}\), \(\mathcal{L}'\) 에 대하여 \(\text{I}\Sigma _n(\mathcal{L} ) = \text{I}\Sigma _n(\mathcal{L} ')\) 이다.

partial truth definition, partial truth predicate \(\operatorname{Tr}_n\)

명제 1.5

1. \(\Sigma_0(\mathcal{L} (\mathsf{EA}))\)-식에 대한 부분적 진리 정의는 산술 \(\mathsf{EA}^{4}\) 안에서 \(\Sigma_0(\mathcal{L} (\mathsf{EA}^4))\)-식에 의하여 정의가능하다.
2. 각 \(n>0\) 에 대하여 \(\Sigma_n(\mathcal{L} (\mathsf{EA}))\)-식에 대한 부분 진리 정의는 산술 \(\mathsf{EA}\) 안에서 \(\Sigma_n(\mathcal{L} (\mathsf{EA}))\)-식 \(\operatorname{Tr}_n\) 에 의하여 정의가능하다.

명제 1.6 (Craig's trick)

임의의 r.e.(=재귀적으로 열거가능한(recursively enumerable)=계산가능하게 열거가능한(computably enumerable)) 이론은 문장들의 기본 재귀 집합에 의하여 공리화 가능하다.