증명 이론

3. 구조적 증명 이론

구조적 증명 이론(structural proof theory^영어)은 형식적 증명(formal proof)을 나타내는 증명 계산(proof calculus)의 구조에 관해 연구하는 분야이다. 얀 우카시에비치는 논리의 추론 규칙에 따라 전제로부터 결론을 도출하는 것을 허용한다면 힐베르트 체계를 논리의 공리적 방식의 기초로써 발전시킬 수 있다고 제안하였고, 이에 스타니스와프 야시코프스키와 게르하르트 겐첸은 독자적으로 자연 연역 계산법을 제시하였다. 특히 겐첸은 자연 연역과 시퀀트 계산의 핵심 부분을 형식화하여 직관 논리 형식화의 기반을 쌓고 페아노 산술의 일관성에 대한 첫 조합적 증명(combinatorial proof)을 완성했다.

겐첸은 단축 제거 정리를 통해 부분 공식 속성을 증명하였다. 단축이 없는 증명의 최종 시퀀스에 있는 모든 공식은 전제 중 하나의 부분 공식이기에, 시퀀트 계산의 일관성을 쉽게 보일 수 있다.^[4] 겐첸의 중간 시퀀스 정리, 크레이그 보간 정리 및 헤르브란트 정리 또한 단축 제거 정리의 따름 정리이다.^[4]

3. 1. 주요 증명 계산

3. 2. 커리-하워드 대응과 유형 이론

4. 순서수 분석

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

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

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

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

5. 증명가능성 논리

증명가능성 논리(provability logic^영어)는 양상 논리의 일종으로, 양상 연산자 $\backslash Box$를 "~가 증명가능하다"는 의미로 해석한다. 페아노 공리계 또는 그 확장 형식 체계에서, A의 증명가능성이 A를 암시한다는 것이 증명가능하면 A도 증명가능하다는 뢰프의 정리를 추가한 GL(괴델-뢰브) 공리계를 바탕으로 한다. (추론 규칙: Modus ponens, Necessitation)

• 분배 공리: $\backslash Box\; (p\; \backslash implies\; q)\; \backslash implies\; (\backslash Box\; p\; \backslash implies\; \backslash Box\; q)$
• 뢰프 공리: $\backslash Box\; (\backslash Box\; p\; \backslash implies\; p)\; \backslash implies\; p$

6. 역수학

역수학(reverse mathematics^영어)은 수학의 정리들을 증명하기 위해 어떤 공리가 필요한가를 추적하는 증명 이론의 한 분야이다. 정리로부터 역으로 공리로 거슬러 올라가는 꼴이기 때문에 역수학(逆數學)으로 불리게 되었다. 기술적 집합론과 밀접한 관련이 있으며, 주로 2차 산술 체계 내에서 연구된다.^[5]

하비 프리드먼에 의해 창시된 역수학의 정의 방법은, 공리로부터 정리를 유도하는 일반적인 수학적 관행과는 반대로 "정리에서 공리로 거꾸로 가는 것"으로 설명할 수 있다.

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

역수학 연구는 종종 재귀 이론과 증명 이론의 방법과 기법을 통합한다.

7. 함수적 해석

함수적 해석은 비구성적 이론을 함수적 이론으로 해석하는 기법이다. 함수적 해석은 힐베르트 프로그램의 한 형태에 기여하는데, 고전적 이론의 일관성을 구성적 이론에 상대적으로 증명하기 때문이다. 성공적인 함수적 해석은 무한 이론을 유한 이론으로, 비예측적 이론을 예측적 이론으로 축소하는 결과를 낳았다.

함수적 해석은 일반적으로 두 단계로 진행된다.

# 고전적 이론 C를 직관주의적 이론 I로 "축소"한다. 즉, C의 정리를 I의 정리로 변환하는 구성적 매핑을 제공한다.

# 직관주의적 이론 I를 양자화사가 없는 함수 F의 이론으로 축소한다.

함수적 해석은 또한 축소된 이론의 증명으로부터 구성적 정보를 추출하는 방법을 제공한다. 일반적으로 해석의 직접적인 결과로, I 또는 C에서 전체성을 증명할 수 있는 모든 재귀 함수는 F의 항으로 표현된다는 결과를 얻는다.

쿠르트 괴델의 Dialectica 해석은 함수적 해석 연구의 시작점으로, 유한형의 함수에 대한 양자화사가 없는 이론에서 직관주의적 산술에 대한 해석을 제공한다.^[2] 이 해석은 직관주의적 논리에서 고전 논리의 이중 부정 해석과 함께, 고전 산술을 직관주의적 산술로 축소한다.

8. 형식적 증명과 비형식적 증명

일상적인 수학적 실천에서의 '비형식적' 증명은 증명 이론의 '형식적' 증명과는 다르다. 비형식적 증명은 전문가가 충분한 시간과 인내심을 가지고 형식적 증명을 (적어도 이론적으로는) 재구성할 수 있도록 하는, 일종의 고차원적인 스케치와 같다.^[4] 대부분의 수학자들에게 완전한 형식적 증명을 작성하는 것은 너무나 세부적이고 장황하여 일반적으로 사용하기 어렵다.

형식적 증명은 대화형 정리 증명에서 컴퓨터의 도움을 받아 구성된다.^[4] 중요한 점은 이러한 증명이 컴퓨터에 의해서도 자동으로 검증될 수 있다는 것이다.^[4] 형식적 증명을 확인하는 것은 대개 간단하지만, 증명을 '찾는' 것(자동 정리 증명)은 일반적으로 어렵다.^[4] 반대로 수학 문헌에 있는 비형식적 증명은 검증을 위해 몇 주 동안의 동료 심사를 거쳐야 하며, 여전히 오류를 포함할 수 있다.^[4]

9. 증명론적 의미론

언어학, 유형 논리 문법, 범주 문법, 몬테규 문법에서는 구조적 증명 이론에 기반한 형식을 적용하여 형식적 자연 언어 의미론을 제공한다.^[6]

참조

_[1] 논문
_[2] 서적
_[3] 서적
_[4] 간행물 Focused and Synthetic Nested Sequents Springer Berlin Heidelberg 2016
_[5] 문서
_[6] 서적 Popular Lectures on Mathematical Logic Van Nostrand Reinhold Company 1981