증명 이론

증명 이론은 증명들을 형식적인 수학적 개체로 나타내며, 수학적 기술에 의한 분석을 용이하게 하는 수학 논리학의 주요^[1] 분야이다.증명은 일반적으로 논리 시스템의 공리와 추론 규칙에 따라 구성되는 플레인 리스트, 박스형 리스트 또는 트리와 같은 유도적으로 정의된 데이터 구조로 나타납니다.결과적으로, 증명 이론은 본질적으로 의미론인 모델 이론과 대조적으로 본질적으로 구문론이다.

증명 이론의 주요 영역들 중 일부는 구조 증명 이론, 순서 분석, 증명 논리, 역수학, 증명 마이닝, 자동화된 정리 증명, 그리고 증명 복잡성을 포함합니다.또한 많은 연구가 컴퓨터 과학, 언어학 및 철학 분야의 응용 분야에 초점을 맞추고 있습니다.

역사

비록 논리학의 공식화가 고틀롭 프레지, 주세페 페아노, 버트런드 러셀, 그리고 리처드 데데킨드와 같은 인물들에 의해 훨씬 더 진전되었지만, 현대 증명 이론의 이야기는 종종 수학의 재단에서 힐버트의 프로그램을 시작한 데이비드 힐버트에 의해 확립된 것으로 보여진다.이 프로그램의 중심 아이디어는 만약 우리가 수학자들이 필요로 하는 모든 정교한 공식 이론들에 대해 결정적인 증거를 제시할 수 있다면, 우리는 메타수학적인 논거를 통해 이 이론들을 기초할 수 있다는 것이었다. 이것은 그들의 순수한 보편적 주장들(더 기술적으로 입증 가능한 $)$을 보여준다.$playstyle \Pi$ _${1}^{0}$문장$$)은 최종적으로 참이다. 일단 근거가 있으면 우리는 이상적 실체의 존재에 대한 의사적 의미 규정으로 간주하여 그들의 존재론적 이론의 비완료적 의미에 대해 신경쓰지 않는다.

프로그램의 실패는 Kurt Gödel의 불완전성 이론에서 비롯되었으며, 이것은 어떤 간단한 산술적 진실을 표현하기에 충분히 강한 어떤 δ-일관성 이론도 그 자체의 일관성을 증명할 수 없다는 것을 보여주었고, Gödel의 공식에는 ${\displaystyle {\mathrm{}}_{}^{}}$0($표시$ 스타일 \Displaystyle $\Pi$ _${1}^{$0$$}}}}}{0}}}}.그러나 힐베르트 프로그램의 수정판이 등장하여 관련 주제에 대한 연구가 수행되었다.그 결과, 특히 다음과 같은 것이 실현되었습니다.

• Gödel의 결과, 특히 J. Barkley Rosser의 개선으로 γ-일관성을 단순일관성으로 약화시킨다.
• 모달 언어, 입증 가능 논리 측면에서 괴델 결과의 핵심을 공리화한다.
• 앨런 튜링과 솔로몬 페퍼맨에 의한 이론의 초무한 반복
• 자기 검증 이론의 발견, 자기 자신을 말할 수 있을 만큼 강하지만 너무 약해서 괴델의 타당성 없는 주장의 핵심인 대각선 주장을 실행할 수 없다.

힐베르트의 프로그램의 흥망성쇠와 동시에, 구조 증명 이론의 기초가 확립되고 있었다.Jan Wukasiewicz는 1926년에 논리 추론 규칙에서 가정으로부터 결론을 도출할 수 있다면 논리학의 공리적인 표현에 대한 기초로서 힐베르트 시스템을 개선할 수 있다고 제안했다.이에 대해 Staniswaw Jakkowski(1929년)와 Gerhard Gentzen(1934년)은 독자적으로 자연추론의 계산이라고 불리는 시스템을 제공하였고, Gentzen의 접근방식은 도입규칙으로 표현된 명제를 주장하는 근거와 엘리미나에서 명제를 받아들이는 결과 사이의 대칭의 개념을 도입하였다.증명 ^[2]이론에서 매우 중요한 것으로 증명된 생각인 규칙.Gentzen(1934)은 또한 논리적 ^[3]연결의 이중성을 더 잘 표현하는 유사한 정신으로 발전한 미적분인 시퀀셜 미적분의 개념을 도입했고, 계속해서 직관적 논리의 형식화에 근본적인 발전을 이루었으며, 페아노 산수의 일관성에 대한 최초의 조합적 증거를 제공했다.자연적 연역과 순차적 미적분의 제시가 함께 이론을 증명하기 위한 분석적 증명이라는 기본 개념을 도입했다.

구조 증명 이론

구조적 증명 이론은 증명 계산의 세부 사항을 연구하는 증명 이론의 하위 분야이다.가장 잘 알려진 세 가지 증명 계산 방식은 다음과 같습니다.

• 힐베르트 계산
• 자연 공제 계산
• 순차 계산

이들 각각은 고전적 또는 직관적 맛의 명제적 또는 술어적 논리, 거의 모든 모달 논리, 그리고 관련성 논리나 선형 논리 같은 많은 하위구조적 논리학의 완전하고 자명한 형식화를 제공할 수 있다.사실, 이러한 계산 중 하나에 대표되는 것에 저항하는 논리를 찾는 것은 드문 일이다.

증명 이론가들은 전형적으로 분석 증명 개념을 뒷받침하는 증명 계산에 관심이 있다.분석 증명의 개념은 순차 미적분을 위해 겐젠에 의해 도입되었습니다.여기서는 분석 증명은 컷 프리입니다.컷프리 증명에 대한 관심의 대부분은서브포뮬라 특성: 컷 프리 프루프의 최종 시퀀스에 포함되는 모든 포뮬라는 전제 중 하나의 서브포뮬라이다.이것은 시퀀셜 미적분의 일관성을 쉽게 보여줄 수 있게 해준다; 만약 빈 시퀀스가 파생될 수 있다면 그것은 어떤 전제의 보조 공식이어야 할 것이다, 그러나 그렇지 않다.젠젠의 중간순차정리, 크레이그 보간정리, 헤르브란트의 정리도 컷-엘리미네이션 정리의 결과로서 뒤따른다.

Gentzen의 자연 연역 미적분학은 Dag Prawitz에 의해 보여지는 분석 증거의 개념도 지지한다.정의는 조금 더 복잡합니다.분석적 증명은 용어 개서에서의 정규형 개념과 관련된 정규형이라고 합니다.Jean-Yves Girard의 프루프 네트와 같은 보다 이국적인 프루프 계산도 분석 프루프 개념을 뒷받침한다.

환원 논리에서 발생하는 특정 분석 증명 패밀리는 목표 지향적 증명 검색 절차의 큰 패밀리를 특징짓는 집중 증명이다.증명 시스템을 초점 형태로 변환하는 능력은 절단 허용성이 증명 시스템이 구문적으로 ^[4]일관됨을 보여주는 방법과 유사한 방식으로, 그 구문적 품질을 잘 나타냅니다.

구조 증명 이론은 자연 연산의 정규화 과정과 유형 람다 미적분의 베타 감소 사이의 구조적 유사성을 관찰하는 카레-하워드 대응에 의해 유형 이론과 연결된다.이것은 Per Martin-Löf에 의해 개발된 직관적 유형 이론의 기초를 제공하며, 종종 세 번째 구간이 데카르트적 닫힌 범주인 3방향 대응으로 확장된다.

구조 이론의 다른 연구 주제로는 다양한 논리학에 대한 결정 절차와 반결정 절차를 제공하기 위해 구조 증명 이론의 분석 증명 중심 아이디어를 적용하는 분석 이론이 있다.

순서형 분석

순서형 해석은 산술, 해석, 집합론의 서브시스템에 조합 일관성 증명을 제공하는 강력한 기술이다.괴델의 두 번째 불완전성 정리는 종종 충분한 힘을 가진 이론에서는 최종적인 일관성 증명은 불가능하다는 것을 보여주는 것으로 해석됩니다.순서형 분석을 통해 이론의 일관성에 대한 무한 내용을 정확하게 측정할 수 있습니다.일관된 재귀 공리화 이론 T에 대해, 어떤 초한 서수의 충분한 근거가 T. 괴델의 두 번째 불완전성 정리의 일관성을 내포하고 있다는 것을 최종 산술적으로 증명할 수 있다.

순서 해석의 결과는 (1) 구성 이론에 대한 고전적인 2차 산술 및 집합론의 서브시스템의 일관성, (2) 조합 독립성 결과 및 (3) 입증 가능한 전체 재귀 함수와 입증 가능한 충분한 근거가 있는 서수의 분류를 포함한다.

서수 분석은 Gentzen에 의해 시작되었으며, Gentzen은 서수 θ까지₀ 초한 유도를 사용하여 Peano 산술의 일관성을 증명했습니다.순서 해석은 1차 및 2차 산술 및 집합론의 많은 조각으로 확장되었다.한 가지 주요 도전은 추정 이론의 순서적 분석이었다.이 방향의 첫 번째 돌파구는 순서도 방법을 사용하여 δ-CA의¹
₁₀ 일관성에 대한 Takeuti의 증명이었다.

증명가능성

증명가능성 논리는 상자 연산자가 '그것은 증명가능하다'고 해석되는 모달 논리이다.요점은 상당히 풍부한 형식 이론의 증명 술어 개념을 포착하는 것이다.Peano 산술에서 증명 가능한 증명 논리 GL(Gödel-Löb)의 기본 공리로서 힐버트-베르나이즈 유도성 조건과 뢰브 정리(A의 증명 가능성이 A를 내포하는 것이 입증 가능한 경우 A는 증명 가능한 것이다)의 모달 유추를 취한다.

페아노 산술의 불완전성에 관한 기본적인 결과와 관련 이론은 증명 논리에 유사점을 가지고 있다.예를 들어, 모순을 증명할 수 없다면 모순을 증명할 수 없다는 것이 GL의 정리이다(Gödel의 두 번째 불완전성 정리).고정점 정리의 모달 유사점도 있다.Robert Solovay는 Peano 산술에 관해 모달 논리 GL이 완전하다는 것을 증명했다.즉, Peano 산술에서의 provibility의 명제 이론은 모달 논리 GL로 완전히 표현된다.이것은 직접적으로 페아노 산술의 증명 가능성에 대한 명제적 추론이 완전하고 결정 가능하다는 것을 암시한다.

증명 논리학의 다른 연구는 1차 증명 논리, 폴리모달 증명 논리(물체 이론에서는 증명 가능성을 나타내고 메타 이론에서는 증명 가능성을 나타내는 다른 모달), 그리고 증명성과 해석 가능성 사이의 상호작용을 포착하기 위한 해석성 논리에 초점을 맞추고 있다.매우 최근의 몇몇 연구는 산술 이론의 순서 해석에 단계적 증명성 대수의 적용을 포함했다.

역수학

역수학은 수학의 ^[5]이론을 증명하기 위해 어떤 공리가 필요한지 결정하는 수학 논리학의 프로그램이다.이 분야는 하비 프리드먼에 의해 설립되었다.그것의 정의 방법은 "정리에서 공리로 거꾸로 가는 것"으로 설명될 수 있는데, 공리에서 정리를 도출하는 일반적인 수학적 관행과는 대조적이다.역수학 프로그램은 선택 공리와 조른의 보조항목이 ZF 집합론보다 동등하다는 고전적 정리 같은 집합론의 결과에 의해 암시되었다.그러나 역수학의 목표는 집합론의 가능한 공리보다는 수학의 일반적인 이론의 가능한 공리를 연구하는 것이다.

역수학에서, 사람은 너무 약해서 관심을 가질 수 있는 대부분의 이론들을 증명하지 못하지만, 이러한 이론들을 진술하기 위해 필요한 정의를 개발할 수 있을 만큼 충분히 강력하다.예를 들어, "실수의 모든 유계 수열에는 슈프림이 있다"라는 정리를 연구하기 위해서는 실수와 실수의 수열을 말할 수 있는 기저 시스템을 사용할 필요가 있다.

기본 체계에서는 진술할 수 있지만 기본 체계에서는 입증할 수 없는 각 정리에 대해, 목표는 그 정리를 증명하기 위해 필요한 특정한 공리 체계(기본 체계보다 더 강한)를 결정하는 것이다.정리 T를 증명하기 위해 시스템 S가 필요하다는 것을 보여주기 위해서는 두 가지 증명이 필요하다.첫 번째 증명은 T가 S로부터 증명 가능하다는 것을 보여준다.이것은 시스템 S에서 실행될 수 있다는 정당성과 함께 일반적인 수학적 증명이다.반전이라고 알려진 두 번째 증거는 T 자체가 S를 의미함을 나타냅니다. 이 증거는 기본 시스템에서 수행됩니다.이 반전은 기본 시스템을 확장하는 어떤 공리 시스템 S'도 T를 증명하는 동안 S보다 약할 수 없다는 것을 확립한다.

역수학에서 한 가지 놀라운 현상은 빅5 공리 시스템의 견고성이다.강도를 높이기 위해 이들 시스템은 RCA, WKL₀, ACA₀, ATR₀ 및 δ-CA라는¹
₁₀ 이니셜로₀ 명명됩니다.수학적으로 역분석된 일반 수학의 거의 모든 정리가 이 다섯 가지 시스템 중 하나와 동등하다는 것이 증명되었다.최근 연구는 RT(Ramsey's theorem for²
₂ pairs)처럼 이 프레임워크에 깔끔하게 들어맞지 않는 조합 원리에 초점을 맞추고 있다.

역수학 연구는 종종 증명 이론뿐만 아니라 재귀 이론의 방법과 기술을 통합합니다.

기능적 해석

기능적 해석은 기능적 해석에서 비건설적 이론의 해석이다.기능적 해석은 보통 두 단계로 진행됩니다.첫째, 고전 이론 C를 직관적인 이론 I로 "축소"한다.즉, C의 이론을 I의 이론으로 변환하는 건설적인 매핑을 제공한다.둘째, 직관론적 이론 I을 함수 F의 수량화 없는 이론으로 환원한다.이러한 해석은 힐베르트 프로그램의 한 형태에 기여하는데, 이는 건설적인 이론과 관련된 고전 이론의 일관성을 증명하기 때문이다.성공적인 기능적 해석은 무한 이론의 축소를 최종 이론으로, 추정 이론은 서술적인 이론으로 귀결시켰다.

기능적 해석은 또한 축소된 이론의 증거로부터 건설적인 정보를 추출하는 방법을 제공한다.해석의 직접적인 결과로서 일반적으로 I 또는 C에서 전체성이 증명될 수 있는 모든 재귀 함수가 F항으로 표현된다는 결과를 얻는다.I에서 F에 대한 추가 해석을 제공할 수 있는 경우(때로는 가능), 이 특성은 실제로 정확한 것으로 나타납니다.종종 F의 항이 원시 재귀 함수나 다항 시간 계산 가능 함수와 같은 자연적인 함수 클래스와 일치한다는 것이 밝혀집니다.기능적 해석은 또한 이론의 순서적 분석을 제공하고 입증 가능한 재귀적 함수를 분류하기 위해 사용되어 왔다.

함수 해석의 연구는 유한형 함수의 수량화 없는 이론에서 직관적 산술의 쿠르트 괴델의 해석으로 시작되었다.이 해석은 일반적으로 변증법 해석으로 알려져 있다.직관적 논리에서의 고전적 논리학의 이중 부정 해석과 함께, 그것은 고전적 산수를 직관적 산수로 환원시킨다.

공식 및 비공식 증명

일상적인 수학 연습의 비공식적인 증명은 공식적인 증명 이론과 다르다.이는 전문가가 충분한 시간과 인내심을 가진다면 최소한 원칙적으로 공식적인 증거를 재구성할 수 있도록 하는 대략적인 스케치와 같다.대부분의 수학자들에게, 완전히 공식적인 증명서를 쓰는 것은 너무 현학적이고 장황해서 일반적으로 쓰이지 않는다.

형식 증명은 대화형 정리 증명에서 컴퓨터의 도움을 받아 구성됩니다.중요한 것은, 이러한 증명은 컴퓨터를 통해서도 자동적으로 확인될 수 있다는 것입니다.공식 증명을 확인하는 것은 보통 간단한 반면, 증명(자동 정리 증명)을 찾는 것은 일반적으로 어렵습니다.반면 수학 문헌의 비공식적인 증명은 몇 주간의 안전 점검이 필요하며 여전히 오류가 있을 수 있다.

증명 이론의 의미론

언어학에서 유형논리문법, 범주문법, 몬태규문법은 형식적인 자연어 의미론을 제공하기 위해 구조적 증명 이론에 기초한 형식주의를 적용한다.

「 」를 참조해 주세요.

• 중간 논리
• 모델 이론
• 증명(진실)
• 실증 기술
• 시퀀트 미적분

메모들

레퍼런스

• J. Avigad와 E.H. Leck(2001).무한의 본질을 밝히는 것: 메타 수학과 증명 이론의 발전.Carnegie-Mellon 기술 보고서 CMU-PHIL-120.
• J. Barwise, ed. (1978)수학 논리 핸드북노스홀랜드.
• S. Buss, ed. (1998) 입증 이론 핸드북.엘세비어
• G. 겐젠(1935/1969)"논리 추리 수사"M.E. 사보, ED.게르하르트 겐젠의 논문 수집.노스홀랜드."Untersuchungen über das logische Schliessen", Mathemisches Zeitschrift v. 39, 176–210, 405 431에서 사보 옮김.
• J.Y. 지라드, P.테일러, Y. 라퐁(1988)"증거와 활자"케임브리지 대학 출판부ISBN 0-521-37181-3
• D. 프라위츠(1965).자연 공제: 증명 이론 연구, 도버 출판물, ISBN 978-0-486-44655-4
• S.G. 심슨(2010).2차 산술 서브시스템, 2판Cambridge University Press, ISBN 978-0521150149.
• A. S. Troelstra와 H.Schwichtenberg(1996).기본 증명 이론, 캠브리지 이론 컴퓨터 과학 분야 논문, 캠브리지 대학 출판부, ISBN 0-521-77911-1.
• H. 왕(1981년).Van Nostrand Reinhold Company, ISBN 0-442-23109-1 수학논리 인기강좌.

외부 링크

• "Proof theory", Encyclopedia of Mathematics, EMS Press, 2001 [1994]
• J. von Plato (2008).증명 이론의 발전스탠포드 철학 백과사전.