5.19 힐베르트 프로그램의 좌절과 수리논리학에 미친 영향

1. 힐베르트 프로그램의 좌절

1.1 세 목표의 실패

힐베르트 프로그램의 세 가지 핵심 목표가 괴델과 튜링-처치의 결과에 의해 달성 불가능한 것으로 확정되었다.

완전성의 좌절(1931): 괴델의 제1 불완전성 정리에 의해, 페아노 산술을 포함하는 무모순 형식 체계에서 증명도 반증도 불가능한 참인 문장이 존재한다. 수학의 완전한 형식화는 원리적으로 불가능하다.

무모순성 증명의 좌절(1931): 괴델의 제2 불완전성 정리에 의해, 충분히 강력한 무모순 형식 체계는 자기 자신의 무모순성을 증명할 수 없다. 유한적 방법에 의한 무모순성 증명이라는 힐베르트의 목표는 달성 불가능하다.

결정 가능성의 좌절(1936): 처치와 튜링의 결과에 의해, 일차 술어 논리의 타당성 문제(판정 문제)는 결정 불가능하다. 수학적 명제의 증명 가능성을 기계적으로 판정하는 일반적 알고리즘은 존재하지 않는다.

1.2 힐베르트의 반응

힐베르트가 괴델의 결과에 대해 어떻게 반응하였는지는 역사적으로 완전히 명확하지 않다. 일부 증언에 따르면 힐베르트는 처음에 분노하였으나(“화가 났다”), 이후 결과의 타당성을 수용하였다. 힐베르트는 1931년 이후에도 증명 이론(Proof Theory) 연구를 계속하였으며, 프로그램의 완전한 포기가 아닌 수정과 약화를 추구하였다.

2. 불완전성 정리 이후의 수리논리학 발전

2.1 증명 이론(Proof Theory)

괴델의 결과는 증명 이론의 연구 방향을 근본적으로 재정립하였다.

겐첸의 무모순성 증명(1936): 겐첸(Gerhard Gentzen)은 PA의 무모순성을 초한 귀납법(Transfinite Induction up to \epsilon_0)을 사용하여 증명하였다. 이 증명은 PA 내부가 아닌 더 강력한 원리를 사용하므로 제2 불완전성 정리에 모순되지 않는다. 겐첸의 결과는 형식 체계의 무모순성이 “증명 불가능“이 아니라 “체계 내부에서 증명 불가능“이라는 정밀한 구분을 예시하였다.

서수 분석(Ordinal Analysis): 겐첸에 의해 시작된 서수 분석 프로그램은 형식 체계의 “증명론적 강도(Proof-Theoretic Strength)“를 서수(Ordinal)로 측정하는 연구 프로그램이다. PA의 증명론적 서수는 \epsilon_0이며, 보다 강력한 체계는 보다 큰 서수를 갖는다.

자연 연역(Natural Deduction)과 시퀀트 계산(Sequent Calculus): 겐첸은 불완전성 정리 연구와 병행하여 자연 연역 체계와 시퀀트 계산을 개발하였다. 이 체계들은 현대 증명 이론과 프로그래밍 언어 이론의 기반이 되었다.

2.2 모형 이론(Model Theory)

괴델의 완전성 정리(1929)와 불완전성 정리(1931)는 모형 이론의 발전을 촉진하였다.

비표준 모형: 불완전성 정리에 의해 PA에서 결정 불가능한 문장이 존재하므로, PA와 양립 가능한 상이한 모형(표준 모형과 비표준 모형)이 존재한다. 이 관찰이 비표준 분석(Nonstandard Analysis, Robinson 1966)의 기반이 되었다.

콤팩트성 정리(Compactness Theorem): 괴델의 완전성 정리의 귀결인 콤팩트성 정리는 모형 이론의 핵심 도구가 되었다.

2.3 계산 이론(Computability Theory)

불완전성 정리는 계산 이론의 탄생에 직접적 동기를 제공하였다.

튜링 기계(1936): 튜링은 괴델의 불완전성 정리에 영감을 받아, “효과적 계산 가능성“의 형식적 정의와 판정 문제의 결정 불가능성 증명에 도달하였다.

재귀 함수 이론: 괴델의 원시 재귀 함수 개념이 클레이니에 의해 재귀 함수 이론으로 체계화되었다.

2.4 집합론(Set Theory)

연속체 가설의 독립성: 괴델은 1940년 연속체 가설(Continuum Hypothesis, CH)이 ZFC와 무모순함을 증명하였고, 코헨(Paul Cohen)은 1963년 \negCH도 ZFC와 무모순함을 증명하였다. 이에 의해 CH는 ZFC에서 독립(Independent)이다. 이 결과는 불완전성 현상의 집합론적 실현이다.

3. 수학 기초론의 재편

3.1 형식주의의 수정

불완전성 정리 이후, 형식주의는 “수학의 완전한 형식화“라는 강한 목표를 포기하고, “부분적이지만 유용한 형식화“를 추구하는 실용적 형식주의로 수정되었다.

3.2 직관주의와 구성적 수학

불완전성 정리는 직관주의(Intuitionism)에도 적용된다. 하이팅 산술(Heyting Arithmetic)도 PA의 공리를 포함하므로 불완전하다. 그러나 직관주의는 형식 체계에 환원되지 않는 수학적 직관을 인정하므로, 불완전성 정리의 영향이 형식주의에 비해 덜 치명적이다.

3.3 큰 기수 공리(Large Cardinal Axioms)

ZFC의 불완전성을 “해소“하기 위해 새로운 공리(큰 기수 공리)를 추가하는 연구 프로그램이 발전하였다. 도달 불가능 기수(Inaccessible Cardinal), 가측 기수(Measurable Cardinal), 초컴팩트 기수(Supercompact Cardinal) 등의 공리가 제안되었다. 그러나 불완전성 정리에 의해, 어떤 공리 추가에 의해서도 불완전성은 완전히 해소되지 않는다.

4. 컴퓨터 과학에 미친 영향

4.1 자동 정리 증명

불완전성 정리는 자동 정리 증명(Automated Theorem Proving)의 원리적 한계를 규정하면서도, 그 실용적 가능성을 부정하지 않는다. 불완전성은 모든 참인 정리를 자동으로 증명하는 것이 불가능하다는 것이지, 특정 정리의 자동 증명이 불가능하다는 것은 아니다.

4.2 프로그래밍 언어와 유형 이론

커리-하워드 대응(Curry-Howard Correspondence)에 의해, 형식적 증명과 프로그래밍 언어의 유형(Type)이 구조적으로 대응한다. 불완전성 정리는 이 대응을 통해 프로그래밍 언어의 표현력 한계로 번역된다.

4.3 AI와 기계 학습

불완전성 정리가 AI의 원리적 한계를 규정하는지에 관한 논쟁은 루카스(1961), 펜로즈(1989, 1994), 그리고 이에 대한 반론(퍼트남, 체이틴 등)에 의해 지속되고 있다.

5. 힐베르트 프로그램의 현대적 유산

힐베르트 프로그램은 원래 목표의 달성에 실패하였으나, 이 프로그램이 촉발한 연구가 현대 수학과 컴퓨터 과학의 핵심 분야를 형성하였다. 증명 이론, 모형 이론, 계산 이론, 집합론, 프로그래밍 언어 이론, 형식 검증은 모두 힐베르트 프로그램의 직접적 또는 간접적 후속 연구에서 발전하였다.

“실패한 프로그램이 가장 성공한 프로그램이었다“는 역설적 평가가 힐베르트 프로그램의 학문사적 위상을 적절히 요약한다.