Skip to content

FormalNumberTheory

Formal Number Theory

형식적 수론(formal number theory)

1차 이론 SS 의 언어 LA\mathcal{L}_A 를 산술의 언어(language of arithmetic)라고 하자. LA\mathcal{L}_A 는 단일 술어 기호 A12A _{1}^{2}, 단일 개별 상수 a1a_1, 세 함수 기호 f11,f12,f22f _{1}^{1},f _{1}^{2}, f _{2}^{2} 를 가진다. A12(t,s)A _{1}^{2}(t, s)t=st = s 로 쓰고, a1a_100 로 쓰고, f11(t)f _{1}^{1}(t)(t)(t') 로 쓰고, f12(t,s)f _{1}^{2}(t, s)(t+s)(t+s) 로 쓰고, f22(t,s)f _{2}^{2}(t, s)(ts)(t \cdot s) 로 쓰자.

SS 의 고유공리는 다음과 같다.

(S1)x1=x2(x1=x3x2=x3)(S1) \quad x_1 = x_2 \implies (x_1 = x_3 \implies x_2 = x_3)

(S2)x1=x2x1=x2(S2) \quad x_1 = x_2 \implies x_1' = x_2'

(S3)0x1(S3) \quad 0 \neq x'_1

(S4)x1=x2x1=x2(S4) \quad x'_1 = x'_2 \implies x_1 = x_2

(S5)x1+0=x1(S5) \quad x_1 + 0 = x_1

(S6)x1+x2=(x1+x2)(S6) \quad x_1 + x'_2 = (x_1 + x_2)'

(S7)x10=0(S7) \quad x_1 \cdot 0 = 0

(S8)x1(x2)=(x1x2)+x1(S8) \quad x_1 \cdot (x_2)' = (x_1 \cdot x_2) + x_1

(S9)(S9) \quad(principle of mathematical induction) SS 의 임의의 wff B(x)B(x) 에 대하여 다음이 성립한다.

B(0)((x)(B(x)B(x))(x)B(x))B(0) \implies \bigg ((\forall x)\Big (B(x) \implies B(x')\Big ) \implies (\forall x)B(x) \bigg )

공리 (S9)(S9) 과 MP 에 의하여 SS 는 다음과 같은 추론규칙을 얻는다. 이것을 귀납 규칙(induction rule)이라 한다.

B(0),(x)(B(x)B(x))S(x)B(x) B(0), (\forall x)(B(x) \implies B(x')) \vdash _S (\forall x)B(x)
  • 수학을 형식화할 때 수학의 엄밀한 기반을 마련하는 첫단계가 수론의 엄밀한 정의이다. 집합론에서 모순이 발견되자 수학자들은 수학의 기초을 엄밀하게 마련해야 할 필요성을 느꼈다. 비유클리드 기하학을 유클리드 기하학으로 매장할 수 있고, 곧 기하학 전체를 산술로 매장할 수 있었다. 자연수가 정의되면, 정수를 정의할 수 있고, 정수로 유리수를 정의할 수 있고, 유리수로 실수를 정의할 수 있고, 실수로 복소수를 정의할 수 있었다. 해석학, 통계학, 확률론 등 수학의 모든 분야를 자연수론, 즉 산술 위에 세울 수 있었다. 따라서 초유의 관심사는 산술이었다.

    첫 준공리적(semiaxiomatic) 성과는 데데킨트에 의하여 소개되었고, 그것을 약간 수정하여 페아노가 산술(자연수론)의 5가지 공리를 소개했다. 이 페아노 공리계와 집합론을 사용하면 산술 뿐만 아니라 유리수, 실수, 복소수까지도 구성할 수 있다.

    그러나 페아노 공리계는 "성질"이라는 직관적 개념을 사용했는데, 이런 개념 때문에 체계가 엄밀하게 형식화될 수 없었다. 따라서 기초 수론의 결과의 증명에 적합하도록 페아노 공리계를 기반으로 1차 논리 언어 위에 1차 이론 SS 를 구성해야 한다.

    SS 과 같은 정리를 갖는 임의의 이론을 페아노 산술(Peano arithmetic, PA) 라고 한다.

  • (S1)(S8)(S1) - (S8) 는 wff, 즉, 공리이다. 그러나 (S9)(S9) 는 공리꼴이다.

  • 공리 (S3)(S3)(S4)(S4)페아노 공리 3), 5) 에 대응된다.

    공리 (S1)(S1)(S2)(S2) 가 동등성에 필요한 성질을 보여준다. 그러나 이는 페아노 공리계에서 직관적으로 명백하므로 암묵적으로 상정되어있던 것이다. 이는 SS 가 페아노 공리계의 엄밀하지 못한 부분들을 완전히 엄밀하게 형식화했다는 것을 의미한다.

    공리 (S5)(S8)(S5)-(S8) 은 덧셈과 곱셈의 재귀적 방정식이다. 페아노 공리계에서는 (S5)(S8)(S5)-(S8) 를 만족하는 연산 ++\cdot 의 존재성이 집합론에 의하여 직관적으로 함의되었기 때문에 페아노 공리계는 (S5)(S8)(S5)-(S8) 를 상정하지 않았다.

    이로써 SS 는 페아노 공리계가 암묵적으로 상정하고 있는 직관적인 개념들을 모두 배제하고 수론을 엄밀하게 형식화했다.

보조정리 3.1

LA\mathcal{L}_A 의 임의의 항 t,s,rt,s,r 에 대하여 다음 wff 들은 SS 의 정리이다.

(S1)t=r(t=sr=s)(S1') \quad t = r \implies (t = s \implies r = s)

(S2)t=rt=r(S2') \quad t = r \implies t' = r'

(S3)0t(S3') \quad 0 \neq t'

(S4)t=rt=r(S4') \quad t' = r' \implies t = r

(S5)t+0=t(S5') \quad t + 0 = t

(S6)t+r=(t+r)(S6') \quad t + r' =(t+r)'

(S7)t0=0(S7') \quad t \cdot 0 = 0

(S8)tr=(tr)+t(S8') \quad t \cdot r' = (t \cdot r)+t

  • 증명

정리 3.2

임의의 항 t,s,rt,s,r 에 대하여 다음 wff 들은 SS 의 정리이다.

  1. t=tt = t
  2. t=rr=tt = r \implies r = t
  3. t=r(r=st=s)t = r \implies (r = s \implies t = s)
  4. r=t(s=tr=s)r = t \implies (s = t \implies r = s)
  5. t=rt+s=r+st = r \implies t + s = r + s
  6. t=0+tt = 0 + t
  7. t+r=(t+r)t' + r = (t + r)'
  8. t+r=r+tt + r = r + t
  9. t=rs+t=s+rt = r \implies s + t = s + r
  10. (t+r)+s=t+(r+s)(t + r) + s = t + (r + s)
  11. t=rts=rst = r \implies t \cdot s = r \cdot s
  12. 0t=00 \cdot t = 0
  13. tr=tr+rt' \cdot r = t \cdot r + r
  14. tr=rtt \cdot r = r \cdot t
  15. t=rst=srt = r \implies s \cdot t = s \cdot r
  • 증명

따름정리 3.3

SS 는 동등성을 지닌 이론이다.

  • 증명

Standard Interpretation

표준 해석(standard interpretation, 표준 모델, standard model)

다음과 같은 해석은 SS 에서 정규 모델이다.

  1. 영역이 음이 아닌 정수이다.
  2. 정수 00 이 기호 00 의 해석이다.
  3. 다음수(successor) 연산(+1+1)이 ' 함수(f11f _{1}^{1})의 해석이다.
  4. 보통의 덧셈과 곱셈이 각각 ++\cdot 의 해석이다.
  5. 항등 관계가 술어 기호 == 의 해석이다.

이 모델을 표준 모델이라고 하고, 자연수 구조라는 의미에서 N\N 으로 표기한다. 따라서 N\N 에서 어떤 자유변수 할당 Φ\Phi 에 대하여 참인 wff AA

N(A)Φ\N \vDash (A) ^{\Phi}

라고 표기하고, 모든 자유변수 할당에서 참이면 다음과 같이 표기한다.

NA\N \vDash A
  • 표준 모델과 동형이 아닌 SS 의 정규 모델을 비표준 모델(nonstandard model)이라고 한다.

  • 표준 해석이 SS 의 모델이면 SS 는 무모순이다. 진리의 성질 2)에 의하여 모델을 가지면 건전성 정리에 의하여 모순이 도출될 수 없기 때문이다. 만약 모순을 도출하면, 즉, \vdash \bot 이면 건전성에 의하여 \vDash \bot 가 된다.

    그러나 집합론의 추론을 포함하는 이러한 의미론적 논증은 무모순성 증명의 기반이 되기에는 안전하지 않다고 여겨진다. 모델에서 진리를 결정하는 근본은 만족의 정의에서 술어를 참이 되게 하는 정의인데, 이 정의는 모델의 영역인 집합에 인자들이 포함되느냐, 포함되지 않느냐로 결정되므로 모델에 의한 무모순성 증명은 집합론의 추론을 기반으로 한다. 증명이론의 의미론적 무모순성 부분에서 이 내용에 대하여 자세히 다룬다.

정리 3.4

임의의 항 t,r,st,r,s 에 대하여 다음의 wff 는 SS 의 정리이다.

  1. t(r+s)=(tr)+(ts)t \cdot (r + s) = (t \cdot r) + (t \cdot s) (distributivity)
  2. (r+s)t=(rt)+(st)(r + s)\cdot t = (r \cdot t) + (s \cdot t) (distributivity)
  3. (tr)s=t(rs)(t \cdot r) \cdot s = t \cdot (r \cdot s) (associativity of \cdot)
  4. t+s=r+st=rt + s = r + s \implies t = r (cancellation law for ++)
  • 증명

Numeral

숫자(numeral)

0,0,0,0, 0', 0'', \dots 를 숫자라고 부르고, 편의상 0,1,2,\overline{0}, \overline{1}, \overline{2}, \dots 라고 쓰자.

정리 3.5

다음은 SS 의 정리이다.

  1. t+1=tt + \overline{1} = t'
  2. t1=tt \cdot \overline{1} = t
  3. t2=t+tt \cdot \overline{2} = t + t
  4. t+s=0t=0s=0t + s = 0 \implies t = 0 \land s = 0
  5. t0(st=0s=0)t \neq 0 \implies (s \cdot t = 0 \implies s = 0)
  6. t+s=1(t=0s=1)(t=1s=0)t + s = \overline{1} \implies (t = 0 \land s = \overline{1})\lor (t = \overline{1}\land s = 0)
  7. ts=1(t=1s=1)t \cdot s = \overline{1} \implies (t = \overline{1} \land s = \overline{1})
  8. t0(y)(t=y)t \neq 0 \implies (\exists y)(t = y')
  9. s0(ts=rst=r)s \neq 0 \implies (t \cdot s = r \cdot s \implies t = r)
  10. t0(t1(y)(t=y))t \neq 0 \implies (t \neq 1 \implies (\exists y)(t = y''))
  • 증명

정리 3.6

  1. 임의의 자연수 m,nm, n 에 대하여 다음이 성립한다.

    1. mnm \neq n 이면 Smn\vdash _S \overline{m} \neq \overline{n} 이다.
    2. Sm+n=m+n\vdash _S \overline{m+n} = \overline{m} + \overline{n} 이고 Smn=mn\vdash _S \overline{m \cdot n} = \overline{m}\cdot \overline{n} 이다.
  2. SS 의 임의의 모델은 무한이다.

  3. 임의의 기수 β\aleph _{\beta} 에 대하여 SS 는 기수 β\aleph _{\beta} 의 정규 모델을 가진다.
  • 증명

Order Relation

순서 관계(order relation)

순서 관계를 다음과 같이 정의한다.

t<s:=(w)(w0w+t=s)ts:=t<st=st>s:=s<tts:=stts:=¬(t<s) \begin{align}\begin{split} t < s&:= (\exists w)(w \neq 0 \land w + t = s)\\ t \leq s&:= t < s \lor t = s\\ t > s&:= s < t \\ t \geq s&:= s \leq t \\ t \not < s&:= \neg (t < s)\\ \end{split}\end{align} \tag*{}

정리 3.7

임의의 항 t,r,st,r,s 에 대하여 다음은 정리이다.

정리 정리
1 ttt \not < t 15 tr(t<rr<t)t \neq r \implies (t < r \lor r < t)
2 t<s(s<rt<r)t < s \implies \\(s < r \implies t < r) 16 t=rt<rr<tt = r \lor t < r \lor r < t
3 t<sstt < s \implies s \not < t 17 trrtt \leq r \lor r \leq t
4 t<st+r<s+rt < s \iff t + r < s + r 18 t+rtt + r \geq t
5 ttt \leq t 19 r0t+r>tr \neq 0 \implies t + r > t
6 ts(srtr)t \leq s \implies \\ (s \leq r \implies t \leq r) 20 r0trtr \neq 0 \implies t \cdot r \geq t
7 tst+rs+rt \leq s \iff t + r \leq s + r 21 r0r>0r \neq 0 \iff r > 0
8 ts(s<rt<r)t \leq s \implies \\ (s < r \implies t < r) 22 r>0(t>0rt>0)r > 0 \implies (t >0 \implies r \cdot t>0)
9 0t0 \leq t 23 r0(t>1tr>r)r \neq 0 \implies (t > 1 \implies t \cdot r > r)
10 0<t0 < t' 24 r0(t<str<sr)r \neq 0 \implies \\ (t <s \iff t \cdot r < s \cdot r)
11 t<rtrt < r \iff t' \leq r 25 r0(tstrsr)r \neq 0 \implies \\(t \leq s \iff t \cdot r \leq s \cdot r)
12 trt<rt \leq r \iff t < r' 26 t0t \not < 0
13 t<tt < t' 27 trrtt=rt \leq r \land r \leq t \implies t = r
14 0<1,1<2,2<3,0<\overline{1}, \overline{1}<\overline{2},\overline{2}<\overline{3},\dots
  • 증명

정리 3.8

임의의 자연수 kk 와 임의의 wff BB 에 대하여 다음이 성립한다.

  1. Sx=0x=kxk\vdash _S x = 0 \lor \dots \lor x = \overline{k} \iff x \leq \overline{k}
  2. SB(0)B(1)B(k)(x)(xkB(x))\vdash _S B(0) \land B(\overline{1}) \land \dots \land B(\overline{k})\iff (\forall x)(x \leq \overline{k} \implies B(x))
  3. k>0k>0 에 대하여 Sx=0x=(k1)x<k\vdash _S x = 0 \lor \dots \lor x = (\overline{k-1})\iff x < \overline{k}.
  4. k>0k>0 에 대하여 SB(0)B(1)B(k1)(x)(x<kB(x))\vdash _S B(0)\land B(\overline{1})\land \dots \land B(\overline{k-1}) \iff (\forall x)(x < \overline{k} \implies B(x)).
  5. S((x)(x<yB(x))(x)(xyC(x)))(x)(B(x)C(x))\vdash _S((\forall x)(x < y \implies B(x)) \land (\forall x)(x \geq y \implies C(x))) \implies (\forall x)(B(x) \lor C(x))
  • 증명

Other forms of induction principle

정리 3.9

  1. 완전 귀납(complete induction)

    S(x)((z)(z<xB(z))B(x))(x)B(x)\vdash _S(\forall x)((\forall z)(z < x \implies B(z)) \implies B(x)) \implies (\forall x)B(x)
  2. 최소수 원리(least-number principle)

    S(x)B(x)(y)B(y)(z)(z<y¬B(z))\vdash _S(\exists x)B(x) \implies (\exists y)B(y) \land (\forall z)(z < y \implies \neg B(z))
  • 완전 귀납의 의미는 이렇다. 성질 PP 가 임의의 xx 보다 작은 모든 자연수에서 성립할 때 xx 에서도 성립하면 PP 자연수 전체에서 성립한다.

    최소수 원리의 의미는 이렇다. 성질 PP 가 어떤 자연수에서 성립하면 PP 를 만족하는 최소수가 존재한다.

Divisor

약수(divisor)

tst|s(z)(s=tz)(\exists z)(s = t \cdot z) 와 같이 정의한다.

정리 3.10

임의의 항 t,s,rt,s,r 에 대하여 다음 wff 들은 정리이다.

  1. ttt|t
  2. 1t\overline{1}|t
  3. t0t|0
  4. tssrtrt|s \land s|r \implies t|r
  5. s0tstss \neq 0 \land t|s \implies t \leq s
  6. tssts=tt|s \land s|t \implies s = t
  7. tst(rs)t|s \implies t|(r \cdot s)
  8. tstrt(s+r)t|s \land t|r \implies t|(s + r)
  • 증명

정리 3.11 몫과 나머지의 유일한 존재성

xx 에 대하여 다음이 성립한다.

Sy0(q)(r)[x=yq+rr<y(q1)(r1)((x=yq1+r1r1<y)q=q1r=r1)] \begin{align}\begin{split} &\vdash _S y \neq 0 \implies (\exists q)(\exists r)[ x = y \cdot q + r \land r < y \\ & \qquad \qquad \qquad \qquad \land (\forall q_1)(\forall r_1)((x = y \cdot q_1 + r_1 \land r_1 < y) \\ & \qquad \qquad \qquad \qquad \qquad \qquad \qquad \implies q = q_1 \land r = r_1) ]\\ \end{split}\end{align} \tag*{}
  • 이 정리는 수 xx 에 대한 약수 yy 에 따른 몫과 나머지의 유일한 존재성을 보장한다.

  • 이 정리에 도달한 시점에서 기초 수론을 SS 안으로 변환할 수 있고 기초 수론의 임의의 결과를 증명할 수 있다. xyx ^{y}x!x! 같은 아직 정의해야 할 수론적 함수(number-theoretic function)들이 있지만, 충분히 정의 가능하다. 로그 함수 같은 비기초적 개념은 SS 안으로 형식화 될 수 없다.

    SS 가 무모순일 경우 SS 안에서 증명될 수 없고 반증될 수도 없는 닫힌 wff 가 존재한다. 따라서 표준 해석 N\N 에서 참임에도 불구하고 SS 에서 증명 불가능한 wff 가 존재한다. 이 SS 의 불완전성이 어떤 핵심적인 공리의 누락 때문에 발생한 것이 아니라 좀 더 깊은 기저의 본질적인 이유가 존재한다.

  • 증명

Number-Theoretic Function and Relation

수론적 함수와 수론적 관계(number-theoretic function and relation)

수론적 함수는 인자와 값이 자연수인 함수 NN\N \to \N 이다. 수론적 관계는 인자가 자연수인 관계이다.

  • 예시

    덧셈과 곱셈은 수론적 함수이다.

    x+y<zx + y < z 는 3개의 인자를 갖는 수론적 관계이다.

Expressible

관계의 표현가능성(expressible)

산술의 언어 LA\mathcal{L}_A 의 임의의 이론 KK 에 대하여 인자 nn 의 수론적 관계 RRKK 에서 표현가능하다는 것은 자유변수 x1,,xnx_1, \dots, x_n 를 갖는 KK 의 wff B(x1,,xn)B(x_1, \dots, x_n) 가 존재하여 임의의 자연수 k1,,knk_1, \dots, k_n 에 대하여 다음이 성립한다는 것과 동치이다.

  1. R(k1,,kn)R(k_1, \dots, k_n) 가 참이면 KB(k1,,kn)\vdash _K B(\overline{k_1}, \dots ,\overline{k_n})
  2. R(k1,,kn)R(k_1, \dots, k_n) 가 거짓이면 K¬B(k1,,kn)\vdash _K \neg B(\overline{k_1}, \dots ,\overline{k_n})
  • 즉, 관계의 이론에서의 표현가능성은 임의의 자연수마다 관계가 참이면 증명가능하고 관계가 거짓이면 반증가능한 wff 의 존재성이다.

  • 관계가 이론 KK 에서 표현가능하면 KK 의 임의의 확장에서도 표현가능하다.

  • 예시

    항등 관계는 SS 에서 wff x1=x2x_1 = x_2 에 의하여 표현된다.

    k1=k2k_1 = k_2 이면 k1\overline{k_1}k2\overline{k_2} 는 같은 항이므로 정리 3.2 1) 에 의하여 Sk1=k2\vdash _S \overline{k_1} = \overline{k_2} 이다. k1k2k_1 \neq k_2 이면 정리 3.6 1) 에 의하여 Sk1k2\vdash _S \overline{k_1} \neq \overline{k_2} 이다.

  • 예시

    관계 "~보다 작은" 도 SS 에서 wff x1<x2x_1 < x_2 에 의하여 표현가능하다.

    x1<x2x_1 < x_2(x3)(x30x3+x1=x2)(\exists x_3)(x_3 \neq 0 \land x_3 + x_1 = x_2) 이다.

    k1<k2k_1<k_2 이면 영이 아닌 수 nn 이 존재하여 k2=n+k1k_2 = n + k_1 이 성립한다. 정리 3.6 1) b) 에 의하여 Sk2=n+k1\vdash _S \overline{k_2} = \overline{n} + \overline{k_1} 이다. (S3)(S3') 에 의하여 n0n \neq 0 이므로 Snˉ0\vdash _S \bar{n} \neq 0 이다. 그러면 rule E4 에 의하여 wff (w)(w0w+k1=k2)(\exists w)(w \neq 0 \land w + \overline{k_1} = \overline{k_2}) 가 증명가능하다. 즉, Sk1<k2\vdash _S \overline{k_1} < \overline{k_2} 이다.

    k1k2k_1 \not < k_2 이면 k2<k1k_2 < k_1 이거나 k2=k1k_2 = k_1 이다. 전자의 경우 앞선 논의에 의하여 Sk2<k1\vdash _S \overline{k_2} < \overline{k_1} 이다. 후자의 경우 앞선 예시에 의하여 Sk2=k1\vdash _S \overline{k_2} = \overline{k_1} 이다. 그러므로 Sk2k1\vdash _S \overline{k_2} \leq \overline{k_1} 이고, 정리 3.7 1), 3) 에 의하여 Sk1k2\vdash _S \overline{k_1} \not < \overline{k_2} 이다.

Representable

함수의 표현가능성(representable)

산술의 언어 LA\mathcal{L}_A 에서 동등성을 가진 임의의 이론 KK 에 대하여 인자 nn 개의 수론적 함수 ff 가 표현가능하다는 것은 자유변수 x1,,xn,yx_1, \dots, x_n,y 를 갖는 KK 의 wff B(x1,,xn,y)B(x_1, \dots, x_n, y) 가 존재하여 임의의 자연수 k1,,kn,mk_1, \dots, k_n, m 에 대하여 다음이 성립한다는 것과 동치이다.

  1. f(k1,,kn)=mf(k_1, \dots, k_n) = m 이면 KB(k1,,kn,m)\vdash _KB(\overline{k_1},\dots ,\overline{k_n}, \overline{m}) 이다.
  2. K(1y)B(k1,,kn,y)\vdash _K(\exists _1y)B(\overline{k_1},\dots ,\overline{k_n},y)

조건 2) 를 다음과 같이 바꾸면 함수 ffKK 에서 강력하게 표현가능하다고 한다.

  1. K(1y)B(x1,,xn,y)\vdash _K(\exists _1y)B(x_1,\dots ,x_n,y)
  • 함수의 표현가능성은 관계의 표현가능성이 그 참거짓에 따라 증명가능하고 반증가능한 wff 의 존재성을 의미한 것에 비해, 임의의 자연수마다 함수가 mm 이라는 값을 가질 때 m\overline{m} 의 값을 유일하게 갖는 wff 의 존재성을 의미한다.

  • n\exists _n 은 성질을 만족하는 대상이 nn개 존재한다는 의미이다.

  • 강력한 표현가능성(조건 3)은 Gen 과 rule A4 에 의하여 표현가능성(조건 2)을 함의한다. 그런데 정리 3.12 는 그 역도 참이라는 것을 말해준다.

정리 3.12 (V.H. Dyson)

f(x1,x2,,xn)f(x_1, x_2, \dots, x_n)KK 에서 표현가능하면 KK 에서 강력하게 표현가능하다.

  • 이 정리에 의하여 강력한 표현가능성과 표현가능성은 동치이다.

  • 함수가 KK 에서 표현가능하면 KK 의 임의의 확장에서 표현가능하다.

  • 증명

Characteristic Function

특성 함수(characteristic function)

인자 nn 개의 관계 RR 에 대하여 특성함수 CRC_R 을 다음과 같이 정의한다.

CR(x1,x2,,xn)={0R(x1,x2,,xn) is true1R(x1,x2,,xn) is false C_R(x_1, x_2, \dots, x_n) = \begin{cases} 0 &R (x_1, x_2, \dots, x_n) \text{ is true}\\ 1 &R (x_1, x_2, \dots, x_n) \text{ is false}\\ \end{cases}

정리 3.13

언어 LA\mathcal{L}_A 에서 동등성을 지닌 이론 KK 에서 K01\vdash _K 0 \neq \overline{1} 이면 수론적 관계 RRKK 에서 표현가능한 것과 CRC_RKK 에서 표현가능한 것은 동치이다.

  • SS 에서 S01\vdash _S 0 \neq \overline{1} 이므로 SS 에서는 관계 RR 의 표현가능성과 CRC_R 의 표현가능성이 동치이다.

  • 증명

Primitive Recursive

초기 함수(initial function)

다음 함수를 초기 함수라고 한다.

  1. 영함수(zero function): 모든 xx 에 대하여 Z(x)=0Z(x) = 0.
  2. 다음수 함수(successor function): 모든 xx 에 대하여 N(x)=x+1N(x) = x + 1.
  3. 사영 함수(projection function): 모든 x1,x2,,xnx_1, x_2, \dots, x_n 에 대하여 Uin(x1,x2,,xn)=xiU _{i}^{n}(x_1, x_2, \dots, x_n) = x_i.
  • SS 에서의 함수의 표현가능성에 대한 연구는 수리논리학과 컴퓨터공학에서 매우 중요한 수론적 함수의 모임으로 이어진다.

Substitution, Recursion, μ-operator

주어진 함수에서 새 함수를 얻는 규칙

  1. 치환(substitution): 함수

    g(y1,,ym),h1(x1,,xn),,hm(x1,,xn) g(y_1, \dots, y_m), h_1(x_1, \dots, x_n), \dots , h_m(x_1, \dots, x_n)

    에 대하여 다음과 같은 함수 ff 를 치환에 의하여 얻어진 함수라고 한다.

    f(x1,,xn)=g(h1(x1,,xn),,hm(x1,,xn)) f(x_1, \dots, x_n) = g(h_1(x_1, \dots, x_n), \dots , h_m(x_1, \dots, x_n))
  2. 재귀(recursion): 다음과 같이 정의된 함수 ffgghh 로부터 재귀에 의하여 얻어진 함수라고 한다.

    f(x1,,xn,0)=g(x1,,xn) f(x_1, \dots, x_n, 0 ) = g(x_1, \dots, x_n)
    f(x1,,xn,y+1)=h(x1,,xn,y,f(x1,,xn,y)) f(x_1, \dots, x_n, y+1) = h(x_1, \dots, x_n, y, f(x_1, \dots, x_n, y))
  3. 제한된 μ\mu-연산자(restricted μ\mu-operator): 함수 g(x1,,xn,y)g(x_1, \dots, x_n, y) 가 임의의 x1,,xnx_1, \dots, x_n 에 대하여 최소한 하나의 yy 가 존재하여 g(x1,,xn,y)=0g(x_1, \dots, x_n, y) = 0 를 만족한다고 하자.

    μy(g(x1,,xn,y)=0)\mu y(g(x_1, \dots, x_n,y) = 0)g(x1,,xn,y)=0g(x_1, \dots, x_n,y) = 0 를 만족하는 최소 yy 라고 정의한다. 일반적으로, 임의의 관계 R(x1,,xn,y)R(x_1, \dots, x_n, y) 에 대하여 μyR(x1,,xn,y)\mu yR(x_1, \dots, x_n,y)R(x1,,xn,y)R(x_1, \dots, x_n,y) 를 만족하는 최소 yy 라고 정의한다.

    f(x1,,xn)=μy(g(x1,,xn,y)=0)f(x_1, \dots, x_n) = \mu y(g(x_1, \dots, x_n, y) = 0) 라고 하자. 이 ffgg 로부터 제한된 μ\mu-연산자에 의하여 얻어졌다고 한다.

  • 재귀 함수에서 n=0n = 0 인 경우 고정된 자연수 kk 에 대하여 ff 는 다음과 같이 정의된다.

    f(0)=k f(0) = k
    f(y+1)=h(y,f(y)) f(y + 1) = h(y, f(y))
  • 재귀의 파라미터는 x1,x2,,xnx_1, x_2, \dots, x_n 이다.

초기함수와 치환으로 얻은 함수의 표현가능성

영함수, 다음수 함수, 사영 함수, 치환에 의하여 얻은 함수는 언어 LA\mathcal{L}_A 에서 동등성을 지닌 임의의 이론에서 표현가능하다. 특히, SS 에서 표현가능하다.

  • 증명

    언어 LA\mathcal{L}_A 에서 동등성을 지닌 임의의 이론 KK 를 잡자.

    영함수 Z(x)=0Z(x) = 0KK 에서 wff x1=x1y=0x_1 = x_1 \land y = 0 에 의하여 강력하게 표현가능하다. 임의의 자연수 k,mk,m 에 대하여 Z(k)=mZ(k) = m 이면 m=0m = 0 이고 Kk=k0=0\vdash _K \overline{k} = \overline{k} \land 0 = 0 이다. 이로써 1) 이 성립한다. K(1y)(x1=x1y=0)\vdash _K(\exists _1y)(x_1 = x_1 \land y = 0) 의 증명은 쉽다. 즉, 3) 이 성립한다. ▲

    다음수 함수 N(x)=x+1N(x) = x + 1 는 wff y=x1y = x'_1 에 의하여 KK 에서 강력하게 표현가능하다. 임의의 k,mk, m 에 대하여 N(k)=mN(k) = m 이면 m=k+1m = k + 1 이다. 그러므로 m\overline{m}k\overline{k}' 이다. 그러면 Km=k\vdash _K \overline{m} = \overline{k}' 이다. K(1y)(y=x1)\vdash _K(\exists _1y)(y = x'_1) 는 쉽게 검증할 수 있다. ▲

    사영 함수 Ujn(x1,x2,,xn)=xjU _{j}^{n}(x_1, x_2, \dots, x_n) = x_jKK 에서 다음 wff 에 의하여 강력하게 표현가능하다.

    x1=x1x2=x2xn=xny=xj x_1 = x_1 \land x_2 = x_2 \land \dots \land x_n = x_n \land y = x_j

    Ujn(k1,,kn)=mU _{j}^{n}(k_1, \dots, k_n) = m 이면 m=kjm = k_j 이다. 그러므로 다음이 성립한다.

    Kk1=k1k2=k2kn=knm=kj \vdash _K \overline{k_1} = \overline{k_1} \land \overline{k_2} = \overline{k_2} \land \dots \land \overline{k_n} = \overline{k_n} \land \overline{m} = \overline{k_j}

    또한, 다음이 성립한다.

    K(1y)(x1=x1x2=x2xn=xny=xj) \vdash _K (\exists _1y) (x_1 = x_1 \land x_2 = x_2 \land \dots \land x_n = x_n \land y = x_j)

    함수 g(x1,,xm),h1(x1,,xn),,hm(x1,,xn)g(x_1, \dots, x_m), h_1(x_1, \dots, x_n), \dots , h_m(x_1, \dots, x_n) 이 동등성을 지닌 이론 KK 에서 각각 wff C(x1,,xm,z),B1(x1,,xn,y1),,Bm(x1,,xn,ym)C(x_1, \dots, x_m, z), B_1(x_1, \dots, x_n, y_1), \dots , B_m(x_1, \dots, x_n, y_m) 에 의하여 강력하게 표현가능하다고 가정하자. 다음과 같은 함수 ff 를 치환에 의하여 정의하자.

    f(x1,,xn)=g(h1(x1,,xn),,hm(x1,,xn)) f(x_1, \dots, x_n) = g(h_1(x_1, \dots, x_n), \dots , h_m(x_1, \dots, x_n))

    그러면 ff 는 다음과 같은 wff D(x1,,xn,z)D(x_1, \dots, x_n, z) 에 의하여 강력하게 표현가능하다.

    (y1)(ym)(B1(x1,,xn,y1)Bm(x1,,xn,ym)C(y1,,ym,z)) (\exists y_1)\dots (\exists y_m)(B_1(x_1, \dots, x_n,y_1)\land \dots \\ \qquad \qquad \land B_m(x_1, \dots, x_n, y_m)\land C(y_1, \dots, y_m, z))

    조건 1) 과 3) 이 성립하는 것은 쉽게 증명가능하다. ■

Primitive Recursive Function

원시 재귀 함수(primitive recursive function)

원시 재귀 함수란 초기 함수에 유한한 수의 치환과 재귀에 의하여 얻어진 함수이다.

  • 즉, 유한한 함수열 f0,,fnf_0, \dots, f_n 이 존재하여 fn=ff_n = f 이고 0in0 \leq i \leq n 에 대하여 각 fif_i 가 초기 함수이거나 앞선 함수에 치환이나 재귀를 적용하여 얻어졌다면 ff 는 원시 재귀이다.

재귀 함수(recursive)

재귀 함수란 초기 함수에 유한한 수의 치환, 재귀, 제한된 μ\mu-연산자를 적용하여 얻어진 함수이다.

  • 원시 재귀 함수의 조건에 제한된 μ\mu-연산자라는 조건만 추가하면 재귀 함수가 된다. 그러므로 원시 재귀 함수이면 재귀 함수이다. 그러나 그 역은 성립하지 않는다.

  • 재귀 함수 모임이 SS 에서 표현가능한 함수의 모임과 같다는 것을 보이려 한다.

정리 3.14

원시 재귀(또는 재귀) g(y1,,yk)g(y_1, \dots, y_k) 와 서로 다른 변수 x1,,xnx_1, \dots, x_n 을 잡고, 1ik1 \leq i \leq k 에 대하여 ziz_ix1,,xnx_1, \dots, x_n 중 하나라고 하자. 그러면 f(x1,,xn)=g(z1,,zk)f(x_1, \dots, x_n) = g(z_1, \dots, z_k) 를 만족하는 함수 ff 는 원시 재귀(또는 재귀)이다.

  • 증명

    1jin1 \leq j_i \leq n 에 대하여 zi=xjiz_i = x _{j_i} 라고 하자. 그러면 zi=Ujin(x1,,xn)z_i = U _{j_i}^{n}(x_1, \dots, x_n) 이다. 따라서 다음이 성립한다.

    f(x1,,xn)=g(Uj1n(x1,,xn),,Ujkn(x1,,xn)) f(x_1, \dots, x_n) = g \left( U _{j_1}^{n}(x_1, \dots, x_n), \dots ,U _{j_k}^{n}(x_1, \dots, x_n) \right)

    ffg,Uj1n,,Ujkng, U _{j_1}^{n}, \dots , U _{j_k}^{n} 로부터 치환에 의하여 정의되므로 원시 재귀(또는 재귀)이다. ■

  • 다음 세 예시는 원시 재귀를 만드는 예시를 보여준다.

  • 예시

    g(x1,x3)g(x_1, x_3) 가 원시 재귀이고 f(x1,x2,x3)=g(x1,x3)f(x_1,x_2,x_3) = g(x_1, x_3) 이면 ff 도 원시 재귀이다. z1=x1z_1 = x_1z2=x3z_2 = x_3 로 두면 정리가 성립한다. 이때 변수 x2x_2ff 의 값에 영향을 미치지 못하므로 더미 변수(dummy variable)라고 한다.

  • 예시

    g(x1,x2,x3)g(x_1, x_2, x_3) 가 원시 재귀이고 f(x1,x2,x3)=g(x3,x1,x2)f(x_1,x_2,x_3) = g(x_3, x_1, x_2) 이면 ff 도 원시 재귀이다. z1=x3z_1 = x_3z2=x1z_2 = x_1z3=x2z_3 = x_2 로 두면 정리가 성립한다.

  • 예시

    g(x1,x2,x3)g(x_1, x_2, x_3) 가 원시 재귀이고 f(x1,x2)=g(x1,x2,x1)f(x_1,x_2) = g(x_1, x_2, x_1) 이면 ff 도 원시 재귀이다. z1=x1z_1 = x_1z2=x2z_2 = x_2z3=x1z_3 = x_1 로 두면 정리가 성립한다.

따름정리 3.15

  1. 영함수 Zn(x1,,xn)=0Z_n(x_1, \dots, x_n) = 0 는 원시 재귀이다.
  2. 상수 함수 Ckn(x1,,xn)=kC _{k}^{n}(x_1, \dots, x_n) = k 는 원시 재귀이다.
  3. 치환 규칙에서 각 함수 hih_i 가 모든 변수에 대한 함수일 필요는 없다. 마찬가지로 재귀 규칙에서 함수 gg 가 모든 변수 x1,,xn,yx_1, \dots, x_n, yf(x1,,xn,y)f(x_1, \dots, x_n,y) 를 포함할 필요가 없고 hh 도 모든 변수 x1,,xn,yx_1, \dots, x_n, yf(x1,,xn,y)f(x_1, \dots, x_n, y) 를 포함할 필요는 없다.
  • 증명

    1:

    정리 3.14 에서 gg 를 영함수 ZZ 로 두고 k=1k = 1 로 두고 z1z_1x1x_1 으로 두면 바로 나온다.

    2:

    수학적 귀납법을 사용하면 된다. k=0k = 0 인 경우 1) 의 결과로부터 쉽게 도출된다.

    CknC _{k}^{n} 이 원시 재귀라고 가정하면 Ck+1n(x1,,xn)C _{k+1}^{n}(x_1, \dots, x_n) 은 치환 Ck+1n(x1,,xn)=N(Ckn(x1,,xn))C _{k+1}^{n}(x_1, \dots, x_n) = N(C _{k}^{n}(x_1, \dots, x_n)) 에 의하여 원시 재귀이다.

    3:

    정리 3.14 에 의하여 x1,,xnx_1, \dots, x_n 중에서 함수에 나타나지 않은 임의의 변수는 더미 변수로써 추가될 수 있다. ■

  • 예시

    3) 의 예시로 h(x1,x3)h(x_1, x_3) 이 원시 재귀라면 h(x1,x2,x3)=h(x1,x3)=h(U13(x1,x2,x3),U33(x1,x2,x3))h ^{*}(x_1, x_2 , x_3) = h(x_1, x_3) = h(U _{1}^{3}(x_1,x_2,x_3), U _{3}^{3}(x_1, x_2, x_3)) 도 치환에 의하여 얻어진 원시 재귀이다.

정리 3.16

다음 함수는 원시 재귀이다.

  1. x+yx+y
  2. xyx \cdot y
  3. xyx ^{y}
  4. δ(x)={x1x>00x=0\delta(x) = \begin{cases} x-1 &x>0\\ 0 &x=0\\ \end{cases}
  5. x ˙y={xyxy0x<yx \dotdiv y = \begin{cases} x-y &x \geq y\\ 0 &x < y\\ \end{cases}
  6. xy={xyxyyxx<y|x - y| = \begin{cases} x - y &x \geq y\\ y - x &x < y\\ \end{cases}
  7. sg(x)={0x=01x0\operatorname{sg} (x) = \begin{cases} 0 &x=0\\ 1 &x \neq 0\\ \end{cases}
  8. mover(x)={1x=00x0\overline{\operatorname{sg} }(x) = \begin{cases} 1 &x=0\\ 0 &x \neq 0\\ \end{cases}
  9. x!x!
  10. min(x,y)\min (x,y)
  11. min(x1,x2,,xn)\min (x_1, x_2, \dots, x_n)
  12. max(x,y)\max (x,y)
  13. max(x1,x2,,xn)\max (x_1, x_2, \dots, x_n)
  14. rm(x,y)\operatorname{rm} (x, y) (yyxx 로 나눈 나머지)
  15. qt(x,y)\operatorname{qt} (x, y) (yyxx 로 나눈 몫)
  • 4) 의 δ\delta 를 이전수 함수(predecessor)라고 한다.

  • 증명

유계 합(bounded sum), 유계 곱(bounded product)

유계 합과 곱을 다음과 같이 정의한다.

y<zf(x1,,xn,y)={0z=0f(x1,,xn,0)++f(x1,,xn,z1)z>0\quad \displaystyle \sum_{y<z}^{}f(x_1, \dots, x_n,y) = \begin{cases} 0 & z = 0\\ f(x_1, \dots, x_n, 0) + \dots + \\ \quad f(x_1, \dots, x_n, z - 1) & z > 0\\ \end{cases}

yzf(x1,,xn,y)=y<z+1f(x1,,xn,y)\quad \displaystyle \sum_{y \leq z}^{}f(x_1, \dots, x_n,y) = \sum_{y<z+1}^{}f(x_1, \dots, x_n,y)

y<zf(x1,,xn,y)={1z=0f(x1,,xn,0)f(x1,,xn,z1)z>0\quad \displaystyle \prod_{y<z}^{}f(x_1, \dots, x_n,y) = \begin{cases} 1 & z = 0\\ f(x_1, \dots, x_n, 0) \dots \\ \quad f(x_1, \dots, x_n, z - 1) & z > 0\\ \end{cases}

yzf(x1,,xn,y)=y<z+1f(x1,,xn,y)\quad \displaystyle \prod_{y \leq z}^{}f(x_1, \dots, x_n,y) = \prod_{y<z+1}^{}f(x_1, \dots, x_n,y)

다음과 같이 이중 유계 합과 곱을 정의할 수 있다.

u<y<vf(x1,,xn,y)=f(x1,,xn,0)++f(x1,,xn,z1)=y<δ(v ˙u)f(x1,,xn,y+u+1)\begin{align}\begin{split} \sum_{u<y<v}^{}f(x_1, \dots, x_n,y) &= f(x_1, \dots, x_n, 0) + \dots\\ &\qquad + f(x_1, \dots, x_n, z - 1) \\ &=\sum_{y<\delta(v \dotdiv u)}^{}f(x_1, \dots, x_n,y+u+1) \\ \end{split}\end{align} \tag*{}
  • 유계 합과 곱은 x1,x2,,xn,zx_1, x_2, \dots, x_n, z 에 대한 함수이다.

정리 3.17

f(x1,x2,,xn,y)f(x_1, x_2, \dots, x_n,y) 가 원시 재귀(또는 재귀)이면 위에서 정의한 모든 유계 합과 곱은 원시 재귀(또는 재귀)이다.

  • 증명

  • 예시

    xx 의 약수의 수 τ(x)\tau(x) 는 다음과 같이 정의되므로 원시 재귀이다.

    τ(x)=yxmover(rm(y,x)) \tau(x) = \sum_{y \leq x}\overline{\operatorname{sg} }(\operatorname{rm} (y,x))

주어진 수론적 관계들에 명제 논리의 연결사를 적용하면 새로운 관계를 얻을 수 있다. 가령 R1(x,y)R_1(x,y)R2(x,u)R_2(x,u) 에 대하여 R1(x,y)R2(x,u)R_1(x,y) \land R_2(x,u) 를 얻는다.

유계 양화사(bounded quantifier)

유계 보편 양화사를 다음과 같이 정의한다.

  • (y)y<zR(x1,x2,,xn,y)(\forall y)_{y<z}R(x_1, x_2, \dots, x_n,y): 모든 yy 에 대하여 yyzz 보다 작을 때 R(x1,x2,,xn,y)R(x_1, x_2, \dots, x_n,y) 이 성립한다.

유계 존재 양화사를 다음과 같이 정의한다.

  • (y)y<zR(x1,x2,,xn,y)(\exists y)_{y<z}R(x_1, x_2, \dots, x_n,y): R(x1,x2,,xn,y)R(x_1, x_2, \dots, x_n,y) 을 만족시키는 어떤 y(<z)y(< z) 가 존재한다.

(y)yz(\forall y)_{y \leq z}(y)yz(\exists y)_{y \leq z} 도 같은 방식으로 정의한다.

유계 μ\mu-연산자(bounded μ\mu-operator)

μyy<zR(x1,,xn,y)\mu y _{y<z}R(x_1, \dots, x_n,y)R(x1,,xn,y)R(x_1, \dots, x_n,y) 를 만족하는 최소 y(<z)y (< z) 가 존재할 때 yy 라고 정의하고, 그렇지 않을 때 zz 라고 정의한다.

μyyzR(x1,,xn,y)\mu y _{y \leq z}R(x_1, \dots, x_n,y)μyy<z+1R(x1,,xn,y)\mu y _{y<z+1}R(x_1, \dots, x_n,y) 로 정의한다.

  • y(<z)y (<z)RR 이 만족하지 않을 때 zz 라고 정의하는 것은 순전히 앞으로의 증명에 편의성을 위한 인위적인 정의이다.

Primitive Recursive Relation

원시 재귀 관계(primitive recursive relation), 재귀 관계(recursive relation)

관계 R(x1,x2,,xn)R(x_1, x_2, \dots, x_n) 이 원시 재귀(또는 재귀)라는 것은 그것의 특성 함수 CR(x1,x2,,xn)C_R(x_1, x_2, \dots, x_n) 이 원시 재귀(또는 재귀)라는 것과 동치이다.

  • 자연수 집합 AA 가 원시 재귀(또는 재귀)인 것은 그것의 특성 함수 CA(x)C_A(x) 가 원시 재귀(또는 재귀)인 것과 동치이다. 이는 성질 xAx \in A 가 원시 재귀(또는 재귀)라는 것이다.

  • 예시

    관계 x1=x2x_1= x_2 는 그것의 특성함수 sg(x1x2)\operatorname{sg} (|x_1 - x_2|) 가 원시 재귀이므로 원시 재귀이다.

    xx 가 소수라고 주장하는 관계 Pr(x)\operatorname{Pr} (x) 는 원시 재귀이다. msub(x)=sg(τ(x)2)C _{\operatorname{Pr} }(x) = \operatorname{sg} (|\tau(x) - 2|) 이기 때문이다. (정수가 소수일 때에만 약수가 2개 이므로 τ(x)=2\tau(x) = 2 가 되며, 00 인 경우 τ(0)=1\tau(0) = 1 이다.)

정리 3.18

원시 재귀[재귀] 관계들에 명제 연결사나 유계 양화사를 적용하여 얻은 관계는 원시 재귀[재귀]이다.

원시 재귀[재귀] 관계에 유계 μ\mu-연산자 μyy<z\mu y _{y<z}μyyz\mu y _{y \leq z} 를 적용한 관계는 원시 재귀[재귀] 함수이다.

  • 증명

    명제 연결사:

    R1(x1,,xn)R_1(x_1, \dots, x_n)R2(x1,,xn)R_2(x_1, \dots, x_n) 가 원시 재귀[재귀] 관계라고 하자. 그러면 특성함수 CR1C _{R_1}CR2C _{R_2} 도 원시 재귀[재귀]이다.

    C¬R1(x1,,xn)=1 ˙CR1(x1,,xn)C _{\lnot R_1}(x_1, \dots, x_n) = 1 \dotdiv C _{R_1}(x_1, \dots, x_n) 이므로 ¬R1\lnot R_1 은 원시 재귀[재귀]이다.

    CR1R2(x1,,xn)=CR1(x1,,xn)CR2(x1,,xn)C _{R_1 \lor R_2}(x_1, \dots, x_n) = C _{R_1}(x_1, \dots, x_n) \cdot C _{R_2}(x_1, \dots, x_n) 이므로 R1R2R_1 \lor R_2 는 원시 재귀[재귀]이다.

    다른 모든 명제 연결사는 ¬\lnot\lor 로 정의가능하다. ▲

    유계 양화사:

    R(x1,,xn,y)R(x_1, \dots, x_n, y) 가 원시 재귀[재귀]라고 하자. Q(x1,,xn,yz)Q(x_1, \dots, x_n, yz) 가 관계 (y)y<zR(x1,,xn,y)(\exists y)_{y<z}R(x_1, \dots, x_n, y) 이면 CQ(x1,,xn,z)=y<zCR(x1,,xn,y)C_Q(x_1, \dots, x_n, z) = \prod_{y<z}^{}C_R(x_1, \dots, x_n, y) 는 정리 3.17 에 의하여 원시 재귀[재귀]이다.

    유계 양화사 (y)yz(\exists y)_{y \leq z}(y)y<z(\exists y)_{y<z} 로부터 치환에 의하여 얻어진 (y)y<z+1(\exists y)_{y < z+1} 와 같다.

    (y)y<z(\forall y)_{y<z}¬(y)y<z¬\lnot (\exists y)_{y<z}\lnot 과 같고 (y)yz(\forall y)_{y \leq z}¬(y)yz¬\lnot (\exists y) _{y \leq z}\lnot 와 같다.

    (y)u<y<v(\exists y)_{u<y<v} 같은 이중 유계 양화사는 유계 양화사를 사용하여 치환에 의하여 정의될 수 있다. ▲

    μ\mu-연산자:

    uyCR(x1,,xn,u)\prod_{u \leq y}^{}C_R(x_1, \dots, x_n, u) 는 모든 uyu \leq y 에 대하여 R(x1,,xn,u)R(x_1, \dots, x_n, u) 가 거짓이면 모든 yy 에 대하여 값이 11 이다. R(x1,,xn,u)R(x_1, \dots, x_n, u) 를 만족시키는 uyu \leq y 가 존재하면 값은 00 이 된다.

    y<z(uyCR(x1,,xn,u))\sum_{y<z}^{}(\prod_{u \leq y}^{}C_R(x_1, \dots, x_n, u))00 부터 숫자를 세지만, R(x1,,xn,y)R(x_1, \dots, x_n, y) 이 성립하는 첫 y<zy < z 부터는 세지 않는다. 만약 그러한 yy 가 존재하지 않으면 결과값은 zz 가 된다. 그러므로 이는 μyy<zR(x1,,xn,y)\mu y _{y<z}R(x_1, \dots, x_n, y) 와 같고 이는 정리 3.17 에 의하여 원시 재귀[재귀]이다. ■

  • 예시

    xx번째 소수를 나타내는 p(x)p(x) 를 잡자. 즉, p(0)=2,p(1)=3,p(0) = 2, p(1) = 3, \dots 이다. p(x)p(x) 를 편하게 pxp_x 라고 쓰기로 하자.

    pxp_x 가 원시 재귀 함수라는 것을 조사하자. pxp_x 는 다음과 같이 정의된다.

    p0=2 p_0 = 2
    px+1=μyy(px)!+1(px<yPr(y)) p _{x+1} = \mu y _{y \leq (p_x)! + 1}(p_x < y \land \operatorname{Pr} (y))

    먼저 px<yPr(y)p_x < y \land \operatorname{Pr} (y) 는 원시 재귀이다. 그러면 본 정리에 의하여 μyyv(px<yPr(y))\mu y _{y \leq v}(p_x < y \land \operatorname{Pr} (y)) 는 원시 재귀 함수 g(u,v)g(u, v) 이다. 이제 u,vu,vz,z!+1z, z!+1 로 치환하면 다음의 원시 재귀 함수를 얻는다.

    h(z)=μyyz!+1(z<yPr(y)) h (z) = \mu y _{y \leq z! + 1}(z < y \land \operatorname{Pr} (y))

    그렇다면 px+1=h(px)p _{x+1} = h(p_x) 이다. 이제 재귀에 의하여 pxp_x 의 정의를 얻는다. 그러므로 pxp_x 는 원시 재귀이다.

11 보다 큰 양의 정수 xx 는 유일한 소수 인수분해 x=p0a0p1a1pkakx = p_0 ^{a_0}p_1 ^{a_1}\dots p_k ^{a_k} 를 갖는다. 이 인수분해의 aja_j(x)j(x)_j 라고 표기하자. x=1x = 1 이면 모든 jj 에 대하여 (x)j=1(x)_j = 1 라고 하고, x=0x = 0 이면 모든 jj 에 대하여 (x)j=0(x)_j = 0 라고 하자.

그러면 함수 (x)j(x)_j 는 다음과 같이 정의되므로 정리 3.18 에 의하여 원시 재귀이다.

(x)j=μyy<x(pjyx¬(pjy+1x)) (x)_j = \mu y _{y < x}\left( p _{j}^{y} | x \land \neg \left( p _{j}^{y+1} | x \right) \right)
  • 산술의 기본정리11 보다 큰 양의 정수 xx 는 유일한 소수 인수분해를 갖는다는 것을 보장해준다.

길이 함수(length function)

x>0x>0 에 대하여 lh(x)\operatorname{lh}(x)xx 의 소수 인수분해에서 영이 아닌 지수의 개수, 즉, xx 를 나눌 수 있는 서로 다른 소수의 개수라고 하자. lh(0)=0\operatorname{lh}(0) = 0 으로 두자.

R(x,y)R(x, y) 을 원시 재귀 관계 Pr(y)yxx0\operatorname{Pr} (y) \land y|x \land x \neq 0 로 두면 lh(x)=yxmover(CR(x,y))\operatorname{lh}(x) = \sum _{y \leq x} \overline{\operatorname{sg}} (C_R(x, y)) 이다. 그러면 정리 3.18 에 의하여 lh\operatorname{lh} 는 원시 재귀이다.

  • lh\operatorname{lh} 는 length 를 뜻한다.

병렬 함수(juxtaposition function)

양의 정수열 a0,a1,,aka_0, a_1, \dots, a_k 를 나타내는 수 x=2a03a1pkakx = 2 ^{a_0}3 ^{a_1}\dots p _{k}^{a_k} 와 양의 정수열 b0,b1,,bmb_0, b_1, \dots, b_m 를 나타내는 수 y=2b03b1pmbmy = 2 ^{b_0}3 ^{b_1}\dots p _{m}^{b_m} 에 대하여 다음과 같이 정의한다.

xy=2a03a1pkakpk+1b0pk+2b1pk+1+mbm x * y = 2 ^{a_0}3 ^{a_1}\dots p _{k}^{a_k}p _{k+1}^{b_0}p _{k+2}^{b_1}\dots p _{k+1+m}^{b_m}

lh(x)=k+1,lh(y)=m+1,bj=(y)j\operatorname{lh}(x) = k+1, \operatorname{lh}(y) = m+1, b_j = (y)_j 이므로 다음이 성립하고, 따라서 * 는 원시 재귀 함수이다.

xy=x×j<lh(y)(plh(x)+j)(y)j x * y = x \times \prod_{j < \operatorname{lh}(y)}^{}(p _{\operatorname{lh}(x) + j})^{(y)_j}

문제 3.16

R(x1,,xn,y)R(x_1, \dots, x_n,y) 이 원시 재귀(또는 재귀) 관계이면 다음이 성립한다.

  1. (y)u<y<vR(x1,,xn,y)(\exists y)_{u<y<v}R(x_1, \dots, x_n, y)(y)uyvR(x1,,xn,y)(\exists y)_{u \leq y \leq v}R(x_1, \dots, x_n, y)(y)uy<vR(x1,,xn,y)(\exists y)_{u \leq y < v}R(x_1, \dots, x_n, y) 는 원시 재귀(또는 재귀) 관계이다.
  2. μyu<y<vR(x1,,xn,y)\mu y _{u<y<v}R(x_1, \dots, x_n, y)μyuyvR(x1,,xn,y)\mu y _{u \leq y \leq v}R(x_1, \dots, x_n, y)μyuy<vR(x1,,xn,y)\mu y _{u \leq y < v}R(x_1, \dots, x_n, y) 는 원시 재귀(또는 재귀) 함수이다.
  3. 모든 자연수 x1,,xnx_1, \dots, x_n 에 대하여 R(x1,,xn,y)R(x_1, \dots, x_n, y) 인 자연수 yy 가 존재하면 함수 f(x1,,xn)=μyR(x1,,xn,y)f(x_1, \dots, x_n) = \mu yR(x_1, \dots, x_n, y) 는 재귀이다.
  • 증명

정리 3.19

다음과 같이 정의하자.

f(x1,,xn)={g1(x1,,xn)R1(x1,,xn) is trueg2(x1,,xn)R2(x1,,xn) is truegk(x1,,xn)Rk(x1,,xn) is true f(x_1, \dots, x_n) = \begin{cases} g_1(x_1, \dots, x_n) & R_1(x_1, \dots, x_n) \text{ is true}\\ g_2(x_1, \dots, x_n) & R_2(x_1, \dots, x_n) \text{ is true}\\ & \vdots \\ g_k(x_1, \dots, x_n) & R_k(x_1, \dots, x_n) \text{ is true}\\ \end{cases}

함수 g1,g2,,gkg_1, g_2, \dots, g_k 와 관계 R1,R2,,RkR_1, R_2, \dots, R_k 가 원시 재귀(또는 재귀)이고, 임의의 x1,x2,,xnx_1, x_2, \dots, x_n 에 대하여 관계 R1,R2,,RkR_1, R_2, \dots, R_k 중 오직 하나만 참이면, ff 는 원시 재귀(또는 재귀)이다.

  • 증명

    f(x1,,xn)=g1(x1,,xn)mover(CR1(x1,,xn))++gk(x1,,xn)mover(CRk(x1,,xn)) \begin{align}\begin{split} f(x_1, \dots, x_n) &=g_1(x_1, \dots, x_n) \cdot \overline{\operatorname{sg} }(C _{R_1}(x_1, \dots, x_n)) \\ & \qquad + \dots +g_k(x_1, \dots, x_n) \cdot \overline{\operatorname{sg} }(C _{R_k}(x_1, \dots, x_n))\\ \end{split}\end{align} \tag*{}

Course-of-Values Recursion

정리 3.20 Course-of-Values 재귀

f#(x1,,xn,y)=u<ypuf(x1,,xn,u)f\#(x_1, \dots, x_n,y) = \prod_{u<y}^{}p _{u}^{f(x_1, \dots, x_n,u)} 라고 하자. 이때 fff#f\# 로부터 f(x1,,xn,y)=(f#(x1,,xn,y+1))yf(x_1, \dots, x_n, y) = (f\#(x_1, \dots, x_n, y+1))_y 와 같이 얻을 수 있다.

h(x1,,xn,y,z)h(x_1, \dots, x_n,y,z) 가 원시 재귀(또는 재귀) 이고 f(x1,,xn,y)=h(x1,,xn,yf#(x1,,xn,y))f(x_1, \dots, x_n,y) = h(x_1, \dots, x_n,yf\#(x_1, \dots, x_n,y)) 이면 ff 는 원시 재귀(또는 재귀)이다.

  • f(x1,x2,,xn,y+1)f(x_1, x_2, \dots, x_n, y+1) 의 값이 f(x1,x2,,xn,y)f(x_1, x_2, \dots, x_n,y) 에만 의존하는 것이 아니라 uyu \leq y 에 대한 모든 f(x1,x2,,xn,u)f(x_1, x_2, \dots, x_n,u) 의 값에 의존하는 재귀에 의하여 정의된 함수도 있다. 이런 종류의 재귀를 course-of-values 재귀라고 한다.

  • 자연수 순서쌍 집합과 자연수 집합 사이의 원시 재귀 일대일 대응을 갖는 것은 때때로 중요하다. 자연수 순서쌍을 나열하면 다음과 같다.

    (0,0),(0,1),(1,0),(1,1),(0,2),(2,0),(1,2),(2,1),(2,2), (0,0), \enspace (0,1),(1,0),(1,1), \enspace (0,2),(2,0),(1,2),(2,1),(2,2),\dots

    kk를 포함하는 순서쌍까지 나열을 했다면, 다음의 방식으로 k+1k+1를 포함하는 순서쌍 그룹을 얻는다.

    (0,k+1),(k+1,0),(1,k+1),(k+1,1),,(k,k+1),(k+1,k),(k+1,k+1) (0, k+1), (k+1, 0), (1, k+1), (k+1, 1), \dots , \\ (k, k+1),(k+1, k), (k+1, k+1)

    이 그룹은 k+1k+1번째 그룹이다.

    x<yx<y 라고 하자.

    처음 yy번째 그룹들은 y2y ^{2}개의 쌍을 갖고, (x,y)(x, y)y+1y+1번째 그룹의 2x+12x+1번째 쌍이다. 그러므로 (x,y)(x, y) 는 전체 순서쌍에서 y2+2x+1y ^{2}+2x+1번째 쌍이고, (y,x)(y,x)y2+2x+2y ^{2}+2x+2번째 쌍이다. x=yx = y 인 경우 (x,y)(x, y)(x+1)2(x +1)^{2}번째 쌍이다.

    따라서 순서쌍 (x,y)(x, y)의 위치를 나타내는 함수 σ2(x,y)\sigma ^{2}(x, y) 를 다음과 같이 정의할 수 있다.

    σ2(x,y)=sg(x ˙y)(x2+2y+1)+mover(x ˙y)(y2+2x) \sigma ^{2}(x, y) = \operatorname{sg} (x \dotdiv y) \cdot (x ^{2} + 2y + 1) + \overline{\operatorname{sg} }(x \dotdiv y)\cdot (y ^{2}+2x)

    σ2\sigma ^{2} 는 명백하게 원시 재귀이다. 이제 다음을 만족하는 역함수 σ12,σ22\sigma _{1}^{2}, \sigma _{2}^{2} 를 정의하자.

    σ12(σ2(x,y))=x,σ22(σ2(x,y))=y,σ2(σ12(z),σ22(z))=z \sigma _{1}^{2}(\sigma ^{2}(x, y)) = x, \sigma _{2}^{2}(\sigma ^{2}(x, y)) = y , \sigma ^{2}(\sigma _{1}^{2}(z), \sigma _{2}^{2}(z)) = z

    즉, σ12(z),σ22(z)\sigma _{1}^{2}(z), \sigma _{2}^{2}(z) 는 각각 zz번째 순서쌍의 첫번째, 두번째 성분이다.

    이제 다음이 성립한다.

    σ12(0)=0,σ22(0)=0 \sigma _{1}^{2}(0) = 0, \sigma _{2}^{2}(0) = 0
    σ12(n+1)={σ22(n)σ12(n)<σ22(n)σ22(n)+1σ12(n)>σ22(n)0σ12(n)=σ22(n) \sigma _{1}^{2}(n + 1) = \begin{cases} \sigma _{2}^{2}(n) & \sigma _{1}^{2}(n) < \sigma _{2}^{2}(n)\\ \sigma _{2}^{2}(n) + 1 & \sigma _{1}^{2}(n) > \sigma _{2}^{2}(n)\\ 0 & \sigma _{1}^{2}(n) = \sigma _{2}^{2}(n)\\ \end{cases}
    σ22(n+1)={σ12(n)σ12(n)σ22(n)σ12(n)+1σ12(n)=σ22(n) \sigma _{2}^{2}(n + 1) = \begin{cases} \sigma _{1}^{2}(n) & \sigma _{1}^{2}(n) \neq \sigma _{2}^{2}(n)\\ \sigma _{1}^{2}(n) + 1 & \sigma _{1}^{2}(n) = \sigma _{2}^{2}(n)\\ \end{cases}

    그러므로 다음이 성립한다.

    σ12(n+1)=σ22(n)(sg(σ22(n) ˙σ12(n)))+(σ22(n)+1)(sg(σ12(n) ˙σ22(n)))=ϕ(σ12(n),σ22(n)) \begin{align}\begin{split} \sigma _{1}^{2}(n+1)&= \sigma _{2}^{2}(n) \cdot (\operatorname{sg} (\sigma _{2}^{2}(n) \dotdiv \sigma _{1}^{2}(n))) +\\ &\qquad (\sigma _{2}^{2}(n)+1) \cdot (\operatorname{sg} (\sigma _{1}^{2}(n) \dotdiv \sigma _{2}^{2}(n))) \\ &= \phi (\sigma _{1}^{2}(n) , \sigma _{2}^{2}(n)) \\ \end{split}\end{align} \tag*{}
    σ22(n+1)=σ12(n)(sg(σ22(n)σ12(n)))+(σ12(n)+1)(mover(σ12(n)σ22(n)))=ψ(σ12(n),σ22(n)) \begin{align}\begin{split} \sigma _{2}^{2}(n+1)&= \sigma _{1}^{2}(n) \cdot (\operatorname{sg} (|\sigma _{2}^{2}(n) - \sigma _{1}^{2}(n)|)) +\\ &\qquad (\sigma _{1}^{2}(n)+1) \cdot (\overline{\operatorname{sg}} (|\sigma _{1}^{2}(n) - \sigma _{2}^{2}(n)|)) \\ &= \psi (\sigma _{1}^{2}(n) , \sigma _{2}^{2}(n)) \\ \end{split}\end{align} \tag*{}

    ϕ\phiψ\psi 는 원시 재귀 함수이다. 따라서 σ12,σ22\sigma _{1}^{2}, \sigma _{2}^{2} 는 재귀적으로 정의된 것이다. 이제 σ12,σ22\sigma _{1}^{2}, \sigma _{2}^{2} 가 원시 재귀임을 보일 수 있다.

    h(u)=2σ12(u)3σ22(u)h(u) = 2 ^{\sigma _{1}^{2}(u)}3 ^{\sigma _{2}^{2}(u)} 로 두면 hh 는 원시 재귀이다. h(0)=2σ12(0)3σ22(0)=2030=1h(0) = 2 ^{\sigma _{1}^{2}(0)}3 ^{\sigma _{2}^{2}(0)} = 2 ^{0} \cdot 3 ^{0} = 1 이고 다음이 성립하기 때문이다.

    h(n+1)=2σ12(n+1)3σ22(n+1)=2ϕ(σ12(n),σ22(n))3ψ(σ12(n),σ22(n))=2ϕ((h(n))0,(h(n))1)3ψ((h(n))0,(h(n))1) \begin{align}\begin{split} h(n+1)&=2 ^{\sigma _{1}^{2}(n+1)}3 ^{\sigma _{2}^{2}(n+1)} \\ &=2 ^{\phi (\sigma _{1}^{2}(n), \sigma _{2}^{2}(n))}3 ^{\psi(\sigma _{1}^{2}(n), \sigma _{2}^{2}(n))} \\ &=2 ^{\phi ((h(n))_0, (h(n))_1)}3 ^{\psi((h(n))_0, (h(n))_1)} \end{split}\end{align} \tag*{}

    정리 3.18 예시에서처럼 함수 (x)i(x)_i 는 원시 재귀이므로 hh 도 원시 재귀이다. 그런데 σ12(x)=(h(x))0\sigma _{1}^{2}(x) = (h(x))_0 이고 σ22(x)=(h(x))1\sigma _{2}^{2}(x) = (h(x))_1 이므로 치환에 의하여 σ12,σ22\sigma _{1}^{2}, \sigma _{2}^{2} 도 원시 재귀이다.

    자연수의 모든 n-튜플 과 모든 자연수 사이의 원시 재귀 일대일 대응을 nn에 대한 귀납으로 보일 수 있다. n=2n=2 의 경우를 지금까지 보인 것이다.

  • 증명

    다음이 성립한다.

    f#(x1,,xn,0)=1f#(x1,,xn,y+1)=f#(x1,,xn,y)pyf(x1,,xn,y)=f#(x1,,xn,y)pyh(x1,,xn,y,f#(x1,,xn,y))\begin{align}\begin{split} f\#(x_1, \dots, x_n, 0)&= 1\\ f\#(x_1, \dots, x_n, y+1)&= f\#(x_1, \dots, x_n, y) \cdot p _{y}^{f(x_1, \dots, x_n,y)} \\ &= f\#(x_1, \dots, x_n, y) \cdot p _{y}^{h(x_1, \dots, x_n, y, f\#(x_1, \dots, x_n, y))} \\ \end{split}\end{align} \tag*{}

    치환 규칙에 의하여 f#f\# 은 원시 재귀(또는 재귀) 이고 f(x1,,xn,y)=(f#(x1,,xn,y+1))yf(x_1, \dots, x_n,y) = (f\#(x_1, \dots, x_n, y+1))_y 이므로 ff 도 원시 재귀(또는 재귀)이다. ■

  • 예시

    피보나치 수열은 이렇게 정의된다. f(0)=1,f(1)=1f(0) = 1, f(1) = 1, k0k \geq 0 에 대하여 f(k+2)=f(k)+f(k+1)f(k +2) = f(k) + f(k + 1). 그러면 ff 는 다음과 같기 때문에 원시 재귀이다.

    f(n)=mover(n)+mover(n1)+((f#(n))n ˙1+(f#(n))n ˙2)sg(n ˙1) f(n) = \overline{\operatorname{sg}} (n) + \overline{\operatorname{sg}} (|n-1|) + ((f\#(n))_{n \dotdiv 1} + (f\#(n))_{n \dotdiv 2}) \cdot \operatorname{sg} (n \dotdiv 1)

    함수

    h(y,z)=mover(y)+mover(y1)+((z)y ˙1+(z)y ˙2)sg(y ˙1) h(y, z) = \overline{\operatorname{sg}} (y) + \overline{\operatorname{sg}} (|y - 1|) + ((z) _{y \dotdiv 1} + (z)_{y \dotdiv 2})\cdot \operatorname{sg} (y \dotdiv 1)

    는 원시 재귀이고, f(n)=h(n,f#(n))f(n) = h(n, f\#(n)) 이다.

따름정리 3.21 관계에서의 Course-of-Values 재귀

H(x1,,xn,y,z)H(x_1, \dots, x_n, y, z) 가 원시 재귀(또는 재귀) 관계이고 R(x1,,xn,y)R(x_1, \dots, x_n, y) 가 성립하는 것이 RR 의 특성함수 CRC_R 에 대한 다음과 동치라면, RR 은 원시 재귀(또는 재귀)이다.

H(x1,,xn,y,(CR)#(x1,,xn,y))H(x_1, \dots, x_n, y, (C_R)\#(x_1, \dots, x_n, y))
  • 증명

Godel's β-Function

보조정리 3.22 괴델의 베타함수(Godel's β\beta-Function)

β(x1,x2,x3)=rm(1+(x3+1)x2,x1)\beta(x_1,x_2,x_3) = \operatorname{rm} (1 + (x_3 + 1) \cdot x_2, x_1) 라고 하자. 정리 3.16(14) 에 의하여 β\beta 는 원시 재귀이다.

또한, β\beta 는 다음의 wff Bt(x1,x2,x3,y)\operatorname{Bt} (x_1,x_2,x_3,y) 에 의하여 SS 에서 강력하게 표현가능하다.

(w)(x1=(1+(x3+1)x2)w+yy<1+(x3+1)x2) (\exists w)(x_1 = (1 + (x_3 + 1)\cdot x_2) \cdot w + y \land y < 1 + (x_3 + 1) \cdot x_2 )
  • 증명

보조정리 3.23

임의의 자연수열 k0,k1,,knk_0, k_1, \dots, k_n 마다 다음을 만족시키는 자연수 b,cb,c 가 존재한다.

  • 0in0 \leq i \leq n 에 대하여 β(b,c,i)=ki\beta(b,c,i) = k_i.
  • 증명

Recursive is Representable in S

정리 3.24

모든 재귀 함수는 SS 에서 표현가능하다.

  • 이 정리가 지금까지의 결론이다. 이는 중요하고 근본적인 정리이다.

    보조정리 3.22, 3.23 에 의하여 유한한 자연수열을 SS 안에서 표현할 수 있게 되었다. 이 능력이 본 정리의 증명에서 핵심 역할을 한다.

  • 증명

    초기함수와 치환으로 얻은 함수의 표현가능성에 의하여 초기 함수 Z,N,UinZ,N,U _{i}^{n}SS 에서 표현가능하고, 치환은 표현가능성을 보존한다. ▲

    (이제 재귀와 μ\mu-연산자가 표현가능성을 보존하는 것을 증명하면 된다. 이 증명은 쉽지만 길고 지루하다.(p188))

따름정리 3.25

모든 재귀 관계는 SS 에서 표현가능하다.

  • 증명

    R(x1,,xn)R(x_1, \dots, x_n) 이 재귀 관계이면 그 특성함수 CRC_R 은 재귀이다. 정리 3.24 에 의하여 CRC_RSS 에서 표현가능하고 정리 3.13 에 의하여 RRSS 에서 표현가능하다. ■

Arithmetization: Godel Numbers

괴델수(godel number)

임의의 1차 이론 KK 의 각 기호 uu 에 다음과 같은 방식으로 양의 홀수 정수 g(u)g(u) 를 대응시키고, 이를 괴델수라고 한다.

(( )) ,, ¬\neg \implies \forall
33 55 77 99 1111 1313
xkx_k aka_k fknf _{k}^{n} AknA _{k}^{n}
13+8k13 + 8k 7+8k7 + 8k 1+8(2n3k)1 + 8(2 ^{n}3 ^{k}) 3+8(2n3k)3 + 8 (2 ^{n}3 ^{k})

KK 의 기호 uju_j 에 대한 식 u0,u1,,uru_0, u_1, \dots, u_r 에는 p0=2p_0 = 2 로 시작하는 jj번째 소수 pjp_j 에 대하여 다음과 같은 괴델수를 부여한다.

g(u0,u1,,ur)=2g(u0)3g(u1)prg(ur) g(u_0, u_1, \dots, u_r) = 2 ^{g(u_0)}3 ^{g(u_1)}\dots p_r ^{g(u_r)}

KK 의 유한한 식의 열 e0,e1,,ere_0, e_1, \dots, e_r 에는 다음과 같은 괴델수를 부여한다.

g(e0,e1,,er)=2g(e0)3g(e1)prg(er)g(e_0, e_1, \dots, e_r) = 2 ^{g(e_0)}3 ^{g(e_1)}\dots p_r ^{g(e_r)}
  • 이 방법은 괴델에 의하여 메타수학(metamathematic)을 산술화(arithmetization)하기 위하여 고안되었다. 즉, 형식 체계의 주장을 동등한 수론적 명제로 교체하고 이 명제를 수론 체계 내에서 표현하는 것이다. 이 아이디어는 수리논리학의 많은 문제에 열쇠가 되었다.

    괴델수는 체계를 산술화하는 유일한 방법이 아니다. 이후 다른 방법들도 고안되었다.

  • 괴델수를 88 로 나누었을 때 uu 가 변수이면 g(u)g(u) 의 나머지는 55, uu 가 개별 상수일 때 나머지는 77, uu 가 함수 기호일 때 나머지는 11, uu 가 술어 기호일 때 나머지는 33 이다.

    서로 다른 식은 산술의 기본정리에 의하여 서로 다른 괴델수를 갖게 된다.

    식은 짝수 괴델수를 갖고, 기호는 홀수 괴델수를 갖는다.

    서로 다른 식의 열은 서로 다른 괴델수를 갖는다. 식의 열의 괴델수는 짝수이고 그것의 22 의 제곱 또한 짝수이므로, 이것은 기호나 식의 괴델수와는 다르다.

    그러므로 ggKK 의 기호와 식과 식의 유한 열의 집합을 양의 정수 집합으로 보내는 단사 함수이다. gg 가 전사는 아니다. 가령, 1010 은 괴델수가 아니다.

  • 단일 기호라도 식으로 취급되면 다른 괴델 수를 갖게 된다. 가령, 기호 x1x_1 이 괴델수 2121 를 갖지만, 식으로 취급되면 괴델수 2212 ^{21} 를 갖는다.

  • 식의 열에 할당되는 괴델수는 KK 에 존재하는 증명에 수를 할당하기 위함이다.

  • 예시

    g(x2)=29,g(a4)=39,g(f12)=97,g(A21)=147 g(x_2) = 29, g(a_4) = 39, g(f _{1}^{2}) = 97, g(A _{2}^{1}) = 147
  • 예시

    g(A12(x1,x2))=2g(A12)3g(()5g(x1)7g(,)11g(x2)13g())=29933521771129135 \begin{align}\begin{split} g \left( A _{1}^{2}(x_1, x_2) \right)&= 2 ^{g(A _{1}^{2})}3 ^{g(()}5 ^{g(x_1)}7 ^{g(,)}11 ^{g(x_2)}13 ^{g())}\\ &= 2 ^{99}3 ^{3}5 ^{21}7 ^{7}11 ^{29}13 ^{5}\\ \end{split}\end{align} \tag*{}

Primitive Recursive Vocabulary

원시 재귀[재귀] 어휘(primitive recursive[recursive] vocabulary)

이론 KK 가 원시 재귀 어휘(또는 재귀 어휘)를 갖는다는 것은 다음의 성질들이 원시 재귀(또는 재귀)라는 것이다.

  1. IC(x)\operatorname{IC} (x): xxKK 의 개별 상수의 괴델수이다.

    가령, KK 의 개별 상수가 aj1,aj2,,ajna _{j_1}, a _{j_2}, \dots ,a _{j_n} 로써 유한하면 IC(x)\operatorname{IC} (x) 는 다음과 동치이다.

    x=7+8j1x=7+8j2x=7+8jn x = 7+8 j_1 \lor x = 7 + 8j_2 \lor \dots \lor x = 7 + 8j_n
  2. FL(x)\operatorname{FL} (x): xxKK 의 함수 기호의 괴델수이다.

  3. PL(x)\operatorname{PL} (x): xxKK 의 술어 기호의 괴델수이다.
  • 이로써 이 성질들은 괴델수에 의하여 순수한 자연수로 환원가능하다.

임의의 이론 KK 가 유한한 수의 개별 상수, 함수 기호, 술어 기호를 가지면, 원시 재귀 어휘를 갖는다.

그러므로 산술의 언어 LA\mathcal{L}_A 의 임의의 이론 KK 는 원시 재귀 어휘를 갖는다. 특히, SS 도 원시 재귀 어휘를 갖는다.

  • 증명

    가령, KK 의 개별 상수가 aj1,aj2,,ajna _{j_1}, a _{j_2}, \dots ,a _{j_n} 라면 IC(x)\operatorname{IC} (x) 는 다음과 동치이다.

    x=7+8j1x=7+8j2x=7+8jn x = 7+8 j_1 \lor x = 7 + 8j_2 \lor \dots \lor x = 7 + 8j_n

    FL(x)\operatorname{FL} (x)PL(x)\operatorname{PL} (x) 도 원시 재귀라는 것을 쉽게 보일 수 있다. ■

정리 3.26 원시 재귀[재귀] 어휘를 갖는 이론에서 원시 재귀[재귀]가 되는 관계와 함수

원시 재귀(또는 재귀) 어휘를 갖는 이론 KK 에서 다음의 관계와 함수들은 원시 재귀(또는 재귀)이다. (각 항목마다 표기와 정의를 쓴 다음 그것의 원시 재귀성(또는 재귀성)이 연역될 수 있는 식을 쓰자.)

  1. EVbl(x)\operatorname{EVbl} (x): xx 는 변수로 구성된 식의 괴델수이다.

    (z)z<x(1zx=213+8z)(\exists z)_{z<x}(1 \leq z \land x = 2 ^{13 + 8z})

    EIC(x)\operatorname{EIC} (x): xx 는 개별 상수로 구성된 식의 괴델수이다.

    (y)y<x(IC(y)x=2y)(\exists y)_{y<x}(\operatorname{IC} (y)\land x = 2 ^{y})

    EFL(x)\operatorname{EFL} (x): xx 는 함수 기호로 구성된 식의 괴델수이다.

    (y)y<x(FL(y)x=2y)(\exists y)_{y<x}(\operatorname{FL} (y)\land x = 2 ^{y})

    EPL(x)\operatorname{EPL} (x): xx 는 술어기호로 구성된 식의 괴델수이다.

    (y)y<x(PL(y)x=2y)(\exists y)_{y<x}(\operatorname{PL} (y) \land x = 2 ^{y})
  2. ArgT(x)=(qt(8,x ˙1))0\operatorname{Arg}_{\text{T}} (x) = (\operatorname{qt} (8, x \dotdiv 1))_0: xx 가 함수 기호 fjnf _{j}^{n} 의 괴델수이면 ArgT(x)=n\operatorname{Arg}_{\text{T}} (x) = n 이다.

    ArgP(x)=(qt(8,x ˙3))0\operatorname{Arg}_{\text{P}} (x) = (\operatorname{qt} (8, x \dotdiv 3))_0: xx 가 술어 기호 AjnA _{j}^{n} 의 괴델수이면 ArgP(x)=n\operatorname{Arg}_{\text{P}} (x) = n 이다.

  3. Gd(x)\operatorname{Gd}(x): xxKK 의 식의 괴델수이다.

    EVbl(x)EIC(x)EFL(x)EPL(x)x=23x=25x=27x=29x=211x=213(u)u<x(v)v<x(x=uvGd(u)Gd(v)) \operatorname{EVbl} (x) \lor \operatorname{EIC} (x) \lor \operatorname{EFL} (x) \lor \operatorname{EPL} (x) \lor \\ x = 2 ^{3} \lor x = 2 ^{5} \lor x = 2 ^{7} \lor x = 2 ^{9} \lor x = 2 ^{11} \lor x = 2 ^{13} \lor \\ (\exists u)_{u<x}(\exists v)_{v<x}(x = u * v \land \operatorname{Gd}(u) \land \operatorname{Gd}(v))
  4. MP(x,y,z)\operatorname{MP}(x,y,z): 괴델수 zz 를 갖는 식이 각각 괴델수 x,yx, y 를 갖는 식의 MP 에 의한 직접적 귀결이다.

    y=23x211z25Gd(x)Gd(z) y = 2 ^{3} * x * 2 ^{11} * z * 2 ^{5} \land \operatorname{Gd}(x) \land \operatorname{Gd}(z)
  5. Gen(x,y)\operatorname{Gen}(x, y): 괴델수 yy 를 가진 식이 괴델수 xx 를 가진 식으로부터 일반화 규칙에 의하여 연역되었다.

    (v)v<y(EVbl(v)y=2323213v25x25Gd(x)) (\exists v)_{v<y}(\operatorname{EVbl} (v) \land \\ y = 2 ^{3} * 2 ^{3} * 2 ^{13} * v * 2 ^{5} * x * 2 ^{5} \land \operatorname{Gd}(x))
  6. Trm(x)\operatorname{Trm}(x): xxKK 의 항의 괴델수이다. 항은 변수 또는 상수 또는 함수기호 fknf _{k}^{n} 와 항 t1,,tnt_1, \dots, t_n 에 대한 fkn(t1,,tn)f _{k}^{n}(t_1, \dots, t_n) 이다. 후자가 성립한다는 것은 다음의 n+1n+1 개의 식의 열이 존재한다는 것과 동치이다.

    fkn(,fkn(t1,fkn(t1,,tn1,fkn(t1,,tn) f _{k}^{n}(, \quad f _{k}^{n}(t_1, \quad \dots f _{k}^{n}(t_1, \dots, t _{n-1}, \quad f _{k}^{n}(t_1, \dots, t_n)

    fkn(t1,,tn)f _{k}^{n}(t_1, \dots, t_n) 의 괴델수를 xx 라고 하고 이 열을 나타내는 괴델수를 yy 라고 하자. 명백하게 다음이 성립한다.

    y<2x3xpnx=(23pn)x<(pn!)x<(px!)x y < 2 ^{x}3 ^{x} \dots p _{n}^{x} = (2 \cdot 3 \dots p_n)^{x} < (p_n!) ^{x} < (p_x!) ^{x}

    또한, lh(y)=n+1\operatorname{lh}(y) = n+1 이고 n=ArgT((x)0)n = \operatorname{Arg}_{\text{T}} ((x)_0) 이므로 Trm(x)\operatorname{Trm}(x) 는 다음과 같다.

    EVbl(x)EIC(x)(y)y<(px!)x[x=(y)lh(y) ˙1lh(y)=ArgT((x)0)+1FL(((y)0)0)((y)0)1=3lh((y)0)=2(u)u<lh(y) ˙2(v)v<x((y)u+1=(y)uv27Trm(v))(v)v<x((y)lh(y) ˙1=(y)lh(y) ˙2v25Trm(v))] \begin{align}\begin{split} &\operatorname{EVbl} (x) \lor \operatorname{EIC} (x) \lor (\exists y) _{y < (p_{x}!)^{x}} \Big [ x = (y) _{\operatorname{lh}(y) \dotdiv 1} \land \\ & \qquad \operatorname{lh}(y) = \operatorname{Arg}_{\text{T}} ((x)_0) + 1 \land \operatorname{FL} (((y)_0)_0) \land \\ & \qquad ((y)_0)_1 = 3 \land \operatorname{lh}((y)_0) = 2 \land \\ & \qquad (\forall u) _{u < \operatorname{lh}(y)\dotdiv 2}(\exists v)_{v<x}\big ((y)_{u+1} = (y)_{u}*v*2 ^{7} \land \operatorname{Trm}(v)\big )\land \\ & \qquad (\exists v)_{v<x}\big ((y)_{\operatorname{lh}(y)\dotdiv 1} = (y)_{\operatorname{lh}(y) \dotdiv 2} * v * 2 ^{5} \land \operatorname{Trm}(v)\big )\Big ] \\ \end{split}\end{align} \tag*{}
  7. Atfml(x)\operatorname{Atfml}(x): xxKK 의 원자 wff 의 괴델수이다. 이는 항 t1,,tnt_1, \dots, t_n 와 술어 기호 AknA _{k}^{n} 가 존재하여 Akn(t1,,tn)A _{k}^{n}(t_1, \dots, t_n) 가 괴델수 xx 를 갖는다는 것과 동치이다. 이는 다음의 n+1n+1 개의 식의 열이 존재한다는 것과 동치이다.

    Akn(,Akn(t1,Akn(t1,,tn1,Akn(t1,,tn) A _{k}^{n}(, \quad A _{k}^{n}(t_1, \quad \dots \quad A _{k}^{n}(t_1, \dots, t _{n-1}, \quad A _{k}^{n}(t_1, \dots, t_n)

    Akn(t1,,tn)A _{k}^{n}(t_1, \dots, t_n) 의 괴델수를 xx 라고 하고, 이 식의 열의 괴델수를 yy 라고 하자. 그러면 명백히 6) 에서와 같은 논리로 y<(px!)xy < (p_x!)^{x} 이고 n=ArgP((x)0)n = \operatorname{Arg}_{\text{P}} ((x)_0) 이다. 따라서 Atfml(x)\operatorname{Atfml}(x) 는 다음과 같다.

    (y)y<(px!)x[x=(y)lh(y) ˙1lh(y)=ArgP((x)0)+1PL(((y)0)0)((y)0)1=3lh((y)0)=2(u)u<lh(y) ˙2(v)v<x((y)u+1=(y)uv27Trm(v))(v)v<x((y)lh(y) ˙1=(y)lh(y) ˙2v25Trm(v))] \begin{align}\begin{split} &(\exists y)_{y<(p_x!)^{x}} \Big [x = (y) _{\operatorname{lh}(y) \dotdiv 1} \land \operatorname{lh}(y) = \operatorname{Arg}_{\text{P}} ((x)_0)+1 \land \\ &\enspace \operatorname{PL} (((y)_0)_0) \land ((y)_0)_1 = 3 \land \operatorname{lh}((y)_0) = 2 \land \\ &\enspace (\forall u)_{u < \operatorname{lh}(y)\dotdiv 2}(\exists v)_{v < x}\big ((y)_{u+1} = (y)_{u} * v * 2 ^{7} \land \operatorname{Trm}(v)\big ) \land \\ &\enspace (\exists v)_{v<x} \big ((y)_{\operatorname{lh}(y) \dotdiv 1} = (y)_{\operatorname{lh}(y)\dotdiv 2} * v * 2 ^{5} \land \operatorname{Trm}(v)\big )\Big ] \end{split}\end{align} \tag*{}
  8. Fml(y)\operatorname{Fml}(y): yyKK 의 wff 의 괴델수이다.

    Atfml(y)(z)z<3y[(Fml(z)y=2329z25)(Fml((z)0)Fml((z)1)y=23(z)0211(z)125)(Fml((z)0)EVbl((z)1)y=2323213(z)125(z)025)] \begin{align}\begin{split} &\operatorname{Atfml}(y) \lor \\ & \enspace (\exists z) _{z < 3 ^{y}}[(\operatorname{Fml}(z) \land y = 2 ^{3} * 2 ^{9} * z * 2 ^{5} )\lor \\ & \enspace (\operatorname{Fml}((z)_0) \land \operatorname{Fml}((z)_1) \land y = 2 ^{3} * (z)_0 * 2 ^{11} * (z)_1 * 2 ^{5}) \lor \\ & \enspace (\operatorname{Fml}((z)_0) \land \operatorname{EVbl} ((z)_1) \land \\ & \qquad y = 2 ^{3} * 2 ^{3} * 2 ^{13} * (z)_1 * 2 ^{5} * (z)_0 * 2 ^{5})] \\ \end{split}\end{align} \tag*{}
  9. Subst(x,y,u,v)\operatorname{Subst}(x, y, u, v): xx 는 괴델수 yy 의 식에서 괴델수 vv 를 갖는 모든 자유변수를 괴델수 uu 의 항으로 치환하여 얻은 결과의 괴델수이다.

    Gd(y)Trm(u)EVbl(2v)[(y=2vx=u)(w)w<y(y=2wy2vx=y)(z)z<y(w)w<y(Fml(w)y=232132v25wz(α)α<x(x=232132v25wαSubst(α,z,u,v)))((¬(z)z<y(w)w<y(Fml(w)y=232132v25wz))(α)α<x(β)β<x(z)z<y(1<zy=2(y)0zx=αβSubst(α,2(y)0,u,v)Subst(β,z,u,v)))] \begin{align}\begin{split} &\operatorname{Gd}(y) \land \operatorname{Trm}(u) \land \operatorname{EVbl} (2 ^{v}) \land \Bigg [(y = 2 ^{v} \land x = u) \lor \\ & \enspace (\exists w)_{w<y}(y = 2 ^{w} \land y \neq 2 ^{v} \land x = y) \lor \\ & \enspace (\exists z)_{z<y}(\exists w)_{w<y}(\operatorname{Fml}(w) \land y = 2 ^{3} * 2 ^{13} * 2 ^{v} * 2 ^{5} * w * z \land \\ & \quad (\exists \alpha)_{\alpha<x}(x = 2 ^{3} * 2 ^{13} * 2 ^{v} * 2 ^{5} * w * \alpha \land \\ & \qquad \operatorname{Subst}(\alpha,z,u,v))) \lor \\ & \enspace \bigg ( \Big ( \neg (\exists z)_{z<y}(\exists w)_{w<y}(\operatorname{Fml}(w) \land \\ & \qquad y = 2 ^{3} * 2 ^{13} * 2 ^{v} * 2 ^{5} * w * z ) \Big ) \land \\ & \qquad (\exists \alpha)_{\alpha<x}(\exists \beta)_{\beta<x}(\exists z)_{z<y}\Big (1 < z \land y = 2 ^{(y)_0}*z \\ & \qquad \land x = \alpha*\beta \land \operatorname{Subst}(\alpha, 2 ^{(y)_0}, u, v) \land \operatorname{Subst}(\beta,z,u,v)\Big )\bigg )\Bigg ]\\ \end{split}\end{align} \tag*{}
  10. Sub(y,u,v)\operatorname{Sub}(y, u, v): 괴델수 yy 의 식에서 괴델수 vv 를 갖는 모든 자유변수를 괴델수 uu 의 항으로 치환하여 얻은 결과의 괴델수.

    Sub(y,u,v)=μxx<(puy!)uySubst(x,y,u,v) \operatorname{Sub}(y,u,v) = \mu x _{x < (p _{uy}!) ^{uy}}\operatorname{Subst}(x,y,u,v)

    (u,v,yu,v,y 에 대한 조건이 성립하지 않을 때 Sub(y,u,v)\operatorname{Sub}(y, u, v) 가 정의는 되지만 그 값은 의미없다.)

  11. Fr(y,v)\operatorname{Fr}(y, v): yy 는 괴델수 vv 의 자유변수를 포함하는 KK 의 wff 나 항의 괴델수이다.

    (Fml(y)Trm(y))EVbl(2v)¬Subst(y,y,213+8v,v) (\operatorname{Fml}(y) \lor \operatorname{Trm}(y)) \land \operatorname{EVbl} (2 ^{v}) \land \neg \operatorname{Subst}(y, y, 2 ^{13+8v}, v)

    (즉, 괴델수 vv 의 자유변수를 어떤 다른 변수로 치환하면 yyyy 가 아니게 된다는 것이다. 이로써 yy 가 반드시 괴델수 vv 의 자유변수를 포함해야 한다는 것을 주장할 수 있다.)

  12. Ff(u,v,w)\operatorname{Ff}(u, v, w): uu 는 괴델수 ww 의 wff 에서 괴델수 vv 의 변수에 대하여 자유인 항의 괴델수이다.

    Trm(u)EVbl(2v)Fml(w)[Atfml(w)(y)y<w(w=2329y25Ff(u,v,y))(y)y<w(z)z<w(w=23y211z25Ff(u,v,y)Ff(u,v,z))(y)y<w(z)z<w(w=23232132z25y25EVbl(2z)(zvFf(u,v,y)(Fr(u,z)¬Fr(y,v))))] \begin{align}\begin{split} &\operatorname{Trm}(u) \land \operatorname{EVbl} (2 ^{v}) \land \operatorname{Fml}(w) \land \Bigg [\operatorname{Atfml}(w) \\ & \enspace \land (\exists y)_{y<w}\big (w = 2 ^{3} * 2 ^{9} * y * 2 ^{5} \land \operatorname{Ff}(u, v, y)\big ) \\ & \enspace \lor (\exists y)_{y<w}(\exists z)_{z < w}\big (w = 2 ^{3} * y * 2 ^{11} * z * 2 ^{5} \\ & \qquad \land \operatorname{Ff}(u, v, y) \land \operatorname{Ff}(u, v, z)\big ) \lor \\ & \enspace (\exists y)_{y<w} (\exists z)_{z < w}\big ( w = 2 ^{3} * 2 ^{3} * 2 ^{13} * 2 ^{z} * 2 ^{5} * y * 2 ^{5} \\ & \qquad \land \operatorname{EVbl} (2 ^{z}) \land (z \neq v \implies \operatorname{Ff}(u, v, y) \\ & \qquad \land (\operatorname{Fr}(u, z) \implies \neg \operatorname{Fr}(y, v)))\big )\Bigg ] \\ \end{split}\end{align} \tag*{}
  13. 1차 이론의 공리에 대하여 다음과 같이 정의한다.

    1. A x1\operatorname{Ax_1}: xx 는 공리꼴 (A1)(A1) 의 인스턴스의 괴델수이다.

      (u)u<x(v)v<x(Fml(u)Fml(v)x=23u21123v211u2525) \begin{align}\begin{split} &(\exists u)_{u<x}(\exists v)_{v<x}(\operatorname{Fml}(u) \land \operatorname{Fml}(v) \\ & \enspace \land x = 2 ^{3} * u * 2 ^{11} * 2 ^{3} * v * 2 ^{11} * u * 2 ^{5} * 2 ^{5}) \\ \end{split}\end{align} \tag*{}
    2. A x2\operatorname{Ax_2}: xx 는 공리꼴 (A2)(A2) 의 인스턴스의 괴델수이다.

      (u)u<x(v)v<x(w)w<x(Fml(u)Fml(v)Fml(w)x=2323u21123v211w25252112323u211v2521123u211w252525) \begin{align}\begin{split} &(\exists u)_{u<x}(\exists v)_{v<x}(\exists w)_{w<x}(\operatorname{Fml}(u) \land \operatorname{Fml}(v)\land \operatorname{Fml}(w) \\ & \enspace \land x = 2 ^{3} * 2 ^{3} * u * 2 ^{11} * 2 ^{3} * v * 2 ^{11} * w * 2 ^{5} * 2 ^{5} \\ & \qquad * 2 ^{11} * 2 ^{3} * 2 ^{3} * u * 2 ^{11} * v * 2 ^{5} * 2 ^{11} * 2 ^{3} * u * 2 ^{11} \\ & \qquad * w * 2 ^{5} * 2 ^{5} * 2 ^{5}) \\ \end{split}\end{align} \tag*{}
    3. A x3\operatorname{Ax_3}: xx 는 공리꼴 (A3)(A3) 의 인스턴스의 괴델수이다.

      (u)u<x(v)v<x(Fml(u)Fml(v)x=23232329v252112329u252521123232329v25211u25211v2525) \begin{align}\begin{split} &(\exists u)_{u<x}(\exists v)_{v<x}(\operatorname{Fml}(u) \land \operatorname{Fml}(v) \\ & \enspace \land x = 2 ^{3} * 2 ^{3} * 2 ^{3} * 2 ^{9} * v * 2 ^{5} * 2 ^{11} * 2 ^{3} * 2 ^{9} * u * 2 ^{5} \\ & \qquad * 2^{5} * 2 ^{11} * 2 ^{3} * 2 ^{3} * 2 ^{3} * 2 ^{9} * v * 2 ^{5} * 2 ^{11} * u * 2 ^{5} \\ & \qquad * 2 ^{11}* v * 2 ^{5} * 2 ^{5}) \\ \end{split}\end{align} \tag*{}
    4. A x4\operatorname{Ax_4}: xx 는 공리꼴 (A4)(A4) 의 인스턴스의 괴델수이다.

      (u)u<x(v)v<x(y)y<x(Fml(y)Trm(u)EVbl(2v)Ff(u,v,y)x=2323232132v25y211Sub(y,u,v)25) \begin{align}\begin{split} &(\exists u)_{u<x}(\exists v)_{v<x}(\exists y)_{y<x}(\operatorname{Fml}(y) \land \operatorname{Trm}(u) \land \operatorname{EVbl} (2 ^{v}) \\ & \qquad \land \operatorname{Ff}(u, v, y) \land x = 2 ^{3} * 2 ^{3} * 2 ^{3} * 2 ^{13} * 2 ^{v} * 2 ^{5} * y \\ & \qquad \qquad * 2 ^{11} * \operatorname{Sub}(y, u, v) * 2 ^{5} )\\ \end{split}\end{align} \tag*{}
    5. A x5\operatorname{Ax_5}: xx 는 공리꼴 (A5)(A5) 의 인스턴스의 괴델수이다.

      (u)u<x(v)v<x(w)w<x(Fml(u)Fml(w)EVbl(2v)¬Fr(u,v)x=2323232132v2523u211w252521123u21123232132v25w252525) \begin{align}\begin{split} &(\exists u)_{u<x}(\exists v)_{v<x}(\exists w)_{w<x}(\operatorname{Fml}(u)\land \operatorname{Fml}(w)\land \operatorname{EVbl} (2 ^{v}) \\ & \enspace \land\neg \operatorname{Fr}(u, v) \land x = 2 ^{3} * 2 ^{3} * 2 ^{3} * 2 ^{13} * 2 ^{v} * 2 ^{5} * 2 ^{3} * u \\ & \qquad * 2 ^{11} * w * 2 ^{5} * 2 ^{5} 2 ^{11} * 2 ^{3} * u * 2 ^{11} * 2 ^{3} * 2 ^{3} * 2 ^{13} \\ & \qquad * 2 ^{v} * 2 ^{5} * w * 2 ^{5} * 2 ^{5} * 2 ^{5})\\ \end{split}\end{align} \tag*{}
    6. LAX(y)\operatorname{LAX}(y): yyKK 의 논리적 공리의 괴델수이다.

      A x1(y) A x2(y) A x3(y) A x4(y) A x5(y) \operatorname{Ax_1}(y)\lor \operatorname{Ax_2}(y)\lor \operatorname{Ax_3}(y)\lor \operatorname{Ax_4}(y) \lor \operatorname{Ax_5}(y)
  14. Neg(x)\operatorname{Neg}(x): xxBB 의 괴델수일 때 (¬B)(\neg B) 의 괴델수이다.

    Neg(x)=2329x25 \operatorname{Neg}(x) = 2 ^{3} * 2 ^{9} * x * 2 ^{5}
  15. Cond(x,y)\operatorname{Cond}(x, y): xxBB 의 괴델수이고 yyCC 의 괴델수일 때 (BC)(B \implies C) 의 괴델수이다.

    Cond(x,y)=23x211y25 \operatorname{Cond}(x, y) = 2 ^{3} * x * 2 ^{11} * y * 2 ^{5}
  16. Clos(u)\operatorname{Clos}(u): uu 가 wff BB 의 괴델수일 때 BB 의 폐포의 괴델수이다.

    V(u)=μvvu(EVbl(2v)Fr(u,v))V(u) = \mu v _{v \leq u}(\operatorname{EVbl} (2 ^{v}) \land \operatorname{Fr}(u, v)) 이라고 하자. V(u)V(u)uu 에 존재하는 자유변수의 최소 괴델수이다. VV 는 원시 재귀(또는 재귀)이다.

    Sent(u)\operatorname{Sent}(u)Fml(u)¬(v)vuFr(u,v)\operatorname{Fml}(u) \land \neg (\exists v)_{v \leq u}\operatorname{Fr}(u, v) 라고 하자. Sent(u)\operatorname{Sent}(u)uu 가 문장(닫힌 wff)의 괴델수일 때에만 성립한다. Sent\operatorname{Sent} 는 원시 재귀(또는 재귀)이다.

    다음과 같이 정의하면, GG 는 원시 재귀(또는 재귀)이다.

    G(u)={2323213Fml(u)¬Sent(u)2V(u)25u25uelse G(u) = \begin{cases} 2 ^{3} * 2 ^{3} * 2 ^{13} & \operatorname{Fml}(u) \land \neg \operatorname{Sent}(u)\\ \enspace * 2 ^{V(u)} * 2 ^{5} * u * 2 ^{5} \\ u & \text{else} \\ \end{cases}

    uu 가 닫혀있지 않은 wff BB 의 괴델수면 G(u)G(u)BB 에서 최소 괴델수인 자유변수 xx 에 대한 (x)B(\forall x)B 의 괴델수가 된다. 그렇지 않은 경우 G(u)=uG(u) = u 이다.

    다음과 같이 정의하면 HH 는 원시 재귀(또는 재귀)이다.

    H(u,0)=G(u) H(u, 0) = G(u)
    H(u,y+1)=G(H(u,y)) H(u, y+1) = G(H(u, y))

    이제 Clos\operatorname{Clos} 를 다음과 같이 정의한다.

    Clos(u)=H(u,μyyu(H(u,y)=H(u,y+1))) \operatorname{Clos}(u) = H(u, \mu y _{y \leq u}(H(u, y) = H(u, y+1)))
  • 이 정리는 원시 재귀[재귀] 어휘를 갖는 이론에서 산술에 대하여 언급하는 명제들이 어떻게 산술화되는지 보여준다.

    8) 은 정형 논리식(wff)의 정의가 산술화된 것이다.

    명제는 언어적으로 문장이지만, 사람이 마음 속 생각이나 아이디어나 발상이나 깨달음 등을 언어로 변환한 것으로 볼 수 있다. 생각이 문장이 되고 문장이 산술화되며 산술 명제들이 기계화되어 자동화 가능하다면, 역으로 기계적 요소를 산술화하고 산술 명제를 자연어로 다시 역변환하고 자연어를 전기신호로 변환하여 뇌로 입력시킬 수도 있다.

  • 증명

Diagonal Function

정리 3.27, 대각함수(diagonal function)

KK 가 원시 재귀(또는 재귀) 어휘를 갖는 이론이고, 개별 상수 00 과 함수 기호 f11f _{1}^{1} 을 포함하는 언어 LA\mathcal{L}_A 를 갖는다고 하자. (그러면 모든 숫자가 KK 의 항이 되고, KKSS 자체가 될 수 있다.) 그러면 다음 함수와 관계는 원시 재귀(또는 재귀)이다.

  1. Num(y)\operatorname{Num}(y): 식 y\overline{y} 의 괴델수.

    Num(0)=215 \operatorname{Num}(0) = 2 ^{15}
    Num(y+1)=24923Num(y)25 \operatorname{Num}(y + 1) = 2 ^{49} * 2 ^{3} * \operatorname{Num}(y) * 2 ^{5}

    (2152 ^{15}27+812 ^{7 + 8 \cdot 1} 로써 첫번째 상수 00 을 뜻하고, 2492 ^{49}21+8(2131)2 ^{1 + 8(2 ^{1}3 ^{1})} 로써 첫번째 함수 f11f _{1}^{1} 를 뜻한다.

  2. Nu(x)\operatorname{Nu}(x): xx 는 숫자의 괴델수이다.

    (y)y<x(x=Num(y)) (\exists y)_{y<x}(x = \operatorname{Num}(y))
  3. D(u)D(u): uu 가 wff B(x1)B(x_1) 의 괴델수일 때 B(u)B(\overline{u}) 의 괴델수.

    D(u)=Sub(u,Num(u),21) D(u) = \operatorname{Sub}(u, \operatorname{Num}(u), 21)

    (212113+8113 + 8 \cdot 1 로써 x1x_1 을 뜻한다.) DD 를 대각 함수라고 한다.

  • 이로써 이 함수와 관계들도 괴델수에 의하여 순수한 자연수로 환원가능하다.

  • 증명

Primitive Recursive Axiom Set

원시 재귀[재귀] 공리 집합(primitive recursive[recursive] axiom set)

이론 KK 가 원시 재귀[재귀] 공리 집합이라는 것은 다음 성질 PrAx\operatorname{PrAx} 가 원시 재귀[재귀]라는 것이다.

  • PrAx(y)\operatorname{PrAx}(y): yyKK 의 고유 공리의 괴델수이다.

    가령, 다음 정리에서처럼 SS 에서 PrAx(y)\operatorname{PrAx}(y) 는 다음과 동치이다.

    y=a1y=a2y=a8A9(y) y = a_1 \lor y = a_2 \lor \dots \lor y = a_8 \lor A_9(y)
  • PrAx\operatorname{PrAx}SS 에서 괴델수에 의하여 산술화된다.

SS 는 원시 재귀 공리 집합이다.

  • 증명

    공리 (S1)(S8)(S1) - (S8) 의 괴델수를 각각 a1,,a8a_1, \dots, a_8 이라고 하자. 수 yy 가 공리꼴 (S9)(S9) 의 인스턴스의 괴델수임을 보이는 것과 다음은 동치이다.

    (v)v<y(w)w<y(EVbl(2v)Fml(w)y=23Sub(w,215,v)2112323232132v2523w211Sub(w,249232v25,v)252521123232132v25w2525) \begin{align}\begin{split} &(\exists v)_{v<y}(\exists w)_{w<y}(\operatorname{EVbl} (2 ^{v}) \land \operatorname{Fml}(w) \\ & \enspace \land y = 2 ^{3} * \operatorname{Sub}(w, 2 ^{15}, v) * 2 ^{11} * 2 ^{3} * 2 ^{3} * 2 ^{3} * 2 ^{13} * 2 ^{v} * 2 ^{5} \\ & \qquad * 2 ^{3} * w * 2 ^{11} * \operatorname{Sub}(w, 2 ^{49} * 2 ^{3} * 2 ^{v} * 2 ^{5} , v) * 2 ^{5} * 2 ^{5} * 2 ^{11}\\ & \qquad * 2 ^{3} * 2 ^{3} * 2 ^{13} * 2 ^{v} * 2 ^{5} * w * 2 ^{5} * 2 ^{5} )\\ \end{split}\end{align} \tag*{}

    이 식을 A9(y)A_9(y) 라고 하자. 그러면 yySS 의 고유 공리의 괴델수인 것은 다음과 동치이다.

    y=a1y=a2y=a8A9(y) y = a_1 \lor y = a_2 \lor \dots \lor y = a_8 \lor A_9(y)

    그러면 PrAx(y)\operatorname{PrAx}(y)SS 에서 원시 재귀이다. ■

정리 3.28 원시 재귀[재귀] 공리 집합 이론에서 원시 재귀[재귀]가 되는 관계

이론 KK 가 원시 재귀(또는 재귀) 어휘와 원시 재귀(또는 재귀) 공리 집합을 가졌다고 하자. 그러면 다음 관계는 원시 재귀(또는 재귀)이다.

  1. Ax(y)\operatorname{Ax}(y): yyKK 의 공리의 괴델수이다.

    LAX(y)PrAx(y) \operatorname{LAX}(y) \lor \operatorname{PrAx}(y)
  2. Prf(y)\operatorname{Prf}(y): yyKK 의 증명의 괴델수이다.

    (u)u<y(v)v<y(z)z<y(w)w<y([y=2wAx(w)][Prf(u)Fml((u)w)y=u2vGen((u)w,v)][Prf(u)Fml((u)z)Fml((u)w)y=u2vMP((u)z,(u)w,v)][Prf(u)y=u2vAx(v)]) \begin{align}\begin{split} &(\exists u)_{u<y}(\exists v)_{v<y}(\exists z)_{z<y}(\exists w)_{w<y}\bigg (\Big [y = 2 ^{w} \land \operatorname{Ax}(w)\Big ] \lor \\ & \enspace \Big [\operatorname{Prf}(u) \land \operatorname{Fml}((u)_w) \land y = u * 2 ^{v} \land \operatorname{Gen}((u)_w, v)\Big ] \lor \\ & \enspace \Big [\operatorname{Prf}(u) \land \operatorname{Fml}((u)_z) \land \operatorname{Fml}((u)_w) \land \\ &\qquad y = u * 2 ^{v} \land \operatorname{MP}((u)_z, (u)_w, v)\Big ]\lor \\ & \enspace \Big [\operatorname{Prf}(u) \land y = u * 2 ^{v} \land \operatorname{Ax}(v)\Big ]\bigg )\\ \end{split}\end{align} \tag*{}
  3. Pf(y,x)\operatorname{Pf}(y, x): yy 는 괴델수 xx 의 wff 의 KK 에서의 증명의 괴델수이다.

    Prf(y)x=(y)lh(y) ˙1 \operatorname{Prf}(y) \land x = (y) _{\operatorname{lh}(y) \dotdiv 1}
  • 원시 재귀 공리 집합 이론에서는 이렇게 공리, 증명도 산술화된다. 이렇게 고차원적인 개념으로 보이는 공리와 증명 같은 개념들을 산술 체계로 끌어내릴 수 있다.

    그런데 증명가능성을 주장하는 이 명제의 산술화가 오히려 체계의 완전성을 붕괴시키는 주범이 되었다. 이 원리를 불완전성 정리에서 자세히 알아본다.

  • 증명

Representable is Recursive in S

정리 3.29

KK 가 동등성을 지닌 이론이고, KK 의 언어가 개별 상수 00 과 함수 기호 f11f _{1}^{1} 가지며, KK 가 원시 재귀(또는 재귀) 어휘와 공리 집합을 갖는다고 하자. 또한, 다음이 성립한다고 하자.

  1. 임의의 자연수 r,sr, s 에 대하여 Kr=s\vdash _K \overline{r} = \overline{s} 이면 r=sr = s 이다.

그러면 KK 에서 표현가능한 임의의 함수 f(x1,,xn)f(x_1, \dots, x_n) 가 재귀이다.

  • 이 정리가 성립하는 이론에서는 표현가능한, 즉 이론 안에서 표현되는 모든 함수가 재귀이다.

  • 증명

    임의의 함수 f(x1,,xn)f(x_1, \dots, x_n) 를 wff B(x1,,xn,xn+1)B(x_1, \dots, x_n, x _{n+1}) 가 표현한다고 하자. PB(u1,,un,un+1,y)P_B(u_1, \dots, u_n, u _{n+1}, y)yyKK 에서의 wff B(u1,,un,un+1)B(\overline{u}_1, \dots , \overline{u}_n, \overline{u}_{n+1}) 의 증명의 괴델수를 뜻한다고 하자. 이때, PB(u1,,un,un+1,y)P_B(u_1, \dots, u_n, u _{n+1}, y) 이면 f(u1,,un)=un+1f(u_1, \dots, u_n) = u _{n+1} 이다.

    f(u1,,un)=rf(u_1, \dots, u_n) = r 로 두자. BBKK 에서 ff 를 표현하므로 KB(u1,,un,r)\vdash _KB(\overline{u}_1, \dots , \overline{u}_n, \overline{r}) 이고 K(1y)B(u1,,un,y)\vdash _K(\exists _1y)B(\overline{u}_1, \dots , \overline{u}_n, y) 이다. 가정에 의하여 PB(u1,,un,un+1,y)P_B(u_1, \dots, u_n,u _{n+1}, y) 이므로 KB(u1,,un,un+1)\vdash _KB(\overline{u}_1, \dots , \overline{u}_n, \overline{u}_{n+1}) 이다. KK 가 동등성을 가진 이론이므로 Kr=un+1\vdash _K \overline{r} = \overline{u}_{n+1} 이다. 1) 에 의하여 r=un+1r = u _{n+1} 이다.

    mmB(x1,,xn,xn+1)B(x_1, \dots, x_n, x _{n+1}) 의 괴델수라고 하자. 그러면 PB(u1,,un,un+1,y)P_B(u_1, \dots, u_n,u _{n+1}, y) 는 다음과 같다. (212113+8113 + 8 \cdot 1 으로써 x1x_1 을 뜻한다.)

    Pf(y,Sub(Sub(Sub(m,Num(u1),21),Num(u2),29)Num(un+1),21+8n)) \operatorname{Pf}(y, \operatorname{Sub}(\dots \operatorname{Sub}(\operatorname{Sub}(m, \operatorname{Num}(u_1), 21), \operatorname{Num}(u_2), 29) \\ \dots \operatorname{Num}(u _{n+1}), 21 + 8n))

    정리 3.26, 3.27, 3.28 에 의하여 PB(u1,,un,un+1,y)P_B(u_1, \dots, u_n, u _{n+1}, y) 는 원시 재귀(또는 재귀)이다.

    임의의 자연수 k1,,knk_1, \dots, k_n 에 대하여 f(k1,,kn)=rf(k_1, \dots, k_n) = r 라고 하자. 그러면 KB(k1,,kn,r)\vdash _KB(\overline{k}_1, \dots , \overline{k}_n, \overline{r}) 이다. KK 에서의 B(k1,,kn,r)B(\overline{k}_1, \dots , \overline{k}_n, \overline{r}) 의 증명의 괴델수를 jj 라고 하자. 그러면 PB(k1,,kn,r,j)P_B(k_1, \dots, k_n,r,j) 이다. 그러므로 임의의 x1,,xnx_1, \dots, x_n 에 대하여 PB(x1,,xn,(y)0,(y)1)P_B(x_1, \dots, x_n, (y)_0, (y)_1)yy 가 존재한다.

    그러면 문제 3.16 3) 에 의하여 μy(PB(x1,,xn,(y)0,(y)1))\mu y(P_B(x_1, \dots, x_n, (y)_0, (y)_1)) 는 재귀이다. 그렇다면 f(x1,,xn)=(μy(PB(x1,,xn,(y)0,(y)1)))0f(x_1, \dots, x_n) = (\mu y(P_B(x_1, \dots, x_n, (y)_0, (y)_1)))_0 이고, 그러므로 ff 는 재귀이다. ■

문제 3.36

술어 기호 ==, 개별 상수 00, 함수 기호 f11f _{1}^{1} 를 포함하는 언어를 갖는 이론 KK 에 대하여 다음이 성립한다.

  1. KK 가 정리 3.29 의 조건 1) 을 만족하면 KK 는 무모순이다.
  2. KK 가 모순이면 모든 수론적 함수는 KK 에서 표현가능하다.
  3. KK 가 무모순이고 동일 관계 x=yx=yKK 에서 표현가능하면 KK 는 정리 3.29 의 조건 1) 을 만족한다.
  • 증명

Recursive is identical with Representable in S

따름정리 3.30

SS 의 무모순성을 가정하면, 재귀 함수의 모임은 SS 에서 표현가능한 함수의 모임과 동일하다.

  • 즉, SS 에서 재귀 함수라면 표현가능하고, 표현가능하면 재귀 함수이다. (챕터 5 에서 재귀 함수의 개념이 효과적으로 계산가능한 함수와 같다는 것을 알아본다.)

  • 증명

    SS 는 원시 재귀 어휘와 공리 집합을 갖는다. 문제 3.36(3) 과 항등 관계가 SS 에서 표현가능하다는 사실에 의하여 정리 3.29 는 SS 에서 표현가능한 모든 함수가 재귀라는 결론을 내려준다. 반면, 정리 3.24 는 모든 재귀 함수가 SS 에서 표현가능하다는 것을 말해준다. ■

따름정리 3.31

수론적 관계 R(x1,,xn)R(x_1, \dots, x_n) 가 재귀인 것은 그것이 SS 에서 표현가능하다는 것과 동치이다.

  • 즉, SS 에서 관계가 재귀이면 표현가능하고, 표현가능하면 재귀이다.

  • 이후에 표현가능한 함수와 재귀 함수가 동등하다는 조건에 대하여 SS 보다 더 약한 조건을 찾아볼 것이다.

  • 증명

    정의에 의하여 RR 이 재귀인 것과 CRC_R 이 재귀인 것은 동치이다. 따름정리 3.30 에 의하여 CRC_R 이 재귀인 것과 CRC_RSS 에서 표현가능한 것은 동치이다. 정리 3.13 에 의하여 CRC_RSS 에서 표현가능한 것과 RRSS 에서 표현가능한 것은 동치이다. ■

Robinson's System

로빈슨 체계(Robinson's System)

언어 LA\mathcal{L}_A 에서 다음의 유한한 고유공리로 갖는 이론을 RRRR 이라고 한다.

  1. x1=x1x_1 = x_1
  2. x1=x2x2=x1x_1 = x_2 \implies x_2 = x_1
  3. x1=x2(x2=x3x1=x3)x_1 = x_2 \implies (x_2 = x_3 \implies x_1 = x_3)
  4. x1=x2x1=x2x_1 = x_2 \implies x'_1 = x'_2
  5. x1=x2(x1+x3=x2+x3x3+x1=x3+x2)x_1 = x_2 \implies (x_1 + x_3 = x_2 + x_3 \land x_3 + x_1 = x_3 + x_2)
  6. x1=x2(x1x3=x2x3x3x1=x3x2)x_1 = x_2 \implies (x_1 \cdot x_3 = x_2 \cdot x_3 \land x_3 \cdot x_1 = x_3 \cdot x_2)
  7. x1=x2x1=x2x'_1 = x'_2 \implies x_1 = x_2
  8. 0x10 \neq x'_1
  9. x10(x2)(x1=x2)x_1 \neq 0 \implies (\exists x_2)(x_1 = x'_2)
  10. x1+0=x1x_1 + 0 = x_1
  11. x1+x2=(x1+x2)x_1 + x'_2 = (x_1 + x_2)'
  12. x10=0x_1 \cdot 0 = 0
  13. x1x2=(x1x2)+x1x_1 \cdot x'_2 = (x_1 \cdot x_2) + x_1
  14. (uniqueness of remainder) (x2=x1x3+x4x4<x1x2=x1x5+x6x6<x1)x4=x6(x_2 = x_1 \cdot x_3 + x_4 \land x_4 < x_1 \land x_2 = x_1 \cdot x_5 + x_6 \land x_6 < x_1) \\ \implies x_4 = x_6
  • RRRR 의 모든 공리는 SS 의 정리이므로 RRRRSS 의 부분이론이다.

  • RRRR 의 고유공리는 유한하다.

보조정리 3.32

RRRR 에서 임의의 자연수 n,mn, m 에 대하여 다음은 정리이다.

  1. n+m=n+m\overline{n}+\overline{m}= \overline{n+m}
  2. nm=nm\overline{n} \cdot \overline{m} = \overline{n \cdot m}
  3. nmn \neq m 일 때 nm\overline{n}\neq \overline{m}
  4. n<mn<m 일 때 n<m\overline{n}<\overline{m}
  5. x0x \not < 0
  6. xnx=0x=1x=nx \leq \overline{n} \implies x = 0 \lor x = \overline{1} \lor \dots \lor x = \overline{n}
  7. xnnxx \leq \overline{n} \lor \overline{n} \leq x
  • 증명

Recursive is the same as Representable in RR

정리 3.33

모든 재귀 함수는 RRRR 에서 표현가능하다.

  • 본 정리에 의하여 모든 재귀 함수는 RRRR 의 임의의 확장에서 표현가능하다. 정리 3.29 와 문제 3.36 3) 에 의하여 언어 LA\mathcal{L}_A 위에서 재귀 공리 집합을 갖는 RRRR 의 임의의 무모순인 확장에서 표현가능한 함수의 모임은 재귀 함수의 모임과 같다.

    또한, 정리 3.13 에 의하여 이러한 이론에서 표현가능한 관계는 곧 재귀 관계이다.

  • 증명

Godel's Incompleteness Theorem

식의 이름(name)

이론의 식 CC 의 괴델수가 qq 이면 숫자 q\overline{q} C \ulcorner C \urcorner 라고 쓰고, 언어 LA\mathcal{L}_A 에서의 CC 의 이름이라고 부르자.

Fixed-Point Theorem

정리 3.34 대각화 보조정리(Diagonalization Lemma)

언어 LA\mathcal{L}_A 안에서 동등성을 가진 이론에서 대각 함수 DD 가 표현가능하면, x1x_1 이 유일한 자유변수인 임의의 wff E(x1)E(x_1) 에 대하여 다음을 만족하는 닫힌 wff CC 가 존재한다.

KCE( C ) \vdash _K C \iff E(\ulcorner C\urcorner)
  • 증명

    wff D(x1,x2)D(x_1, x_2) 가 대각함수 DDKK 에서 표현한다고 하자. 다음과 같은 wff 를 정의하자.

    (x2)(D(x1,x2)E(x2))(1) (\forall x_2)(D(x_1, x_2) \implies E(x_2)) \tag{1}

    (1)(1) 의 괴델수를 mm 이라고 하자. (1)(1) 에서 x1x_1m\overline{m} 으로 치환하자.

    (x2)(D(m,x2)E(x2))(C) (\forall x_2)(D(\overline{m}, x_2) \implies E(x_2)) \tag{C}

    wff CC 의 괴델수를 qq 라고 하자. 즉, q\overline{q} C \ulcorner C\urcorner 이다.

    이때 대각함수의 정의에 의하여 D(m)=qD(m) = q 가 성립한다. wff DD 가 대각함수 DDKK 에서 표현하므로 다음이 성립한다.

    KD(m,q)(2) \vdash _KD(\overline{m}, \overline{q}) \tag{2}

    KCE(q)\vdash _KC \implies E(\overline{q}) 를 증명하자.

    연역 근거
    1 CC Hyp
    2 (x2)(D(m,x2)E(x2))(\forall x_2)(D(\overline{m}, x_2) \implies E(x_2)) 1 의 정의
    3 D(m,q)E(q)D(\overline{m}, \overline{q}) \implies E(\overline{q}) 2, rule A4
    4 D(m,q)D(\overline{m}, \overline{q}) (2)(2)
    5 E(q)E(\overline{q}) 3, 4, MP
    6 CKE(q)C \vdash _K E(\overline{q}) 1-5
    7 KCE(q)\vdash _K C \implies E(\overline{q}) 1-6, 따름정리 2.6

    KE(q)C\vdash _K E(\overline{q}) \implies C 를 증명하자.

    연역 근거
    1 E(q)E(\overline{q}) Hyp
    2 D(m,x2)D(\overline{m}, x_2) Hyp
    3 (1x2)D(m,x2)(\exists _1 x_2) D(\overline{m}, x_2) wff DD 가 대각함수 DD 를 표현한다
    4 D(m,q)D(\overline{m}, \overline{q}) (2)(2)
    5 x2=qx_2 = \overline{q} 2-4, == 의 성질
    6 E(x2)E(x_2) 1,5, == 의 치환성
    7 E(q),D(m,x2)KE(x2)E(\overline{q}), D(\overline{m}, x_2) \vdash _KE(x_2) 1-6
    8 E(q)KD(m,x2)E(x2)E(\overline{q}) \vdash _K D(\overline{m}, x_2) \implies E(x_2) 1-7, 따름정리 2.6
    9 E(q)K(x2)(D(m,x2)E(x2))E(\overline{q}) \vdash _K (\forall x_2)( D(\overline{m}, x_2) \implies E(x_2)) 8, Gen
    10 KE(q)(x2)(D(m,x2)E(x2))\vdash _K E(\overline{q}) \implies (\forall x_2)( D(\overline{m}, x_2) \implies E(x_2)) 1-9, 따름정리 2.6
    11 KE(q)C\vdash _K E(\overline{q}) \implies C 10

    그러므로 biconditional introduction에 의하여 KCE(q)\vdash _KC \iff E(\overline{q}) 이다. ■

정리 3.35 고정점 정리(Fixed-Point Theorem)

언어 LA\mathcal{L}_A 안에서 동등성을 가진 이론 KK 에서 모든 재귀 함수가 표현가능하다고 하자. 그러면 x1x_1 이 유일한 자유변수인 임의의 wff E(x1)E(x_1) 에 대하여 다음을 만족하는 닫힌 wff CC 가 존재한다.

KCE( C ) \vdash _K C \iff E(\ulcorner C\urcorner)
  • 정리 3.33 에 의하여 고정점 정리는 KKRRRR 이거나 RRRR 의 임의의 확장일 때 성립한다.

    특히, 고정점 정리는 SS 에서 성립한다.

  • 증명

    정리 3.27 에 의하여 대각함수 DD 는 재귀이다. 그러므로 DDKK 에서 표현가능하다. 그렇다면 정리 3.34 가 적용된다. ■

ω-consistency

ω\omega-무모순성(ω\omega-consistency)

개별 상수 00 과 함수 기호 f11f _{1}^{1} 를 포함하는 언어를 갖는 임의의 이론 KKω\omega-무모순하다는 것은 오직 xx 를 자유변수로 갖는 KK 의 모든 wff B(x)B(x) 에 대하여, 모든 자연수 nn 에 대해 K¬B(n)\vdash _K \neg B(\overline{n}) 이면 K(x)B(x)\vdash _K(\exists x)B(x) 가 아니라는 것이다.

참된 이론(true theory)

언어 LA\mathcal{L}_A 의 임의의 이론 KK 가 참된 이론이라는 것은 KK 의 모든 고유 공리가 표준 모델에서 참이라는 것이다.

  • 모든 논리적 공리가 모든 모델에서 참이고, MP 와 Gen 은 어떤 모델에서 참인 wff 를 그 모델에서 참인 wff 로 이끌어주기 때문에, 참된 이론의 모든 정리는 표준 모델에서 참이다.

  • 모든 참된 이론 KK 는 반드시 ω\omega-무모순이다. 즉, 모든 자연수 nn 에 대하여 K¬B(n)\vdash _K \neg B(\overline{n}) 이면 모든 자연수에 대하여 B(x)B(x) 가 거짓이고, 그러므로 표준모델에서 (x)B(x)(\exists x)B(x) 는 참이 될 수 없다. 그러므로 (x)B(x)(\exists x)B(x)KK 의 정리가 아니다.

    특히, RRRRSSω\omega-무모순이다.

정리 3.36

KKω\omega-무모순이면 KK 는 무모순이다.

  • 그러나 이후의 연구로 본 정리의 역은 성립하지 않는다는 것이 밝혀진다.

  • 증명

    E(x)E(x) 를 오직 xx 를 자유변수로 갖는 임의의 wff 라고 하자. B(x)B(x)E(x)¬E(x)E(x) \land \neg E(x) 라고 하자. 그러면 ¬B(n)\neg B(\overline{n}) 은 항진식의 인스턴스이다. 그러므로 임의의 자연수 nn 에 대하여 K¬B(n)\vdash _K \neg B(\overline{n}) 이다. 그렇다면 ω\omega-무모순성에 의하여 K(x)B(x)\vdash _K(\exists x)B(x) 가 아니다. 그러므로 KK 는 무모순이다.

    (항진식 ¬A(AB)\neg A \implies (A \implies B) 에 의하여 모순적인 이론에서는 모든 wff 가 증명가능하다. 그러므로 단 하나의 wff 라도 증명불가능하면 이론이 반드시 무모순이라는 사실을 1차 논리에서 여러번 공부하였다.) ■

Godel's Incompleteness Theorem

결정불가능한 문장(undecidable sentence)

이론 KK 의 결정불가능한 문장은 BB¬B\neg B 가 모두 KK 의 정리가 아닌, 즉, KB\vdash _KB 도 아니고 K¬B\vdash _K \neg B 도 아닌 닫힌 wff BB 이다.

  • 결정불가능한 문장은 증명될 수 없고, 반증될 수도 없다.

    체계에 결정불가능한 문장이 존재하면 우리는 진실을 알기 위하여 체계의 증명에만 의지할 수 없고, 그러므로 타인에게나 자기 자신에게나 진실을 말하도록 하기 위하여 사실을 체계 내에서 증명하라고 강요할 수도 없다. 불완전성 정리는 체계의 복잡도가 조금만 증가해도 결정불가능한 문장이 형성된다는 것을 말해준다.

    완전성 정리가 증명되었을 때 수학자들은 1차 논리에 산술의 고유공리를 추가해도 완전성이 보존될 것이라고 낙관했다. 그러나 괴델은 1차 논리에 공리를 추가하여 산술을 만들면 완전성은 붕괴되고 불완전성이 내재하게 된다는 것을 보였다.

정리 3.37 괴델의 불완전성 정리(Godel's Incompleteness Theorem), 괴델 문장(Godel sentence)

언어 LA\mathcal{L}_A 에서 동등성을 지닌 이론 KK 에 대하여 다음 조건을 두자.

  1. KK 는 재귀 공리 집합을 갖는다. (즉, PrAx(y)\operatorname{PrAx}(y) 가 재귀이다.)
  2. K01\vdash _K 0 \neq \overline{1}
  3. 모든 재귀 함수가 KK 에서 표현가능하다.

정리 3.28 에 의하여 Pf\operatorname{Pf} 는 재귀이다. 그러므로 Pf\operatorname{Pf}KK 에서 wff PF(x2,x1)PF(x_2, x_1) 에 의하여 표현가능하다. E(x1)E(x_1) 을 wff (x2)¬PF(x2,x1)(\forall x_2) \neg PF(x_2, x_1) 라고 하자. 고정점 정리에 의하여 다음을 만족하는 닫힌 wff GG 가 반드시 존재한다. GGKK 에 대한 괴델 문장(Godel sentence)이라고 한다.

KG(x2)¬PF(x2, G )(1) \vdash _K G \iff (\forall x_2) \neg PF(x_2, \ulcorner G\urcorner) \tag{1}

KK 가 조건 1), 2), 3) 을 만족하면 다음이 성립한다.

  1. KK 가 무모순이면, KG\vdash _KG 가 아니다.
  2. KKω\omega-무모순이면, K¬G\vdash _K \neg G 가 아니다.

그러므로 KKω\omega-무모순이면, GGKK 의 결정불가능한 문장이다.

  • 가정 1) 에 의하여 정리 3.26-3.28 이 적용된다. 가정 2) 와 3) 에 의하여 정리 3.13 이 적용되므로 모든 재귀 관계는 KK 에서 표현가능하다. 가정 3) 에 의하여 고정점 정리가 적용된다. KKRRRR, 특히 산술 SS, 또는 더욱 일반적으로 재귀 공리 집합을 갖는 RRRR 의 임의의 확장일 수 있다.

  • 표준 해석의 관점에서 (x2)¬PF(x2, G )(\forall x_2)\neg PF(x_2, \ulcorner G\urcorner)KK 에서 wff GG 의 증명의 괴델수인 자연수가 존재하지 않는다고 주장한다. 이는 곧 GG 의 증명이 KK 에 존재하지 않는다는 주장이다. 그러므로 GGGGKK 에서 증명불가능하다는 주장과 같다. 즉, GG 는 "나는 KK 에서 증명불가능하다" 라고 말하고 있는 것인데, 이는 거짓말쟁이의 역설 "나는 거짓말을 하고 있다" 와 같다.

    이 말이 참이면 이 말의 내용에 의하여 이 말은 거짓이 된다. 이 말이 거짓이면 이 말의 내용이 부정되므로 이 말은 참이 된다. 이처럼 "이 문장은 거짓이다" 라고 말하면 모순이다. 거짓말쟁이의 역설의 결론이 모순인 것처럼 GGKK 에서 결정불가능한 문장이다.

  • 괴델의 불완전성 정리는 위 조건 1)-3) 을 만족하는 언어 LA\mathcal{L}_A 에서 동등성을 지닌 임의의 이론 KK 에 적용된다.

    KK 가 또한 다음 조건을 만족시킨다고 가정하자.

    K 는 참된 이론이다.(+) K \text{ 는 참된 이론이다.} \tag{+}

    (KKSS 또는 SS 의 임의의 부분 이론이 될 수 있다.) 정리 3.37 의 결론 1) 은 KK 가 무모순이면 GGKK 에서 증명불가능하다는 것을 말해준다. 그러면 GG 의 진위 여부를 증명할 수 없으므로 GG 의 가부를 판정할 수 없는가? 그런데 표준 해석에서 GGKK 에서의 자신의 증명불가능성을 주장한다. 그러므로 GG 는 표준 해석에 대하여 참이다.

    또한, KK 가 참된 이론일 때 다음의 KK 에서 GG 의 결정불가능성에 대한 간단한 직관적인 논증이 주어진다.

    1. KG\vdash _KG 를 가정하자. KG(x2)¬PF(x2, G )\vdash _KG \iff (\forall x_2) \neg PF(x_2, \ulcorner G\urcorner) 이므로 K(x2)¬PF(x2, G )\vdash _K(\forall x_2)\neg PF(x_2, \ulcorner G\urcorner) 이다. KK 가 참된 이론이므로 (x2)¬PF(x2, G )(\forall x_2)\neg PF(x_2, \ulcorner G\urcorner) 는 표준 해석에서 참이다. 그러나 이 wff 는 GGKK 에서 증명 불가능하다고 말하고 있고, 이는 가정에 모순이다. 그러므로 KG\vdash _KG 가 아니다.
    2. K¬G\vdash _K \neg G 를 가정하자. KG(x2)¬PF(x2, G )\vdash _KG \iff (\forall x_2)\neg PF(x_2, \ulcorner G\urcorner) 이므로 K¬(x2)¬PF(x2, G )\vdash _K \neg (\forall x_2) \neg PF(x_2, \ulcorner G\urcorner) 이다. 즉, K(x2)PF(x2, G )\vdash _K(\exists x_2)PF(x_2, \ulcorner G\urcorner) 이다. KK 가 참된 이론이므로 이 wff 는 표준해석에서 참이다. 즉, GGKK 에서 증명가능하다. 이는 앞선 결과에 모순이다. 그러므로 K¬G\vdash _K \neg G 가 아니다.
  • 증명

    GG 의 괴델수가 qq 라고 하자.

    1. KG\vdash _K G 를 가정하자. GGKK 에서의 증명의 괴델수를 rr 이라고 하자. 그러면 Pf(r,q)\operatorname{Pf}(r, q) 이다. 그러므로 KPF(r,q)\vdash _K PF(\overline{r}, \overline{q}) 이다. 즉, KPF(r, G )\vdash _K PF( \overline{r}, \ulcorner G\urcorner) 이다.

      그러나 (1)(1)biconditional elimination에 의하여 K(x2)¬PF(x2, G )\vdash _K(\forall x_2)\neg PF(x_2, \ulcorner G\urcorner) 이다. rule A4 에 의하여 K¬PF(r, G )\vdash _K \neg PF(\overline{r}, \ulcorner G\urcorner) 이다. 그러므로 KK 는 모순이다.

      그러므로 KK 가 무모순이면 반드시 KG\vdash _KG 가 아니여야 한다.

    2. KKω\omega-무모순인 것과 K¬G\vdash _K \neg G 을 가정하자. (1)(1) 와 biconditional elimination 에 의하여 K¬(x2)¬PF(x2, G )\vdash _K \neg (\forall x_2)\neg PF(x_2, \ulcorner G\urcorner) 이다. 이는 다음과 같다.

      K(x2)PF(x2, G )(*) \vdash _K (\exists x_2)PF(x_2, \ulcorner G\urcorner) \tag{*}

      한편, KKω\omega-무모순이므로 정리 3.36 에 의하여 KK 는 무모순이다. 그러면 K¬G\vdash _K \neg G 이므로 KG\vdash _KG 가 아니다. 즉, KK 에서 GG 의 증명은 존재하지 않는다.

      그러므로 Pf(n,q)\operatorname{Pf}(n,q) 는 모든 자연수 nn 에 대하여 거짓이고, 그러므로 모든 자연수 nn 에 대하여 K¬PF(n, G )\vdash _K \neg PF(\overline{n}, \ulcorner G\urcorner) 이다. ( G \ulcorner G\urcornerq\overline{q} 이다.) 그러면 ω\omega-무모순성에 의하여 K(x2)PF(x2, G )\vdash _K(\exists x_2)PF(x_2, \ulcorner G\urcorner) 가 아니다. 이는 ()(*) 와 모순이다.

  • 이로써 완전성이 성립하는 1차 논리에 산술의 공리를 추가하면 완전성이 붕괴되고 체계에 불완전성이 내재된다는 것을 알아보았다. 그 원리는 쉽게 말해서 이렇다. 체계에 산술이 성립되도록 하면, 모든 명제와 증명이 수로 환원될 수 있고, 모든 재귀 함수를 체계 내에서 표현가능하다. 그러면 증명가능성을 주장하는 술어 Pf\operatorname{Pf} 도 wff PF\operatorname{PF} 로 표현가능하고, 고정점 정리가 성립하여서 괴델수 하나를 입력받는 임의의 명제 E(x1)E(x_1) 를 잡아도 E(x1)E(x_1) 이 그 괴델수 x1x_1 에 해당하는 명제 AA 와 동치라는 것을 증명할 수 있는 AA 가 존재하게 된다.

    이제 E(x1)E(x_1) 을 괴델수 x1x_1 에 해당하는 명제 AA 가 증명불가능하다고 주장하게 만들면 AAE( A )E(\ulcorner A\urcorner) 의 동치가 증명가능하게 되어 가불기가 걸린다. AA 가 증명가능하면, 이 증명가능한 동치관계 때문에 E( A )E(\ulcorner A\urcorner) 이 증명가능한데, 이로써 AA 가 증명불가능하다. 반면 AA 가 증명불가능하면 E( A )E(\ulcorner A\urcorner) 가 참이 되어 AA 가 증명가능한 것이 된다.

    이 불완전성이 의미하는 바는 불완전 체계 안에 기계적인 방식으로 자동적으로 증명불가능한 참인 사실들이 존재한다는 것이다. 그러나 물론 1차 논리는 완전하므로 기계적으로 자동적으로 모든 진리를 밝힐 수 있다. 괴델 문장 같은 결정불가능한 문장들이 체계 내에서 정의되는 기계적인 방식으로 증명이 불가능한 문장들이다. 그러나 괴델 문장은 메타 논증으로 증명된다. 괴델 문장이 자기 자신이 체계 내에서 증명불가능하다고 주장하는데, 실제로 그러하므로 괴델 문장은 참이다. 이렇게 약한 체계에서 체계가 정의하는 기계적인 방식(공리에 추론규칙을 적용하는 것)으로 증명이 불가능한 사실들은 더 강한 체계에서 증명된다.

The Godel–Rosser Incompleteness Theorem

괴델 문장 GG 의 결정불가능성의 증명은 ω\omega-무모순성을 가정한다. 로서는 결정불가능한 문장의 복잡도를 조금 올려서 ω\omega-무모순성에 대한 가정을 무모순성으로 교체할 수 있음을 보였다.

정리 3.38 괴델-로서의 불완전성 정리(Godel-Rosser Incompleteness Theorem), 로서 문장(Rosser sentence)

정리 3.37 의 가정 1)-3) 에 추가적으로 다음을 가정하자.

  1. 모든 자연수 nn 에 대하여 Kxnx=0x=1x=n\vdash _Kx \leq \overline{n} \implies x = 0 \lor x = \overline{1} \lor \dots \lor x = \overline{n}.
  2. 모든 자연수 nn 에 대하여 Kxnnx\vdash _Kx \leq \overline{n}\lor \overline{n}\leq x.

그러면 KK 는 재귀 공리 집합을 가진 RRRR 의 임의의 확장이고, 특히 KKRRRR 이나 SS 가 될 수 있다.

정리 3.26(14) 에 의하여 Neg\operatorname{Neg} 는 원시 재귀 함수이고 wff BB 의 괴델수 xx 에 대하여 Neg(x)\operatorname{Neg}(x)(¬B)(\neg B) 의 괴델수이다. 모든 재귀 함수가 KK 에서 표현가능하므로 NEG(x1,x2)NEG(x_1, x_2)KK 에서 표현된 Neg\operatorname{Neg} 라고 하자. 그러면 x2x_2x1x_1 의 wff 의 부정의 괴델수이다.

이제 다음과 같이 wff E(x1)E(x_1) 을 정의하자.

(x2)(PF(x2,x1)(x3)(NEG(x1,x3)(x4)(x4x2PF(x4,x3)))) \begin{align}\begin{split} (\forall x_2) \Big ( PF(x_2, x_1) \implies & (\forall x_3) \big ( NEG(x_1, x_3) \\ & \implies (\exists x_4) ( x_4 \leq x_2 \land PF(x_4, x_3) ) \big ) \Big ) \\ \end{split}\end{align} \tag*{}

고정점 정리에 의하여 다음을 만족하는 닫힌 wff RR 이 존재한다.

KRE( R )(1) \vdash _K R \iff E(\ulcorner R\urcorner) \tag{1}

RRKK 에 대한 로서 문장(Rosser sentence)이라고 하자. KK 가 조건 1)-5) 를 만족하고 KK 가 무모순이면, RRKK 의 결정불가능한 문장이다.

  • 표준해석에서 RR 의 직관적 의미는 RRKK 에서 괴델수 x2x_2 인 증명을 가지면 ¬R\neg Rx2x_2 보다 작은 괴델수의 증명을 가진다는 것이다. 그러면 ¬R\neg R 의 부정은 또 다시 그것보다 작은 괴델수의 증명을 갖는다. 이것은 RRKK 의 무모순성을 가정했을 때 증명불가능하다는 것을 뜻한다.

  • 이론 SS 에 대한 괴델 문장과 로서 문장은 SS 의 결정불가능한 문장이다. 괴델 문장 GGGGSS 에서 증명불가능하다고 주장한다. 이처럼 이 결정불가능한 문장은 직관적인 수학적 의미를 갖는다.

    최근까지 수학적으로 본질적인 관심을 갖는 SS 의 결정불가능한 문장은 알려지지 않았다. 그러나 1977년에 유한 램지 정리에 관련된 수학적으로 중요한 조합적 문장이 SS 에서 결정불가능하다는 것이 보여졌다.

  • 증명

Recursively Axiomatizable

재귀적으로 공리화가능한(recursively axiomatizable)

이론 KK 가 재귀적으로 공리화가능하다는 것은 재귀 공리 집합을 갖고 KK 와 같은 정리는 갖는 이론 KK ^{*} 이 존재한다는 것이다.

따름정리 3.39

언어 LA\mathcal{L}_A 의 이론 KK 가 무모순이고 재귀적으로 공리화 가능한 RRRR 의 확장이면, KK 는 결정불가능한 문장을 갖는다.

  • 증명

    KK ^{*}KK 와 같은 정리를 갖고 재귀 공리 집합을 가지면 정리 3.38 의 가정 1)-5) 가 KK ^{*} 에서 성립한다. 그러므로 KK ^{*} 에 대한 로서 문장은 KK ^{*} 에서 결정불가능하고, 그러므로 KK 에서도 결정불가능하다. ■

Church's Thesis

효과적으로 결정가능한(effectively decidable)

대상의 집합이 효과적으로 결정가능하다는 것은 주어진 임의의 대상이 그 집합에 속했는지 결정하는 기계적인 절차가 존재한다는 것이다.

  • 기계적인 절차란 기발함이나 독창성 없이 자동적으로 수행할 수 있는 절차이다.

재귀적 집합(recursive set)

자연수 집합 AA 가 재귀적이라는 것은 성질 xAx \in A 가 재귀적이라는 것이다.

  • xAx \in A 가 재귀적이라는 것은 특성함수 CAC_A 가 재귀 함수라는 것이다.

처치의 논제(Church's thesis)

재귀 집합은 효과적으로 결정가능한 자연수 집합과 같다.

  • 처치의 논제는 다음과 같은 형태로도 취해진다. 이는 위의 정의와 동등하다.

    수론적 함수가 효과적으로 계산가능한 것은 그것이 재귀인 것과 동치이다.

    처치의 논제는 재귀가 아닌 함수를 기계적으로 계산할 절차가 존재하지 않는다는 것을 말한다.

  • 계산가능성에서 재귀 집합의 개념이 효과적으로 결정가능한 자연수 집합의 개념과 같다는 것을 이해해야 한다. 이 가정을 처치의 논제(Church's thesis)라고 한다.

    이론이 공리적이라는 것은 그것의 공리가 효과적으로 결정가능한 것이다. 공리집합이 효과적으로 결정가능하다는 것과 공리의 괴델수 집합이 효과적으로 결정가능하다는 것은 동치이다. wff 를 그것의 괴델수로 효과적으로 보낼 수 있고, 그 역도 가능하기 때문이다. 그러므로 처치의 논제를 받아들이면, KK 가 재귀 공리 집합을 갖는다는 것은 KK 가 공리적 이론이라는 것과 같고, 그러므로 따름정리 3.39 는 RRRR 이 본질적으로 불완전하다는 것을 말해준다. 즉, RRRR 의 모든 무모순 공리적 확장은 결정불가능한 문장을 갖는다. 이 결과는 산술의 완전한 공리화가 존재할 수 없다, 즉, 수론의 모든 문제를 결정할 수 있는 기반 위에 공리적 체계를 구축할 방법이 없다는 것을 말해주기 때문이다.

Godel's Second Incompleteness Theorem

체계의 무모순성을 주장하는 wff CONCON

KK 를 언어 LA\mathcal{L}_A 에서 재귀 공리 집합을 갖는 SS 의 확장이라고 하자. CONKCON_K 를 다음의 KK 의 닫힌 wff 라고 정의하자.

(x1)(x2)(x3)(x4)¬(NEG(x3,x4)PF(x1,x3)PF(x2,x4)) (\forall x_1)(\forall x_2)(\forall x_3)(\forall x_4) \neg \big (NEG(x_3, x_4) \land PF(x_1, x_3) \land PF(x_2, x_4) \big )

표준 해석에서 CONKCON_K 는 wff 와 그것의 부정의 증명이 동시에 존재하지 않는다고 주장한다. 즉, KK 의 무모순성을 주장한다.

  • KK 의 괴델 문장 GG 에 대하여 다음과 같은 문장 G\Bbb{G} 를 정의하자.

    CONKG CON_K \implies G

    GGGGKK 에서 증명불가능하다고 주장한다. 그러므로 G\Bbb{G}KK 가 무모순이면 GGKK 에서 증명불가능하다고 주장하는 것이다. 그런데 이것은 괴델의 불완전성 정리의 결론 1) 이다.

    이 정리의 증명에서 사용된 메타수학적 추론은 표현될 수 있고 KK 안에서 수행될 수 있기 때문에 G\Bbb{G}KK 에서의 증명을 얻을 수도 있다. 따라서 KCONKG\vdash _K CON_K \implies G 이다. 그러나 괴델의 불완전성 정리에 의하여 KK 가 무모순이면 GGKK 에서 증명불가능하다. 그러므로 KK 가 무모순이면 CONKCON_KKK 에서 증명불가능하다. 만약 KK 의 무모순성을 KK 의 체계 내에서 증명가능하다면 CONKCON_KKK 안에서 증명가능한 것이고, 곧 KCONK\vdash _K CON_K 이므로 MP 에 의하여 KG\vdash _K G 인데, 이는 불완전성 정리와 모순이다.

    이것이 아래에서 살펴볼 괴델의 두번째 불완전성 정리(1931)가 말하는 바이다. 만약 KK 가 무모순이면 KK 의 무모순성을 KK 안에서 증명할 수 없다. 즉, KK 의 무모순성 증명은 반드시 KK 에서 사용할 수 있는 아이디어나 방법론의 범주를 초월해있는 아이디어와 방법론을 사용해야 한다. SS(산술) 의 무모순성 증명은 최초로 겐첸(1936)에 의하여 제시되었고 이후에 다른 수학자들에 의하여 다른 증명들도 제안되었다. 이 내용을 PA\mathsf{PA} 의 서수 분석에서 엄밀하게 알아본다. 이 증명들은 SS 안에서 형식화 불가능한 개념과 방법들(가령, 가산 무한 서수 이론의 일부)을 사용한다.

    괴델의 두번째 불완전성 정리는 쉬운 말로 이렇게 표현된다. 이론 KK 가 "충분히 강력하면" KK 의 무모순성을 KK 안에서 증명할 수 없다. KK 의 무모순성을 형식화하는 방법은 중요하다. 페퍼만(Feferman, 1960)은 SS 의 무모순성 CONSCON_S 를 형식화할 수 있는 방법을 보였다. 괴델의 두번째 불완전성 정리의 정확한 형식화는 페퍼만(1960)의 논문 《Arithmetization of metamathematics in a general setting》 에서 찾을 수 있다.

The Hilbert–Bernays Derivability Conditions

힐베르트-버네이즈 도출가능성 조건(The Hilbert–Bernays Derivability Conditions)

BEW(x1)BEW(x_1)(x2)PF(x2,x1)(\exists x_2)PF(x_2, x_1) 로 정의하자. 임의의 wff CC 에 대하여 C\Box CBEW( C )BEW(\ulcorner C\urcorner) 로 정의하자.

SS 의 임의의 닫힌 wff C,DC, D 에 대하여 힐베르트-버네이즈 도출가능성 조건은 다음과 같다.

(HB1)(HB1) \quad SC\vdash _SC 이면 SC\vdash _S \Box C 이다.

(HB2)S(CD)(CD)(HB2) \quad \vdash _S \Box (C \implies D) \implies (\Box C \implies \Box D)

(HB3)SCC(HB3) \quad \vdash _S \Box C \implies \Box \Box C

  • 힐베르트와 버네이즈(Hilbert and Bernays, 1939)는 그들의 괴델의 두번째 정리의 증명을 도출가능성 조건(derivability condition)을 기반으로 했다. 확실하게 하기 위하여 괴델의 두번째 불완전성 정리가 SS 의 재귀적인 공리화가능한 확장에도 성립하지만 오직 이론 SS 만을 생각하자.

  • 표준해석에서 BEW(x1)BEW(x_1) 은 괴델수 x1x_1 의 wff 의 증명이 SS 에 존재한다고 주장한다. 즉, 괴델수 x1x_1 의 wff 는 SS 에서 증명가능하다. BEWBEW 는 증명가능성을 뜻하는 독일어 약자이다.

    SS 에 대한 괴델 문장 GG 는 고정점 조건을 만족하므로 SG¬BEW( G )\vdash _S G \iff \neg BEW(\ulcorner G\urcorner) 가 성립한다.

  • (HB1)(HB1) 의 증명은 쉽다. (HB2)(HB2)PFPF 의 성질로 쉽게 얻을 수 있다.

    그러나 (HB3)(HB3) 의 증명은 어렵다. Boolos, G. (1993) The Logic of Provability 와 Shoenfield, J. (1967) Mathematical Logic 를 참고하면 된다.

  • 증명

Henkin Sentence

헹킨 문장(Henkin sentence)

고정정 정리를 사용하여 SHH\vdash _S H \iff \Box H 을 만족하는 문장 HH 를 얻을 수 있다. HHSS 에 대한 헹킨 문장이라고 한다.

  • SS 에 대한 괴델 문장 GGSS 에서의 자신의 증명불가능성을 주장한다. 즉, SG¬G\vdash _S G \iff \neg \Box G 이다.

    HHSS 에서의 자기 자신의 증명가능성을 주장한다. HH 가 참인지, 증명가능하거나 증명불가능하거나 결정불가능한지 판정하기는 어렵다. 이 문제는 롭(Lob, 1955)에 의하여 아래의 정리 3.40 을 기반으로 해결되었다.

Lob's Theorem

정리 3.40 롭의 정리(Lob's Theorem)

SS 의 문장 CC 에 대하여 SCC\vdash _S \Box C \implies C 이면 SC\vdash _S C 이다.

  • 증명

    wff BEW(x1)CBEW(x_1) \implies C 에 고정점 정리를 적용하여 SL(BEW( L )C)\vdash _S L \iff (BEW(\ulcorner L\urcorner) \implies C) 를 만족하는 문장 LL 을 얻자. 즉, SL(LC)\vdash _S L \iff (\Box L \implies C) 이다. 이제 다음과 같이 CC 를 연역하자.

    연역 근거
    1 SL(LC)\vdash _S L \iff (\Box L \implies C) 위의 논증에 의하여
    2 SL(LC)\vdash _S L \implies (\Box L \implies C) 1, biconditional elimination
    3 S(L(LC))\vdash _S \Box (L \implies (\Box L \implies C)) 2, (HB1)(HB1)
    4 SL(LC)\vdash _S \Box L \implies \Box (\Box L \implies C) 3, (HB2)(HB2), MP
    5 S(LC)(LC)\vdash _S \Box (\Box L \implies C) \implies (\Box \Box L \implies \Box C) (HB2)(HB2)
    6 SL(LC)\vdash _S \Box L \implies (\Box \Box L \implies \Box C) 4, 5, 적절한 항진식에 의하여
    7 SLL\vdash _S \Box L \implies \Box \Box L (HB3)(HB3)
    8 SLC\vdash _S \Box L \implies \Box C 6, 7, 적절한 항진식에 의하여
    9 SCC\vdash _S \Box C \implies C Hyp
    10 SLC\vdash _S \Box L \implies C 8, 9, 적절한 항진식에 의하여
    11 SL\vdash _S L 1, 10, biconditional elimination
    12 SL\vdash _S \Box L 11, (HB1)(HB1)
    13 SC\vdash _S C 10, 12, MP

따름정리 3.41

SS 에 대한 헹킨 문장 HH 에 대하여 SH\vdash _S H 이고 HH 가 표준해석에서 참이다.

  • 증명

    SHH\vdash _S H \iff \Box H 이다. biconditional elimination에 의하여 SHH\vdash _S \Box H \implies H 이다. 롭의 정리에 의하여 SH\vdash _S H 이다. HH 의 내용이 HHSS 에서의 증명가능성을 주장하므로 HH 는 참이 된다. ■

Godel's Second Incompleteness Theorem

정리 3.42 괴델의 두번째 불완전성 정리(Godel's Second Incompleteness Theorem)

SS 가 무모순이면 SCONS\vdash _SCON_S 이 아니다.

  • 즉, 산술이 무모순이면 산술의 무모순성을 산술 내에서 증명할 수 없다. 산술의 무모순성은 반드시 산술의 바깥의 힘에 의존해야 증명된다.

    괴델의 두번째 불완전성 정리는 LA\mathcal{L}_A 에서 재귀 공리 집합을 갖는 SS 의 임의의 확장에서 성립하지만 수학자들이 산술을 설명하기 위하여 구축한 체계 SS 에 포커싱하기 위하여 SS 에 대하여 정리를 서술한 것이다.

  • 증명

    SS 의 무모순성을 가정하자. S01\vdash _S 0 \neq \overline{1} 이므로 SS 의 무모순성에 의하여 S0=1\vdash _S 0 = \overline{1} 이 아니다. 그러면 롭의 정리에 의하여 S(0=1)0=1\vdash _S \Box (0 = \overline{1})\implies 0 = \overline{1} 이 아니다. 그렇다면 항진식 ¬A(AB)\neg A \implies (A \implies B) 에 의하여 다음이 성립한다.

    S¬(0=1) 이 아니다.(1) \vdash _S \neg \Box (0 = \overline{1}) \text{ 이 아니다.} \tag{1}

    S01\vdash _S 0 \neq \overline{1} 이므로 (HB1)(HB1) 에 의하여 S(01)\vdash _S \Box (0 \neq \overline{1}) 이다. 그러면 SCONS¬(0=1)\vdash _S CON_S \implies \neg \Box (0 = \overline{1}) 라는 사실은 쉽게 증명된다.

    그런데 이 결론은 SCONS\vdash_S CON_S 일 때 S¬(0=1)\vdash _S\neg \Box (0 = \overline{1}) 라는 것을 의미하는데, 이것과 (1)(1)SS 의 무모순성에 위배된다. 그러므로 SCONS\vdash _SCON_S 가 아니여야 한다. ■

  • 산술이 무모순이면 산술의 무모순성을 체계 내에서 증명할 수 없다. 산술의 무모순성을 증명하려면 반드시 체계를 초월해 있는 아이디어나 방법론을 사용해야만 한다. 즉, 산술의 무모순성은 상위 체계에 의존한다.

    이 내용을 PA\mathsf{PA} 의 서수 분석에서 알아본다.

    이 결과는 충격적이었다. 체계의 특정 성질에 대한 결론을 내리기 위해서는 반드시 다른 체계의 논증이 필요하다! 이는 체계가 갖는 모든 진실이 체계 내로부터 생성될 수 없다는 것을 뜻했다. 이는 공리와 추론규칙을 기계에 입력하면 모든 진실이 도출되는 힐베르트 프로그램이 존재할 수 없다는 것을 뜻했다. 괴델이 불완전성 정리를 발표하는 회장에서 두번째 불완전성 정리까지 발표하자 폰 노이만은 힐베르트 학파 사람들에게 "이제 우린 다 끝났군요" 라고 말했다.

    유클리드의 『원론』 이 고대 그리스의 수학을 정립하면서 공리를 통하여 정리를 도출해내었다. 이때부터 수학자들은 수학이란 공리로부터 진실들을 도출해내는 학문이라는 인식을 갖게 되었다. 또한, 유클리드의 기하학이 세상을 표현하는 참된 진리라는 믿음을 갖고 있었다. 수학이 유럽으로 전달되었을 때 유럽은 기독교 문화를 갖고 있었다. 수학자들은 유클리드의 기하학이 하나님이 세상을 만드신 설계도라고 생각하며, 수학의 진실을 규명해내고 밝혀내는 것 자체가 하나님의 신성을 나타내는 일이라고 생각했다. 그리고 그 과정 중에서 수학자들은 엄밀한 증명에 의존하지 않았다. 왜냐하면 어차피 수학이 신이 세상을 만든 설계도이므로 그 기반의 엄밀함을 의심할 필요가 없기 때문이다. 칸트도 비판 시리즈를 펼쳐내면서 이 시대정신에 가담했지만, 데이비드 흄은 반박을 했다. 그러나 대중들은 칸트의 편을 들었다.

    그러나 가우스가 비유클리드 기하학으로 인하여 유클리드 기하학이 유일한 기하학이 아니라는 것을 밝혀내자 수학의 기반이 흔들렸다. 수학이 세상의 설계도가 아닐 수도 있고, 단지 바둑이나 체스처럼 인간의 생각의 인위적인 산물에 불과할 수도 있다는 공포가 엄습하기 시작했다. 또한 이 사실은 인류가 얼마나 시대정신에 휩쓸려서 진실을 판단하는지를 보여주었다. 설령 당대의 저명한 학자와 객관적으로 판단할 수 있고 최고의 판단능력을 갖고 있다고 여겨졌던 수학자들까지도 얼마나 시대정신에 영향을 받아서 판단능력이 흐려졌던 것인가? 실제로 가우스도 비유클리드 기하학을 발견했지만 놀림받을 것이 두려워서 죽을 때까지 비유클리드 기하학을 발표하지 않았다.

    수학을 신으로부터 내려온 설계도라고 생각한 것은 인간의 오만함이었다. 그때부터 수학자들은 수학의 기반이 무너지지는 않을까 하는 두려움에 시달렸다. 그리고 그 두려움이 수학의 무모순성 증명을 발견해야만 한다는 갈망을 일으켰다. 힐베르트는 비유클리드 기하학을 유클리드 기하학으로 사상시켜서 유클리드 기하학의 무모순성이 증명되면 비유클리드 기하학도 무모순이 되게 했다. 그리고 최종적으로 기하학의 무모순성을 산술의 무모순성에 의존시켰다. 수학자들은 통계학, 해석학 등등 모든 수학 분야의 무모순성을 산술의 무모순성에 의존시켰다. 이제 초유의 관심사는 산술의 무모순성이다.

    힐베르트는 유클리드로부터 시작된 공리적 방법론을 통하여 모든 진실을 규명해낼 수 있을 것이라고 생각했고, 이것이 수학자들의 대중적인 믿음이었다. 그러나 괴델은 공리적 방법론으로는 모든 진실을 밝혀낼 수 없고, 생성할 수 없다는 것을 보여주었다. 힐베르트는 그 유명한 폰 노이만의 스승이다. 이 사건은 힐베르트 정도 되는 위치에 있는 사람까지도 얼마나 주관적으로 판단했는지, 얼마나 시대정신에 휩쓸려서 생각했는지 알 수 있다.

    인간은 진정으로 객관적으로 판단할 수 있을까? 인간이 자신의 지혜로 객관적으로 판단하여 진리에 도달할 수 있는가? 매우 객관적이라고 믿어왔던 사실들도 사실은 주관적인 믿음이었고 편향이었고 편견이었고 시대정신과 대중적인 관념에 휩쓸려서 내려진 결론이었다. 그렇다면 인류가 지금도 갖고 있는 믿음과 진실과 사실들에 얼마나 많은 거짓이 섞여있을까? 진실을 알기 위하여 인간이 자기 지혜에 의지할 수 없다면 인간은 진실을 가르쳐줄 존재로써 무엇에 의지해야 하는가?

Recursive Undecidability

재귀적으로 결정가능한(recursively decidable), 재귀적으로 결정불가능한(recursively undecidable), 본질적으로 재귀적으로 결정불가능한(essentially recursively undecidable)

이론 KK 에 대하여 KK 의 정리의 괴델수의 집합을 TKT_K 라고 하자.

TKT_K 가 재귀 집합이면, 즉, 성질 xTKx \in T_K 가 재귀일 때 KK 를 재귀적으로 결정가능하다고 한다.

TKT_K 가 재귀가 아닐 때 KK 를 재귀적으로 결정불가능하다고 한다.

KKKK 의 모든 무모순 확장이 재귀적으로 결정불가능할 때 KK 를 본질적으로 재귀적으로 결정불가능하다고 한다.

  • 처치의 논제를 받아들이면, 재귀적 결정불가능성은 효과적 결정불가능성과 같다. 즉, 정리에 대한 기계적인 결정절차가 존재하지 않는다. 그러므로 임의의 wff 가 정리인지 판정하기 위해서 무지성의 기계적인 방법이 아닌 기발함과 독창성이 필요하다.

정리 3.43

대각함수 DD 가 표현가능한 언어 LA\mathcal{L}_A 에서 동등성을 지닌 무모순 이론 KK 에 대하여 성질 xTKx \in T_KKK 에서 표현불가능하다.

  • 증명

    xTKx \in T_KKK 에서 wff T(x1)T(x_1) 에 의하여 표현가능하다고 하자. 그러면 다음이 성립한다.

    1. nTKn \in T_K 이면 KT(n)\vdash _KT(\overline{n}).
    2. n∉TKn \not \in T_K 이면 K¬T(n)\vdash _K \neg T(\overline{n}).

    3. 대각화 보조정리¬T(x1)\neg T(x_1) 에 적용하면 KC¬T( C )\vdash _KC \iff \neg T(\ulcorner C\urcorner) 를 만족하는 문장 CC 가 존재한다. CC 의 괴델수를 qq 라고 하면 다음이 성립한다.

      KC¬T(q)\vdash _KC \iff \neg T(\overline{q})

    KC\vdash _KC 라고 하자. 그러면 CC 가 정리이고 CC 의 괴델수가 qq 이므로 qTKq \in T_K 이다. 그러나 KC\vdash _KC 와 c) 에 biconditional elimination을 적용하면 K¬T(q)\vdash _K \neg T(\overline{q}) 이다. 그러므로 KK 는 모순적이다. 그러나 이는 가정과 모순된다. ▲

    KC\vdash _KC 가 아니라고 하자. 그러면 q∉TKq \not\in T_K 이다. b) 에 의하여 K¬T(q)\vdash _K \neg T(\overline{q}) 이다. 그러면 c) 와 biconditional elimination 에 의하여 KC\vdash _KC 이다. ▲

    두 경우 모두 모순이 도출된다. ■

Tarski's Theorem

산술적 집합(arithmetical set)

자연수 집합 BB 가 산술적 집합이라는 것은 언어 LA\mathcal{L}_A 에서 다음을 만족하는 하나의 자유변수 xx 를 갖는 wff C(x)C(x) 가 존재한다는 것이다.

  • 모든 자연수 nn 에 대하여 nBn \in B 인 것과 표준해석에서 C(n)C(\overline{n}) 이 참인 것은 동치이다.
  • 산술적 집합은 산술의 형식문으로 정의가능한 자연수 집합을 뜻한다. 즉, 언어 LA\mathcal{L}_A 로 표현가능한 집합이 산술 집합이다.

  • 예시

    소수 집합은 산술적이다.

따름정리 3.44 타르스키의 정리(Tarski's Theorem)

TrTr 을 표준해석에서 참인 SS 의 wff 들의 괴델수의 집합이라고 하자. 그러면 TrTr 은 산술적이지 않다.

  • 이 정리는 러프하게 말해서 산술적 진리의 개념이 산술적으로 정의불가능하다는 것을 말해준다.

  • 증명

    표준 해석에서 참인 모든 wff 를 고유공리로 갖는 SS 의 확장 NN 을 잡자. NN 의 모든 정리가 표준해석에서 참이므로 NN 의 정리는 NN 의 공리와 같다. 그러므로 TN=TrT_N = Tr 이다.

    따라서 임의의 닫힌 wff BB 에 대하여 BB 가 표준 해석에서 성립하는 것은 NB\vdash _N B 와 동치이다. 그렇다면 집합 BB 가 산술적이라는 것은 성질 xBx \in BNN 에서 표현가능하다는 것과 동치이다. (BB 가 산술적이면 자연수 nn 에 대하여 nBn \in B 인 것과 표준해석에서 C(n)C(\overline{n}) 이 참인 것이 동치가 되게 하는 wff C(x)C(x) 가 존재한다는 것인데, 앞선 논증에 의하여 C(x)C(x) 가 참이면 정리이므로 표현가능하기 때문이다.)

    NN 이 표준 해석을 모델로 가지므로 NN 의 무모순성을 가정할 수 있다. 모든 재귀 함수가 SS 에서 표현가능하므로 모든 재귀 함수가 NN 에서 표현가능하고, 그러므로 대각 함수 DDNN 에서 표현가능하다. 그렇다면 정리 3.43 에 의하여 xTrx \in TrNN 에서 표현불가능하다.

    NN 이 무모순이고, 집합 BB 가 산술적인 것과 xBx \in BNN 에서 표현가능한 것이 동치이므로 TrTr 은 산술적이지 않다. ■

정리 3.45

모든 재귀 함수가 표현가능한 언어 LA\mathcal{L}_A 에서 동등성을 지닌 무모순 이론 KK 에 대하여 K01\vdash _K 0 \neq \overline{1} 이면 KK 는 재귀적으로 결정불가능하다.

  • 증명

    대각 함수 DD 가 원시 재귀이므로 KK 에서 표현가능하다. 정리 3.43 에 의하여 성질 xTKx \in T_KKK 에서 표현불가능하다. 정리 3.13에 의하여 특성 함수 CTKC _{T_K}KK 에서 표현불가능하다. 따라서 CTKC _{T_K} 는 재귀 함수가 아니다. 그러므로 TKT_K 는 재귀 집합이 아니고, 그러므로 KK 는 재귀적으로 결정불가능하다. ■

Godel-Rosser Theorem

따름정리 3.46

RRRR 은 본질적으로 재귀적으로 결정불가능하다.

  • RRRR 이 무모순인 이유를 그것이 표준해석을 모델로써 갖기 때문이라고 볼 수 있으나, 더욱 구조적인 무모순성 증명이 이후에 Beth 와 Kleene 등에 의해 주어졌다.

    이제 이 결과가 괴델-로서 정리의 또 다른 변형을 도출하게 된다.

  • 증명

    RRRRRRRR 의 모든 무모순 확장은 정리 3.45 의 KK 에 대한 조건을 만족한다. 그러므로 RRRR 은 본질적으로 재귀적으로 결정불가능하다. ■

정리 3.47

재귀 어휘를 갖는 이론 KK 에 대하여 KK 가 재귀적으로 공리화가능하고 재귀적으로 결정불가능하면, KK 는 불완전하다.

  • KK 가 불완전하다는 것은 KK 는 결정불가능한 문장을 가진다는 것이다.

  • 증명

따름정리 3.48 괴델-로서 정리(Godel-Rosser Theorem)

임의의 무모순인 재귀적으로 공리화가능한 RRRR 의 확장은 결정불가능한 문장을 갖는다.

  • 증명

    따름정리 3.46 과 정리 3.47 에 의하여 바로 나온다.

Finite Extension, Compatible

유한 확장(finite extension), 양립가능(compatible)

같은 언어의 두 이론 K1,K2K_1, K_2 에 대하여 다음과 같이 정의한다.

  1. K2K_2K1K_1 의 유한 확장이라는 것은 wff 집합 AA 와 wff 유한 집합 BB 가 존재하여 다음 조건을 만족한다는 것이다.

    1. K1K_1 의 정리들이 AA 에서 도출가능한 wff 들이다.
    2. K2K_2 의 정리들이 ABA \cup B 에서 도출가능한 wff 들이다.
  2. K1K2K_1 \cup K_2K1K_1K2K_2 의 공리 집합의 합집합으로 정의하자. K1K_1K2K_2 가 양립가능하다는 것은 K1K2K_1 \cup K_2 가 무모순이라는 것이다.

정리 3.49

같은 언어의 두 이론 K1,K2K_1, K_2 에 대하여 K2K_2K1K_1 의 유한 확장이고 K2K_2 가 재귀적으로 결정불가능하면, K1K_1 은 재귀적으로 결정불가능하다.

  • 증명

정리 3.50

언어 LA\mathcal{L}_A 의 이론 KKRRRR 과 양립가능하면 KK 는 재귀적으로 결정불가능하다.

  • 증명

따름정리 3.51

모든 참된 이론 KK 는 재귀적으로 결정불가능하다.

  • 증명

따름정리 3.52

언어 LA\mathcal{L}_A 위에서의 술어 계산 PSP_S 는 재귀적으로 결정불가능하다.

  • 증명

Full and Pure first-order predicate calculus

완전 1차 술어 계산(full first-order predicate calculus), 순수 1차 술어 계산(pure first-order predicate calculus)

완전 1차 술어 계산이란 모든 술어 기호와 함수 기호와 개별 상수를 갖는 1차 술어 계산이고, PF\operatorname{PF} 라고 표기한다. 순수 1차 술어 계산이란 모든 술어 기호를 포함하지만 함수 기호와 개별 상수를 전혀 포함하지 않는 1차 술어 계산이고, PP\operatorname{PP} 라고 표기한다.

보조정리 3.53

다음을 만족하는 재귀 함수 hh 가 존재한다.

  • 괴델수 uu 를 갖는 PF\operatorname{PF} 의 임의의 wff BB 에 대하여 괴델수 h(u)h(u) 를 갖고 다음을 만족하는 PP\operatorname{PP} 의 wff BB' 가 존재한다.

    • BBPF\operatorname{PF} 에서 증명가능한 것과 BB'PP\operatorname{PP} 에서 증명가능한 것은 동치이다.
  • 증명

Church's Theorem

정리 3.54 처치의 정리(Church's Theorem)

PF\operatorname{PF}PP\operatorname{PP} 는 재귀적으로 결정불가능하다.

  • 처치의 논제를 받아들이면 재귀적 결정불가능함은 효과적 결정불가능함과 같다. 그렇다면 이 정리는 PP\operatorname{PP}PF\operatorname{PF} 의 정리를 인지할 수 있는 결정절차가 존재하지 않는다는 것을 의미한다. 완전성 정리에 의하여 이 결과는 주어진 임의의 wff 가 논리적으로 타당한지 효과적으로 판정할 방법이 존재하지 않는다는 것을 의미한다.

  • 증명


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