증명 이론

위키백과, 우리 모두의 백과사전.
둘러보기로 가기 검색하러 가기

수리논리학에서, 증명 이론(證明理論, 영어: 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)의 기초적 개념을 제시한 것이기도 하다.

구조적 증명 이론[편집]

구조적 증명 이론은 증명 이론의 하위분야로, 특히 증명 계산에 관해 연구한다. 증명 계산의 가장 잘 알려진 세 가지 예시는 다음과 같다:

이들 각각은 고전적이든 직관적이든 간에 명제논리술어논리를 비롯하여 거의 모든 양상 논리나 많은 부분구조 논리 등 여러 논리체계들의 완전하고 공리적인 형식화를 제시할 수 있으며, 이 계산들 중 하나로라도 표현되지 않는 논리는 흔하지 않다.

참고 문헌[편집]

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

외부 링크[편집]