증명 이론

수리논리학에서 증명 이론(證明理論, 영어: proof theory)은 증명을 형식적인 수학적 개체로 표상하여 수학적 기법으로 이용하여 증명을 객관적으로 분석하는 이론이다.

증명은 귀납적으로 정의된 자료구조로 표현되는데, 이는 어떠한 이론체계의 공리와 추론 규칙에 따라 구성된다. 즉 모형이론에 의미론적 성질이 있는 데 대조적으로 증명 이론에는 구문론적 성질이 있다. 모형 이론, 집합론, 재귀 이론과 함께 증명 이론은 수학기초론의 4대 기둥이라고도 불린다.

역사

초기의 수리논리학을 발전시킨 고틀로프 프레게, 주세페 페아노, 버트런드 러셀, 리하르트 데데킨트 등의 논리학자들의 연구가 증명 이론의 성립의 바탕이 되었으며, 이후 수학의 형식화 방안을 모색한 다비트 힐베르트의 힐베르트 프로그램(Hilbert's program)이 현대 증명 이론의 효시가 되었다고 평가받는다. 쿠르트 괴델이 발표한 완전성 정리가 1차 논리의 완전성을 보이면서 모든 수학을 1가지의 유한적 형식 체계로 환원하려는 힐베르트의 목적에 희망을 주는 듯 하였으나, 이후 발표된 불완전성 정리에 의해 산술 체계로부터 나온 공리계의 무모순성을 증명할 수 없음이 증명되면서 힐베르트의 목적은 불가능한 것으로 판명되었다. 이들 연구는 힐베르트 체계(Hilbert system)이라는 증명계산 상에서 이루어졌다.

힐베르트 프로그램의 흥망과 병행하여 구조적 증명 이론(structural proof theory)의 기초도 세워지고 있었는데, 1926년 얀 우카시에비치(Jan Łukasiewicz)가 논리의 추론 규칙에 따라 전제로부터 결론을 도출하는 것을 허용한다면 힐베르트 체계를 논리의 공리적 방식의 기초로써 발전시킬 수 있으리라고 제안하였고, 이에 스타니스와프 야시코프스키(Stanisław Jaśkowski)와 게르하르트 겐첸(Gerhard Gentzen)은 독자적으로 자연 연역의 계산법을 제시하였다. 특히 겐첸은 자연 연역과 시퀀트 계산의 핵심부분을 형식화하여 직관 논리의 형식화의 기반을 쌓고 페아노 산술의 일관성에 대한 첫 조합적 증명(combinatorial proof)을 완성했다. 자연 연역과 시퀀트 계산의 등장은 증명 이론의 해석적 증명(analytic proof)의 기초적 개념을 제시한 것이기도 하다.

구조적 증명 이론

구조적 증명 이론(영어: structural proof theory)은 증명 이론의 가장 고전적인 분야로, 특히 형식적 증명(formal proof)을 나타내는 증명 계산(proof calculus)의 구조에 관해 연구한다. 증명 계산의 가장 잘 알려진 세 가지 예시는 다음과 같다:

이들 각각은 고전적이든 직관적이든 간에 명제논리나 술어논리를 비롯하여 양상 논리 등 많은 논리체계들을 완전하고 공리적으로 형식화할 수 있다.

커리-하워드 대응을 통해 직관주의적인 증명 연산은 계산적인 유형 이론과 연관지어진다.

순서수 분석

순서수 분석(영어: ordinal analysis)은 이론에 순서수(주로 큰 가산 순서수)를 부여하여 그 강도(strength)를 측정하는 증명론적 기법으로, 이를 통해 산술이나 집합론의 일관성을 조합적으로 증명할 수 있다. 이때 특정되는 순서수를 증명론적 순서수(proof-theoretic ordinal)이라 한다. 예를 들어 페아노 공리계의 증명론적 순서수는 $\epsilon _{0}$ 이다. 순서수 분석은 게르하르트 겐첸이 초한귀납법을 통해 페아노 공리계의 무모순성을 증명하는 과정에서 개발해낸 것으로, 이후 다양한 형식 체계에 적용되었다.

재귀적으로 공리화된 이론 T가 있을 때, 특정 초한 순서수의 정초성(well-foundedness)이 T의 무모순성을 함의한다는 것을 유한한 산술체계 내에서 증명할 수 있다. 즉 순서수 분석 이론에서는 괴델의 제2불가능성 정리를 이론 T 내에서 그 이론을 증명할 순서수의 정초성이 증명될 수 없음을 뜻하는 것이라고 해석할 수 있다.

순서수 분석을 통해서 다음과 같은 결과들을 이끌어 낼 수 있다:

고전적 2차 산술과 집합론의 하위체계의 무모순성
조합적 독립성 증명
전역적 재귀함수와 정초적 순서수의 분류

이러한 순서수 분석은 상당히 강력한 기법으로, 같은 증명론적 순서수를 가진 이론은 서로 등무모순적인 경우가 많으며, 더 높은 증명론적 순서수를 가진 이론으로부터 더 낮은 증명론적 순서수를 가진 이론의 무모순성을 증명할 수 있다.

증명가능성 논리

증명가능성 논리(영어: provability logic)는 양상 논리의 일종으로, 양상 연산자 $\Box$ 가 "~가 증명가능하다"는 의미를 담는 논리이다. 양상논리의 일반 공리계 K에 뢰프의 정리(Löb's theorem)를 변형하여 추가한 GL(Gödel-Löb) 공리계를 바탕으로 삼는다.(추론 규칙으로는 Modus ponens와 Necessitation이 있다)

분배 공리: $\Box (p\implies q)\implies (\Box p\implies \Box q)$
뢰프(Löb) 공리: $\Box (\Box p\implies p)\implies p$

뢰프의 정리는 페아노 공리계 또는 그 확장 형식 체계 내에서 A의 증명가능성이 A를 암시한다는 것이 증명가능하면 A도 증명가능하다는 정리로, 증명론에서 중요한 진술이다.

역수학

역수학(영어: reverse mathematics)은 수학의 정리들을 증명하기 위해 어떤 공리가 필요한가를 추적하는 증명이론의 한 분야이다. 정리로부터 역으로 공리로 거슬러올라가는 꼴이기 때문에 역수학(逆數學)으로 불리게 되었다. 기술적 집합론(descriptive set theory)과 밀접한 연관이 있다.

역수학은 주로 모든 대상을 자연수나 자연수의 집합으로 표현할 수 있는 2차 산술(second-order arithmetic) 체계 내에서 전개된다. 또한 이렇게 표현된 식의 복잡성은 Post's theorem이 암시하는 바와 같이 계산 가능성과도 연관성이 있으며, 따라서 산술적 위계와 그 확장인 해석적 위계(analytical hierarchy)는 역수학을 비롯한 증명 이론에 있어서 중요한 개념이 된다.

스티븐 심슨(Stephen G. Simpson)은 역수학에서 일반적으로 나타나는 2차 산술의 하위체계 5개를 특정하기에 이르렀다. 이들은 Big Five라고도 불리며 증명론적 순서수가 작은 것부터 정렬하면 RCA₀, WKL₀, ACA₀, ATR₀, and Π1
1-CA₀가 있다. 이들 각각은 구성주의, 유한주의 등 수학적 입장을 나타내고 있는 것으로, 수리철학적 입장에 따라 어떠한 공리들을 받아들일 것인가를 분별할 중요한 기준이 될 수 있어 현대 기초론 분야에서 활발히 연구되고 있다.

같이 보기

참고 문헌

Troelstra, A. S.; H. Schwichtenberg (1996). 《Basic Proof Theory》. Cambridge Tracts in Theoretical Computer Science (영어). Cambridge University Press. ISBN 0-521-77911-1.

외부 링크

“Proof theory”. 《Encyclopedia of Mathematics》 (영어). Springer-Verlag. 2001. ISBN 978-1-55608-010-4.
Weisstein, Eric Wolfgang. “Proof theory”. 《Wolfram MathWorld》 (영어). Wolfram Research.
von Plato, Jan (2014년 10월 13일). “The development of proof theory”. 《Stanford Encyclopedia of Philosophy》 (영어).
Schroeder-Heister, Peter (2012년 12월 5일). “Proof-theoretic semantics”. 《Stanford Encyclopedia of Philosophy》 (영어).
Avigad, Jeremy; Erich H. Reck (2001). ““Clarifying the nature of the infinite”: the development of metamathematics and proof theory” (영어). Carnegie-Mellon Technical Report CMU-PHIL-120. ^{[깨진 링크(과거 내용 찾기)]}