5.3 형식 체계(Formal System)의 구성 요소와 공리적 방법

1. 형식 체계의 정의

형식 체계(Formal System)는 기호의 형식적 조작에 의해 수학적 정리를 도출하는 엄밀한 체계이다. 형식 체계는 자연 언어의 모호성을 배제하고, 추론의 각 단계가 기호의 형태만으로 결정되는 순수 구문적(Syntactic) 체계로 구성된다.

괴델의 불완전성 정리는 특정 조건을 만족하는 형식 체계에 관한 결과이므로, 형식 체계의 정밀한 정의가 정리의 이해에 선행되어야 한다.

형식 언어 $\mathcal{L}$ 은 체계에서 사용되는 기호의 알파벳(Alphabet)과 적격식(Well-Formed Formula, WFF)을 생성하는 형성 규칙(Formation Rules)으로 구성된다.

알파벳의 구성:

형성 규칙: 적격식을 귀납적으로 정의한다.

항(Term): 변수, $0$ , $S(t)$ , $t_1 + t_2$ , $t_1 \times t_2$ (여기서 $t, t_1, t_2$ 는 항)
원자식(Atomic Formula): $t_1 = t_2$ (여기서 $t_1, t_2$ 는 항)
공식(Formula): 원자식, $\neg \phi$ , $\phi \rightarrow \psi$ , $\forall x \, \phi$ (여기서 $\phi, \psi$ 는 공식, $x$ 는 변수)

공리는 증명 없이 참으로 수용되는 적격식의 집합이다. 불완전성 정리의 맥락에서 공리는 두 종류로 구분된다.

논리적 공리(Logical Axioms): 순수 논리의 기본 진리를 표현한다. 전형적 논리 공리 도식:

$\phi \rightarrow (\psi \rightarrow \phi)$
$(\phi \rightarrow (\psi \rightarrow \chi)) \rightarrow ((\phi \rightarrow \psi) \rightarrow (\phi \rightarrow \chi))$
$(\neg \psi \rightarrow \neg \phi) \rightarrow (\phi \rightarrow \psi)$
양화사 관련 공리

비논리적 공리(Non-Logical Axioms, 수학적 공리): 특정 수학 이론의 내용을 규정한다. 페아노 산술(Peano Arithmetic, PA)의 공리:

$\forall x \, \neg(S(x) = 0)$ (0은 어떤 수의 후자도 아니다)
$\forall x \, \forall y \, (S(x) = S(y) \rightarrow x = y)$ (후자 함수는 단사이다)
$\forall x \, (x + 0 = x)$ , $\forall x \, \forall y \, (x + S(y) = S(x + y))$ (덧셈의 재귀 정의)
$\forall x \, (x \times 0 = 0)$ , $\forall x \, \forall y \, (x \times S(y) = x \times y + x)$ (곱셈의 재귀 정의)
수학적 귀납법 공리 도식: $[\phi(0) \wedge \forall x \, (\phi(x) \rightarrow \phi(S(x)))] \rightarrow \forall x \, \phi(x)$ (모든 공식 $\phi$ 에 대해)

형식적 도출(Formal Derivation)에서 기존 공식으로부터 새로운 공식을 산출하는 변환 규칙이다.

전건 긍정(Modus Ponens): $\phi$ 와 $\phi \rightarrow \psi$ 로부터 $\psi$ 를 도출한다.

$\frac{\phi, \quad \phi \rightarrow \psi}{\psi}$

전칭 일반화(Universal Generalization): 공식 $\phi(x)$ 가 $x$ 에 대한 가정 없이 도출되었으면, $\forall x \, \phi(x)$ 를 도출한다.

정리는 공리로부터 추론 규칙의 유한 번 적용에 의해 도출 가능한 적격식이다.

$\mathcal{F} \vdash \phi$ : $\phi$ 는 형식 체계 $\mathcal{F}$ 의 정리이다.

공리적 방법은 소수의 기본 진리(공리)로부터 논리적 추론에 의해 체계적으로 새로운 진리(정리)를 도출하는 수학적 방법론이다. 유클리드의 『원론(Elements)』에서 기원하여, 힐베르트의 형식주의에 의해 현대적 형태로 정립되었다.

괴델의 불완전성 정리가 밝힌 공리적 방법의 근본적 한계:

불완전성: 충분히 강력한 무모순 형식 체계에서 참이지만 증명 불가능한 명제가 존재한다. 공리의 추가에 의해 이를 해결하려 하면, 새로운 결정 불가능 명제가 발생한다.
자기 정당화의 불가능성: 형식 체계가 자기 자신의 무모순성을 증명할 수 없다. 체계의 신뢰성은 체계 외부에서 확보되어야 한다.

괴델의 불완전성 정리가 적용되기 위해 형식 체계 $\mathcal{F}$ 가 만족해야 하는 조건:

효과적 공리화(Effective Axiomatization): 공리의 집합이 결정 가능(Decidable)하다. 즉, 주어진 공식이 공리인지 아닌지를 알고리즘적으로 판별할 수 있다.
무모순성(Consistency): $\mathcal{F}$ 가 무모순하다.
충분한 표현력: $\mathcal{F}$ 가 페아노 산술(또는 로빈슨 산술 Q)을 포함한다. 즉, 자연수의 기본 산술을 표현할 수 있을 만큼 강력하다.

조건 3이 핵심적이다. 산술의 표현력이 자기 참조적 구성(괴델 문장)을 가능하게 하며, 이것이 불완전성의 원천이다. 산술을 포함하지 않는 약한 형식 체계(예: 프레스버거 산술)에서는 불완전성이 발생하지 않을 수 있다.