분석증거
Analytic proof수학에서 분석적 증명이란 분석에서 방법만을 사용하고 대수적 방법이나 기하학적 방법을 주로 사용하지 않는 정리의 증거다.이 용어는 베르나르 볼자노에 의해 처음 사용되었는데, 그는 처음에는 자신의 중간 가치 정리에 대한 비분석적 증거를 제공했고, 그 후 몇 년 후 어느 한 지점에서 서로 교차하는 선에 관한 직관으로부터 자유로워진 정리에 대한 증거를 제공했기 때문에, 분석적(Bolzano 1817)이라고 부르는 데 행복을 느꼈다(Volzano 1817).
볼자노의 철학적인 저작은 시위가 언제 분석적인 것으로 간주될 수 있는지에 대한 좀 더 추상적인 읽기를 권장했다. 여기서 증명서는 주제(Sebastik 2007)를 넘어서지 않으면 분석적인 것이다.증명 이론에서, 분석적 증거는 그들 중 어느 누구도 가정에 포함된 것과 입증된 것을 넘어서지 못하게 하는 추론의 종류에 관한 조건 때문에 특별한 방법으로 구조가 단순한 증거를 의미하게 되었다.
구조증거이론
증명 이론에서, 분석적 증명 개념은 본질적으로 구별되는 다수의 증명 캘커리 사이의 유사성을 끌어내는 근본적인 개념을 제공하므로, 구조 증명 이론의 하위 분야를 정의한다.분석적 증명에 대한 논란의 여지가 없는 일반적인 정의는 없지만, 몇 가지 증명에 대해서는 받아들여지는 개념이 있다.예를 들면 다음과 같다.
- Gerhard Gentzen의 자연공제 미적분학에서 분석적 증거는 정상적인 형태에 있는 것들이다. 즉, 공식 발생은 제거 규칙의 주요 전제와 도입 규칙의 결론이다.
- 겐첸의 속편 미적분학에서 분석적 증거는 절단 규칙을 사용하지 않는 것이다.
그러나 조건을 만족하지만 분석적이지 않은 증거가 있도록 양쪽 캘커리의 추론 규칙을 확장할 수 있다.예를 들어, 특히 까다로운 예는 Tableau 방법에 널리 사용되는 분석 절단 규칙으로, 절단 공식이 절단 규칙의 측면 공식의 보조 형태인 절단 규칙의 특별한 경우: 분석적 절단을 포함하는 증거는 분석적이지 않은 규칙으로 인한 것이다.
더욱이 겐첸의 이론과 유사하지 않은 구조적 증명 이론은 다른 분석적 증명 개념을 가지고 있다.예를 들어, 구조물의 미적분은 그 추론규칙을 위편과 아래편이라고 하는 쌍으로 조직하고, 분석적 증거는 아래편만 포함하는 것이다.
