1.19 형식 체계(Formal System)의 공리, 추론 규칙, 정리의 구조

1. 형식 체계의 정의

형식 체계(Formal System)는 기호의 형식적 조작에 의해 정리(Theorem)를 도출하는 수학적 체계이다. 형식 체계는 의미(Semantics)에 대한 참조 없이 순전히 구문적(Syntactic) 규칙에 의해 정의되며, 이는 추론의 기계화 가능성을 보장하는 핵심 조건이다.

형식 체계 \mathcal{F}는 다음의 네 구성 요소로 정의된다:

1. 형식 언어(Formal Language) \mathcal{L}: 기호의 알파벳과 적격식(Well-Formed Formula, WFF)을 생성하는 형성 규칙의 집합
2. 공리(Axioms) \mathcal{A}: 증명 없이 참으로 받아들여지는 적격식의 집합
3. 추론 규칙(Rules of Inference) \mathcal{R}: 기존 적격식으로부터 새로운 적격식을 도출하는 변환 규칙의 집합
4. 정리(Theorems) \mathcal{T}: 공리로부터 추론 규칙의 유한 번 적용에 의해 도출 가능한 적격식의 집합

2. 형식 언어의 구조

형식 언어 \mathcal{L}은 다음의 두 요소로 구성된다.

2.1 알파벳(Alphabet)

알파벳은 체계에서 사용되는 기호의 유한 집합이다. 전형적으로 다음의 범주로 분류된다:

• 변수 기호(Variable Symbols): x, y, z, \ldots
• 상수 기호(Constant Symbols): a, b, c, \ldots, 0, 1, \ldots
• 연산 기호(Operation Symbols): +, \times, f, g, \ldots
• 관계 기호(Relation Symbols): =, <, P, Q, R, \ldots
• 논리 기호(Logical Symbols): \neg, \wedge, \vee, \rightarrow, \forall, \exists
• 보조 기호(Auxiliary Symbols): (, ), ,

2.2 형성 규칙(Formation Rules)

형성 규칙은 알파벳의 기호를 결합하여 적격식을 구성하는 재귀적 규칙이다. 적격식은 형성 규칙에 의해 생성된 기호열만을 포함하며, 형성 규칙에 의해 생성되지 않은 기호열은 적격식이 아니다. 형성 규칙은 형식 언어의 문법(Grammar)에 해당한다.

3. 공리(Axioms)

공리는 형식 체계에서 증명의 출발점이 되는 적격식이다. 공리는 증명 없이 참으로 수용되며, 다른 모든 정리는 공리로부터 도출된다.

3.1 공리의 유형

논리적 공리(Logical Axioms): 논리적 연결사와 양화사의 기본 성질을 규정하는 공리이다. 이 공리는 형식 체계의 특정 주제(산술, 기하학 등)에 독립적이며, 모든 형식 체계에 공통적으로 적용된다.

명제 논리의 전형적 논리 공리 도식(Axiom Schema):

• \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)

여기서 \phi, \psi, \chi는 임의의 적격식에 대한 메타변수(Metavariable)이다.

비논리적 공리(Non-Logical Axioms): 특정 수학적 이론의 구체적 성질을 규정하는 공리이다. 예를 들어, 페아노 산술의 공리:

• \forall x \, \neg(S(x) = 0) (0은 어떤 자연수의 후자도 아니다)
• \forall x \, \forall y \, (S(x) = S(y) \rightarrow x = y) (후자 함수는 단사이다)
• 수학적 귀납법 공리 도식

3.2 공리 도식(Axiom Schema)

공리 도식은 무한히 많은 공리를 유한하게 기술하는 방법이다. 도식은 메타변수를 포함하는 패턴이며, 메타변수에 임의의 적격식을 대입하면 하나의 공리가 된다.

3.3 공리가 만족해야 할 조건

이상적으로, 공리 체계는 다음의 조건을 만족해야 한다:

1. 무모순성(Consistency): 공리로부터 모순(\phi와 \neg \phi가 동시에 도출)이 발생하지 않아야 한다.
2. 독립성(Independence): 각 공리는 나머지 공리들로부터 도출 불가능해야 한다.
3. 완전성(Completeness): 의도된 해석에서 참인 모든 문장이 공리로부터 도출 가능해야 한다.

괴델의 불완전성 정리에 의해, 자연수 산술을 포함하는 충분히 강력한 무모순 형식 체계에서 완전성은 달성 불가능함이 증명되었다.

4. 추론 규칙(Rules of Inference)

추론 규칙은 하나 이상의 적격식(전제, Premise)으로부터 새로운 적격식(결론, Conclusion)을 도출하는 형식적 변환 규칙이다.

4.1 추론 규칙의 형식

추론 규칙은 일반적으로 다음과 같이 표기된다:

\frac{\phi_1, \phi_2, \ldots, \phi_n}{\psi}

가로선 위의 \phi_1, \ldots, \phi_n이 전제이고, 가로선 아래의 \psi가 결론이다.

주요 추론 규칙

전건 긍정(Modus Ponens, MP): 가장 기본적이고 보편적인 추론 규칙이다.

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

전칭 일반화(Universal Generalization, UG):

\frac{\phi(x)}{\forall x \, \phi(x)}

(x가 \phi의 도출에 사용된 가정에 자유롭게 나타나지 않을 때)

전칭 예화(Universal Instantiation, UI):

\frac{\forall x \, \phi(x)}{\phi(t)}

(t가 x에 대해 \phi에서 자유로운 항일 때)

4.2 추론 규칙의 건전성

추론 규칙은 건전(Sound)해야 한다. 규칙이 건전하다 함은, 전제가 모두 참인 모든 해석에서 결론도 참이라는 것이다. 건전성은 추론 규칙이 거짓을 도출하지 않음을 보장한다.

5. 증명(Proof)과 정리(Theorem)

5.1 증명의 정의

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

1. \phi_i는 공리이다.
2. \phi_i는 열에서 앞선 적격식들에 추론 규칙을 적용하여 도출된 것이다.

5.2 정리의 정의

형식 체계 \mathcal{F}에서 증명이 존재하는 적격식을 정리(Theorem)라 한다. 이를 \mathcal{F} \vdash \phi로 표기하며, “\phi는 \mathcal{F}에서 증명 가능하다“로 읽는다.

기호 \vdash(턴스타일, Turnstile)은 구문론적 도출 가능성(Syntactic Derivability)을 나타내며, 의미론적 귀결(Semantic Entailment)을 나타내는 \models(더블 턴스타일)과 구별된다.

6. 건전성과 완전성

6.1 건전성(Soundness)

형식 체계 \mathcal{F}가 건전하다 함은, \mathcal{F}에서 증명 가능한 모든 적격식이 의미론적으로도 참이라는 것이다:

\mathcal{F} \vdash \phi \implies \models \phi

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

완전성(Completeness)

형식 체계 \mathcal{F}가 완전하다 함은, 의미론적으로 참인 모든 적격식이 \mathcal{F}에서 증명 가능하다는 것이다:

\models \phi \implies \mathcal{F} \vdash \phi

완전성은 형식 체계가 모든 진리를 포착함을 보장한다.

괴델은 1929년 박사 학위 논문에서 일차 술어 논리의 완전성 정리(Completeness Theorem)를 증명하였다: 일차 술어 논리의 표준적 공리화는 건전하고 완전하다. 그러나 1931년의 불완전성 정리에서 페아노 산술을 포함하는 형식 체계는 (무모순이라면) 완전할 수 없음을 증명하였다.

7. 형식 체계의 메타 이론(Metatheory)

형식 체계 자체에 관한 수학적 연구를 메타 이론(Metatheory) 또는 메타 수학(Metamathematics)이라 한다. 메타 이론에서 다루는 주요 문제는 다음과 같다:

• 무모순성: 체계가 모순을 도출하지 않는가?
• 완전성: 체계가 모든 참인 문장을 도출할 수 있는가?
• 결정 가능성(Decidability): 임의의 문장이 정리인지 아닌지를 판정하는 알고리즘이 존재하는가?

이 세 문제에 대한 답변—괴델의 불완전성 정리, 처치와 튜링의 결정 불가능성 결과—이 현대 수리논리학과 계산 이론의 핵심 성과를 구성하며, 인공지능의 이론적 가능성과 한계를 규정하는 근본적 결과이다.