교정 미적분학
Proof calculus수학 논리학에서는 증명 미적분학이나 증명 시스템이 만들어져서 진술을 증명한다.
개요
증명 시스템에는 다음 구성 요소가 포함된다.[1]
- 언어: 예를 들어 제안 논리 또는 1차 논리처럼 시스템에서 인정하는 공식의 집합 L.
- 추론 규칙: 공리와 이론으로부터 이론들을 증명하기 위해 사용될 수 있는 규칙들의 목록.
- 공리: 유효하다고 가정된 L의 공식 모든 이론은 공리에서 나온 것이다.
많은 증명 미적분은 결정되지 않고 근본적으로 다른 로직들에 사용될 수 있기 때문에 일반적으로 주어진 증명 미적분학은 하나의 특정한 형식적인 시스템 이상을 포함한다. 예를 들어, 패러다임 케이스는 연속 미적분학으로, 직관적 논리와 목적적합성 논리의 결과 관계를 표현하는데 사용될 수 있다. 그러므로 느슨하게 말하면, 증명 미적분학은 특정한 형식 추론의 스타일에 의해 특징지어지는 템플릿이나 설계 패턴으로, 그러한 시스템에 대한 실제 추론 규칙을 명시함으로써 특정 형식 시스템을 생산하는데 특화될 수 있다. 이 용어를 가장 잘 정의할 수 있는 방법에 대한 논리학자 간 의견 일치가 없다.
교정 칼쿨리의 예
가장 널리 알려진 증명 캘커리는 여전히 널리 사용되고 있는 고전 캘커리다.
- 힐버트 시스템의 등급이며, 그 중 가장 유명한 예는 1928년 힐버트-아커만 시스템의 1차 논리학이다.
- 게르하르트 겐첸의 자연공제의 미적분(구조적 증명 이론의 첫 번째 형식주의)이며 기능적 프로그래밍에 관한 논리와 관련된 공식적 형식적 대응의 초석이다.
- 구조 증명 이론의 가장 많이 연구된 형식주의인 겐첸의 속편 미적분학.
많은 다른 증거 칼쿨리는 세미놀이었거나 그랬을 수도 있지만 오늘날 널리 쓰이지 않고 있다.
- 오르가논에 제시된 아리스토텔레스의 삼단논법적 미적분은 형식화를 흔쾌히 인정한다. 용어 논리의 보호 아래 행해지는 삼단논법에 대한 현대적 관심은 여전히 존재한다.
- 고틀로프 프레게의 베그리프슈리프트(1879)의 2차원 표기법은 대개 현대적인 정량화 개념을 논리에 도입하는 것으로 간주된다.
- C.S. Peirce의 실존적 그래프는 역사가 다르게 작용했다면 쉽게 정석이었을 것이다.
현대의 논리학 연구는 경쟁적인 증거와 함께 복잡하다.
- 일반적인 텍스트 구문을 일부 그래픽 구문으로 대체하는 몇 가지 시스템이 제안되었다. 교정망과 권적 미적분학도 그러한 시스템들 중 하나이다.
- 최근 구조적 입증 이론에 관심이 있는 많은 논리학자들이 디스플레이 논리, 초시퀀스, 구조의 미적분, 뭉치 함축성 등 깊은 추론을 가지고 미적분학을 제안하고 있다.
참고 항목
참조
- ^ Anita Wasilewska. "General proof systems" (PDF).
