5.10 원시 재귀 함수를 통한 구문론적 조작의 산술적 표현
1. 구문론적 조작의 산술화
괴델 증명에서 형식 체계의 구문론적 조작(Syntactic Operations)—기호열의 연결, 대입, 공리 인스턴스 생성, 추론 규칙 적용 등—이 괴델 수 위의 원시 재귀 함수(Primitive Recursive Functions)로 표현됨을 보이는 것이 기술적 핵심이다. 이 표현 가능성이 메타수학적 술어의 PA 내 표현의 기반이 된다.
2. 기본 산술 함수의 원시 재귀성
2.1 소수 관련 함수
p(n): n번째 소수
p(0) = 2, \quad p(n+1) = \mu k \leq p(n)! + 1 \, [\text{Prime}(k) \wedge k > p(n)]
유클리드의 소수 무한성 증명에 의해, p(n)! + 1 이하에 p(n)보다 큰 소수가 반드시 존재한다. 제한 무한화(Bounded Minimization)이므로 원시 재귀적이다.
\text{exp}(a, i): a의 소인수분해에서 p(i)의 지수
\text{exp}(a, i) = \mu k \leq a \, [p(i)^{k+1} \nmid a]
\text{len}(a): 열의 길이 (소인수분해에서 지수가 0이 아닌 소수의 최대 인덱스)
\text{len}(a) = \mu i \leq a \, [p(i+1) \nmid a]
기호열 조작 함수의 원시 재귀성
연결(Concatenation)
두 기호열의 괴델 수를 입력으로 받아, 연결된 기호열의 괴델 수를 출력하는 함수:
\text{concat}(a, b) = a \cdot \prod_{i=1}^{\text{len}(b)} p(\text{len}(a) + i)^{\text{exp}(b, i)}
a의 소인수분해를 유지하면서, b의 각 원소를 a 이후의 소수 위치에 배치한다.
이 함수는 원시 재귀적이다. 곱은 제한된 범위의 반복 곱셈(원시 재귀)이고, 각 구성 요소(\text{len}, \text{exp}, p)가 원시 재귀적이기 때문이다.
2.2 부분열 추출(Subsequence Extraction)
기호열의 i번째부터 j번째까지의 부분열을 추출하는 함수:
\text{substr}(a, i, j) = \prod_{k=i}^{j} p(k-i+1)^{\text{exp}(a, k)}
기호 출현 검사(Symbol Occurrence Check)
기호열 a에 기호 s가 출현하는지 검사:
\text{occurs}(s, a) = \exists i \leq \text{len}(a) \, [\text{exp}(a, i) = s]
제한 양화이므로 원시 재귀적이다.
3. 구문론적 판별 함수
3.1 항 판별(Term Check)
\text{Term}(a): “a는 항의 괴델 수이다”
항의 귀납적 정의에 따라:
- a = \#(0) (상수 0의 괴델 수) → \text{Term}(a)
- a가 변수의 괴델 수 → \text{Term}(a)
- a가 S(t) 형태이고 t가 항 → \text{Term}(a)
- a가 (t_1 + t_2) 또는 (t_1 \times t_2) 형태이고 t_1, t_2가 항 → \text{Term}(a)
이 판별은 기호열의 구조를 재귀적으로 분석하여 수행되며, 항의 길이에 대한 귀납법에 의해 원시 재귀적으로 정의된다.
3.2 공식 판별(Formula Check)
\text{Form}(a): “a는 적격식의 괴델 수이다”
원자식, 부정, 조건, 전칭 양화의 네 구성 형태에 대해 재귀적으로 검사한다. 공식의 길이에 대한 귀납법에 의해 원시 재귀적이다.
3.3 문장 판별(Sentence Check)
\text{Sent}(a): “a는 문장(자유 변수 없는 공식)의 괴델 수이다”
\text{Form}(a)이고 a에 자유 변수가 없음을 검사. 자유 변수의 집합을 계산하는 함수가 원시 재귀적이므로, \text{Sent}도 원시 재귀적이다.
4. 공리 판별 함수
4.1 논리적 공리 판별
\text{LogAx}(a): “a는 논리적 공리의 괴델 수이다”
논리적 공리 도식의 각 인스턴스인지를 검사한다. 예를 들어, “a가 \phi \rightarrow (\psi \rightarrow \phi) 형태인지“를 a의 기호열 구조를 분석하여 판별한다. 도식의 각 형태에 대해 패턴 매칭을 수행하며, 유한 개의 도식 형태에 대한 논리합으로 구성된다.
4.2 페아노 공리 판별
\text{PAx}(a): “a는 PA의 비논리적 공리의 괴델 수이다”
고정 공리(영의 비후자성, 후자의 단사성, 덧셈/곱셈의 재귀 정의)는 유한 개이므로 직접 비교로 판별. 귀납법 공리 도식의 인스턴스 판별은 “a가 [\phi(0) \wedge \forall x (\phi(x) \rightarrow \phi(S(x)))] \rightarrow \forall x \phi(x) 형태인지“를 기호열 분석으로 수행한다.
4.3 전체 공리 판별
\text{Axiom}(a) = \text{LogAx}(a) \vee \text{PAx}(a)
추론 규칙 적용의 검사
전건 긍정(Modus Ponens)
“공식 c가 공식 a와 공식 b로부터 전건 긍정에 의해 도출되었는가?”
\text{MP}(a, b, c) \equiv (b = \text{imp}(a, c))
여기서 \text{imp}(a, c)는 a \rightarrow c의 괴델 수를 구성하는 함수이다. 이 함수는 연결(Concatenation)에 의해 원시 재귀적으로 정의된다.
4.4 전칭 일반화(Universal Generalization)
“공식 b가 공식 a로부터 전칭 일반화에 의해 도출되었는가?”
\text{Gen}(a, b) \equiv \exists i \leq b \, [b = \text{univ}(i, a)]
여기서 \text{univ}(i, a)는 \forall x_i \, a의 괴델 수를 구성하는 함수이다.
증명 관계의 원시 재귀적 정의
위의 모든 구성 요소를 결합하여 증명 관계 \text{Proof}(m, n)을 정의한다:
\text{Proof}(m, n) \equiv \text{Seq}(m) \wedge \text{last}(m) = n \wedge \forall i \leq \text{len}(m) \, \text{ValidStep}(m, i)
여기서:
- \text{Seq}(m): m이 유효한 공식 열의 괴델 수인지
- \text{last}(m): 열의 마지막 원소의 괴델 수
- \text{ValidStep}(m, i): 열의 i번째 원소가 공리이거나, 앞선 원소들로부터 추론 규칙에 의해 올바르게 도출되었는지
\text{ValidStep}(m, i) \equiv \text{Axiom}(\text{exp}(m, i)) \vee \exists j, k < i \, [\text{MP}(\text{exp}(m, j), \text{exp}(m, k), \text{exp}(m, i))] \vee \exists j < i \, [\text{Gen}(\text{exp}(m, j), \text{exp}(m, i))]
모든 양화가 제한 양화(Bounded Quantification)이므로, \text{Proof}(m, n)은 원시 재귀적 관계이다.
PA에서의 표현 가능성
원시 재귀적 관계가 PA에서 표현 가능(Representable)하다는 것은 다음을 의미한다:
원시 재귀적 관계 R(\vec{x})에 대해 PA의 공식 \phi_R(\vec{x})가 존재하여:
- R(\vec{a})가 참이면 PA \vdash \phi_R(\vec{\overline{a}})
- R(\vec{a})가 거짓이면 PA \vdash \neg\phi_R(\vec{\overline{a}})
이 표현 가능성에 의해, \text{Proof}(m, n)이 PA의 공식 \text{Prf}(m, n)으로 표현되고, 증명 가능성 술어 \text{Prov}(n) = \exists m \, \text{Prf}(m, n)이 PA 내에서 정의된다. 이것이 괴델 문장 구성의 직접적 기반이다.