5.5 형식 언어에서의 논리식 구성과 증명 개념

1. 형식 언어에서의 논리식 구성

1.1 항(Term)의 귀납적 정의

페아노 산술의 형식 언어에서 항(Term)은 자연수를 나타내는 표현이며, 다음과 같이 귀납적으로 정의된다:

$0$ 은 항이다.
변수 $x_i$ 는 항이다.
$t$ 가 항이면 $S(t)$ 는 항이다.
$t_1$ 과 $t_2$ 가 항이면 $(t_1 + t_2)$ 와 $(t_1 \times t_2)$ 는 항이다.
위 규칙에 의해 구성된 것만이 항이다.

1.2 원자식(Atomic Formula)

$t_1$ 과 $t_2$ 가 항이면, $t_1 = t_2$ 는 원자식이다. 원자식은 두 항의 동등성을 주장하는 가장 기본적인 명제적 표현이다.

1.3 공식(Formula, WFF)의 귀납적 정의

원자식은 공식이다.
$\phi$ 가 공식이면 $\neg \phi$ 는 공식이다.
$\phi$ 와 $\psi$ 가 공식이면 $(\phi \rightarrow \psi)$ 는 공식이다.
$\phi$ 가 공식이고 $x_i$ 가 변수이면 $\forall x_i \, \phi$ 는 공식이다.
위 규칙에 의해 구성된 것만이 공식이다.

1.4 파생 연결사(Derived Connectives)

기본 연결사 $\neg, \rightarrow, \forall$ 로부터 다른 연결사를 정의한다:

$\phi \vee \psi \equiv \neg \phi \rightarrow \psi$ (논리합)
$\phi \wedge \psi \equiv \neg(\phi \rightarrow \neg \psi)$ (논리곱)
$\phi \leftrightarrow \psi \equiv (\phi \rightarrow \psi) \wedge (\psi \rightarrow \phi)$ (쌍조건)
$\exists x \, \phi \equiv \neg \forall x \, \neg \phi$ (존재 양화)

1.5 문장(Sentence)

자유 변수(Free Variable)가 없는 공식을 문장(Sentence) 또는 폐쇄식(Closed Formula)이라 한다. 문장은 진리값을 가지며, 형식 체계에서 증명의 대상이 된다.

2. 증명(Proof)의 형식적 정의

2.1 형식적 증명(Formal Proof)

형식 체계 $\mathcal{F}$ 에서 문장 $\phi$ 의 형식적 증명은 공식의 유한 열(Finite Sequence) $\phi_1, \phi_2, \ldots, \phi_n$ 으로서, $\phi_n = \phi$ 이고, 각 $\phi_i$ 는 다음 중 하나를 만족한다:

$\phi_i$ 는 $\mathcal{F}$ 의 공리(논리적 또는 비논리적)이다.
$\phi_i$ 는 열에서 앞선 공식들에 추론 규칙(전건 긍정 또는 전칭 일반화)을 적용하여 도출된 것이다.

2.2 증명 가능성(Provability)

문장 $\phi$ 가 $\mathcal{F}$ 에서 증명 가능(Provable)하다 함은, $\phi$ 의 형식적 증명이 존재함을 의미한다. 이를 $\mathcal{F} \vdash \phi$ 로 표기한다.

2.3 증명의 기계적 검증 가능성

형식적 증명의 각 단계가 공리인지, 추론 규칙의 올바른 적용인지를 기계적으로(알고리즘적으로) 검증할 수 있다. 이 검증 가능성이 형식적 증명의 핵심 장점이다.

그러나 증명의 존재 여부를 판별하는 것—즉 주어진 문장이 증명 가능한지를 판정하는 것—은 일반적으로 결정 불가능하다. 이는 “증명을 검증하는 것“과 “증명을 발견하는 것“의 난이도가 근본적으로 상이함을 보여준다.

3. 증명 관련 핵심 메타수학적 개념

3.1 건전성(Soundness)

형식 체계 $\mathcal{F}$ 가 건전(Sound)하다 함은, $\mathcal{F}$ 에서 증명 가능한 모든 문장이 참(표준 모형에서)이라는 것이다:

$\mathcal{F} \vdash \phi \implies \mathbb{N} \models \phi$

건전성은 형식 체계가 거짓을 증명하지 않음을 보장한다.

무모순성(Consistency)

$\mathcal{F}$ 가 무모순(Consistent)하다 함은, 어떤 문장 $\phi$ 에 대해서도 $\mathcal{F} \vdash \phi$ 와 $\mathcal{F} \vdash \neg \phi$ 가 동시에 성립하지 않음을 의미한다.

건전성은 무모순성을 함의한다: $\mathcal{F}$ 가 건전하면 $\mathcal{F}$ 는 무모순하다. 역은 일반적으로 성립하지 않는다.

완전성(Completeness)

$\mathcal{F}$ 가 완전(Complete)하다 함은, $\mathcal{F}$ 의 언어로 표현 가능한 모든 문장 $\phi$ 에 대해 $\mathcal{F} \vdash \phi$ 또는 $\mathcal{F} \vdash \neg \phi$ 가 성립함을 의미한다.

괴델의 불완전성 정리는 PA가 완전하지 않음을 증명한다—PA에서 증명도 반증도 불가능한 문장이 존재한다.

증명의 산술적 표현

괴델의 불완전성 정리 증명에서 핵심적인 단계는 “증명” 개념 자체를 PA의 언어로 표현하는 것이다.

증명 관계의 산술적 부호화

괴델 수 부호화에 의해, 공식의 유한 열(즉, 증명 후보)이 자연수로 부호화된다. “ $m$ 이 공식 $n$ 의 증명의 괴델 수이다“라는 메타수학적 관계가 PA의 공식 $\text{Proof}(m, n)$ 으로 표현된다.

$\text{Proof}(m, n)$ 는 원시 재귀적 관계이므로, PA 내에서 $\Delta_0$ 공식으로 표현 가능하다.

증명 가능성 술어(Provability Predicate)

$\text{Prov}(n) \equiv \exists m \, \text{Proof}(m, n)$

$\text{Prov}(\ulcorner \phi \urcorner)$ 는 “공식 $\phi$ 가 PA에서 증명 가능하다“를 PA의 언어로 표현한 것이다. 이 술어가 괴델 문장의 구성에서 핵심적 역할을 한다.

4. 논리식 구성과 증명 개념의 이론적 위상

형식 언어에서의 논리식 구성과 증명 개념의 정밀한 형식화는 괴델 증명의 전제 조건이다. 논리식이 기호의 유한 열로 정의되고, 증명이 공식의 유한 열로 정의되며, 이 모든 구문론적 대상이 자연수로 부호화 가능하다는 사실이 “수학이 자기 자신에 관해 말할 수 있다“는 자기 참조 가능성의 기반이다. 이 자기 참조 가능성이 불완전성 정리의 핵심 메커니즘이다.