1.20 힐베르트 프로그램과 수학의 완전성 추구

1. 다비트 힐베르트의 형식주의

다비트 힐베르트(David Hilbert, 1862–1943)는 괴팅겐(Göttingen) 대학교의 수학 교수로서, 20세기 초 수학의 기초론(Foundations of Mathematics) 논쟁에서 형식주의(Formalism) 입장을 대표한 인물이다. 힐베르트는 수학을 형식 체계(Formal System)로 구축하고, 그 체계의 무모순성(Consistency)을 유한한 방법(Finitary Methods)으로 증명함으로써 수학의 확실한 기초를 확보하고자 하였다.

힐베르트의 형식주의는 직관주의(Intuitionism)와 논리주의(Logicism)에 대한 대안으로 제시되었다. 브라우어(L.E.J. Brouwer)가 이끄는 직관주의는 배중률(Law of Excluded Middle)의 무제한적 사용을 거부하여 고전 수학의 상당 부분을 포기할 것을 요구하였다. 힐베르트는 이를 “수학자에게서 배중률을 빼앗는 것은 권투 선수에게서 주먹 사용을 금지하는 것과 같다“고 비판하며, 고전 수학의 방법론적 정당성을 형식적으로 확보하는 방법을 추구하였다.

2. 힐베르트 프로그램의 핵심 목표

힐베르트 프로그램(Hilbert’s Program)은 1920년대에 힐베르트가 제안한 수학 기초론의 연구 프로그램으로, 다음의 목표를 추구하였다.

2.1 수학의 완전한 형식화

수학의 모든 분야를 형식 체계로 구축한다. 즉, 수학적 개념을 형식 언어의 기호로, 수학적 공리를 형식적 공리로, 수학적 증명을 형식적 도출로 변환하여, 수학 전체를 기호의 기계적 조작 체계로 재구성한다.

2.2 완전성(Completeness)의 증명

형식화된 수학 체계가 완전함을 증명한다. 즉, 체계의 형식 언어로 표현 가능한 모든 참인 수학적 명제가 공리로부터 도출 가능함을 증명한다.

2.3 무모순성(Consistency)의 증명

형식화된 수학 체계가 무모순함을 증명한다. 즉, 어떤 명제 \phi에 대해서도 \phi와 \neg \phi가 동시에 도출되지 않음을 증명한다. 힐베르트는 이 증명이 유한적 방법(Finitary Methods)으로 수행되어야 한다고 요구하였다. 유한적 방법이란 무한 대상에 대한 존재 가정 없이, 유한 개의 기호에 대한 구체적·조합론적 조작만을 사용하는 방법이다.

2.4 결정 가능성(Decidability)의 확인

형식화된 수학 체계에 대해 결정 절차(Decision Procedure)가 존재하는지 확인한다. 이 결정 절차는 임의의 수학적 명제가 주어졌을 때, 유한 단계 내에 그 명제의 증명 가능성 또는 반증 가능성을 판정하는 알고리즘이다. 이 문제는 판정 문제(Entscheidungsproblem)로 알려져 있다.

3. 힐베르트의 23가지 문제와 형식주의

힐베르트는 1900년 파리 국제 수학자 대회(International Congress of Mathematicians)에서 20세기 수학이 해결해야 할 23가지 문제를 제시하였다. 이 중 제2문제가 산술 공리의 무모순성 증명이었으며, 이는 힐베르트 프로그램의 핵심 목표와 직접 연결된다.

4. 메타수학(Metamathematics)의 확립

힐베르트 프로그램의 방법론적 혁신은 메타수학(Metamathematics)의 확립이다. 메타수학은 수학적 형식 체계 자체를 수학적 연구의 대상으로 삼는 학문이다. 형식 체계 내에서 수학적 정리를 증명하는 것과 형식 체계에 관한 성질(무모순성, 완전성 등)을 증명하는 것은 서로 다른 수준의 활동이며, 후자가 메타수학의 영역이다.

힐베르트의 증명 이론(Proof Theory)은 메타수학의 핵심 분야로서, 형식적 증명을 구문론적 대상으로 취급하고, 증명의 존재, 길이, 구조 등에 관한 수학적 정리를 도출한다.

5. 괴델의 불완전성 정리에 의한 프로그램의 좌절

힐베르트 프로그램의 핵심 목표는 1931년 괴델의 두 불완전성 정리에 의해 근본적으로 좌절되었다.

5.1 제1 불완전성 정리

페아노 산술을 포함하는 임의의 무모순 형식 체계 \mathcal{F}에 대해, \mathcal{F}의 언어로 표현 가능하지만 \mathcal{F} 내에서 증명도 반증도 불가능한 참인 문장이 존재한다.

이 결과는 힐베르트 프로그램의 완전성 목표가 달성 불가능함을 의미한다.

5.2 제2 불완전성 정리

페아노 산술을 포함하는 임의의 무모순 형식 체계 \mathcal{F}는 자기 자신의 무모순성을 증명할 수 없다.

이 결과는 힐베르트 프로그램의 무모순성 증명 목표가 달성 불가능함을 의미한다. 체계 \mathcal{F}의 무모순성을 증명하려면 \mathcal{F}보다 강력한 체계가 필요하며, 그 강력한 체계의 무모순성은 다시 더 강력한 체계를 요구하여 무한 후퇴(Infinite Regress)가 발생한다.

5.3 판정 문제의 부정적 해결

1936년 처치(Alonzo Church)와 튜링(Alan Turing)은 독립적으로 판정 문제가 일반적으로 해결 불가능함을 증명하였다. 일차 술어 논리의 정리 여부를 판정하는 일반적 알고리즘은 존재하지 않는다.

6. 힐베르트 프로그램의 유산

괴델의 결과에도 불구하고, 힐베르트 프로그램은 현대 수학과 컴퓨터 과학에 지대한 유산을 남겼다.

첫째, 형식 체계의 개념 자체가 계산 이론(Theory of Computation)의 직접적 토대가 되었다. 튜링이 판정 문제를 해결하기 위해 도입한 튜링 기계(Turing Machine)는 형식 체계의 기계적 성격을 엄밀하게 모델링한 것이며, 이 모델이 현대 컴퓨터의 이론적 원형이다.

둘째, 증명 이론은 프로그래밍 언어 이론(Programming Language Theory)과 깊이 연결된다. 커리-하워드 대응(Curry-Howard Correspondence)은 형식적 증명과 컴퓨터 프로그램 사이의 구조적 동형성을 확립하며, “명제는 유형이고, 증명은 프로그램이다“라는 원리를 제시한다.

셋째, 형식 검증(Formal Verification)과 자동 정리 증명(Automated Theorem Proving)은 힐베르트 프로그램의 기계화 이상을 컴퓨터를 통해 부분적으로 실현한 것이다. 소프트웨어와 하드웨어의 정확성을 형식적으로 검증하는 현대의 형식 방법론(Formal Methods)은 힐베르트의 형식주의 전통을 직접적으로 계승한다.

힐베르트 프로그램은 그 최초의 목표가 실현 불가능함이 증명되었음에도, 형식적 방법론의 가능성과 한계를 동시에 규명하는 과정에서 현대 수학, 논리학, 컴퓨터 과학의 가장 심원한 결과들을 산출하였다.