시퀀스 미적분학

Sequent calculus

수학적 논리학에서 시퀀스 미적분학증명서의 모든 행이 조건부 태토학(게르하르트 겐첸서열이라 불리는 것)이 아닌 조건부 태토학인 형식 논리 논리의 한 스타일이다. 각 조건부 tautology는 추론의 규칙과 절차에 따라 형식적인 논쟁에서 이전 행의 다른 조건부 tautology로부터 유추되어, 모든 행이 무조건적인 tautol이었던 David Hilbert의 초기 형식 논리학 스타일보다 수학자들이 사용하는 자연적인 추론 스타일에 더 나은 근사치를 제공한다.ogy. 예를 들어, 명제는 비논리적 공리에 암묵적으로 의존할 수 있다. 이 경우 시퀀스는 조건부 토폴로지가 아닌 1차 언어로 조건부 정리를 나타낸다.

순차 미적분은 선별 논리적인 주장을 표현하기 위한 몇 가지 현존하는 증명 미적분학 스타일 중 하나이다.

  • 힐버트 스타일. 모든 선은 무조건적인 tautology(또는 정리)이다.
  • 젠첸 스타일. 모든 선은 왼쪽에 0개 이상의 조건이 있는 조건부 tautology(또는 정리)이다.
    • 자연공제. 모든 (조건부) 노선은 정확히 오른쪽에 하나의 주장된 명제를 가지고 있다.
    • 시퀀스 미적분학 모든 (조건부) 노선은 우측에 0 또는 그 이상의 주장된 명제를 가지고 있다.

즉, 자연적 추론과 추론적 미적분 체계는 특별히 구별되는 종류의 겐젠식 체계가 된다. 힐버트식 시스템은 일반적으로 공리 집합에 더 의존하는 매우 적은 수의 추론 규칙을 가지고 있다. 젠첸식 시스템은 일반적으로 공리가 거의 없으며, 만약 있다면, 규칙 집합에 더 의존한다.

겐첸식 시스템은 힐버트식 시스템에 비해 상당히 실용적이고 이론적인 이점을 가지고 있다. 예를 들어 자연적 추론과 순열 미적분학 시스템은 모두 보편적 및 실존적 정량자의 제거와 도입을 촉진하여 훨씬 간단한 명제 미적분학 규칙에 따라 미정수의 논리표현을 조작할 수 있다. 일반적인 주장에서는 정량자를 제거한 다음 명제 미적분학을 미정식(일반적으로 자유 변수를 포함)에 적용한 다음 정량자를 다시 도입한다. 이것은 수학자들이 실제로 수행하는 수학적 증거와 매우 유사하다. 술어 미적분학 증거는 일반적으로 이 접근법으로 발견하기가 훨씬 쉬우며, 종종 더 짧다. 자연공제 제도는 실질적인 정리검증에 더 적합하다. 순차 미적분 시스템은 이론 분석에 더 적합하다.

개요

증명 이론수학적 논리학에서, 연속 미적분학은 일정한 형식의 추론과 특정한 형식적 속성을 공유하는 형식 시스템의 한 가족이다. 첫 번째 시퀀스 캘커리 시스템인 LKLJ는 게르하르트 겐첸에[1] 의해 1934/1935년에 1차 논리(각각 고전적 버전과 직관적 버전)에서 자연 추론을 연구하는 도구로 도입되었다. Gentzen이 LK와 LJ에 대해 소위 말하는 "주 정리"(Hauptsatz)는 컷-리미네이션 정리였으며,[2][3] 결과 일관성을 포함한 광범위한 메타이탈적 결과가 나왔다. 겐젠은 몇 년 후 괴델의 불완전성 이론에 놀라움으로 대응하여 페아노 산술의 일관성에 대한 (투명성) 증거를 제시하기 위해 컷 엘리미네이션 주장을 적용하면서 이 기법의 힘과 유연성을 더욱 입증했다. 이 초기 작품부터 겐첸계라고도 불리는 속편적 칼쿨리,[4][5][6][7] 이와 관련된 일반적인 개념들이 증명 이론, 수학 논리학, 자동화된 추론 분야에 폭넓게 적용되어 왔다.

힐버트식 공제 제도

서로 다른 방식의 공제제도를 분류하는 한 가지 방법은 제도에서 판단의 형태, 즉 사물이 (하위)방식의 결론으로 나타날 수 있는 형태를 보는 것이다. 가장 단순한 판단 양식은 힐버트식 공제 시스템에서 사용되는데, 여기서 판단 양식은 다음과 같다.

여기서 1차 논리(또는 공제 시스템이 적용되는 논리, 예를 들어 명제 미적분 또는 고차 논리 또는 모달 논리)의 공식이다. 그 이론들은 유효한 증거에서 결론적인 판단으로 나타나는 공식들이다. 힐버트식 시스템은 공식과 판단의 구분이 필요하지 않다; 우리는 단지 뒤에 오는 사례들과 비교하기 위해 여기에 하나를 만든다.

힐버트식 시스템의 단순한 구문에 대해 지불되는 가격은 완전한 공식적인 증명들이 극도로 길어지는 경향이 있다는 것이다. 그러한 시스템에서 입증에 대한 구체적인 주장은 거의 항상 공제 정리에 호소한다. 이것은 자연적 추리에서 일어나는 제도에서 공제 정리를 형식적인 규칙으로 포함시키는 발상으로 이어진다.

자연공제제도

자연 추론에서 판단은 그 모양을 가지고 있다.

여기서 는) 다시 공식이고 순열은 중요하지 않다. 즉, 판단은 개찰구 기호 " }"의 왼쪽에 공식의 목록(아마도 비어 있을 것이다)으로 구성되며, 오른쪽에는 공식 하나가 있다.[8][9][10] 왼쪽이 비어 있음)이 유효한 증명의 결론이라는 식의 이 있다 ( 자연 추론 발표에서는 i 개찰구를 명시적으로 기록하지 않고 대신 추론할 수 있는 2차원 표기법을 사용한다.)

자연적 차감 판결의 표준 의미론은 }등이 모두 사실일 때마다[11] 도 사실일 것이라고 주장하는 것이다. 판결은

그리고

어느 한쪽의 증거가 다른 한쪽의 증거에까지 확장될 수 있다는 강한 의미에서 동등하다.

순차 미적분학 시스템

마지막으로, 연속 미적분은 자연적 차감 판단의 형태를 다음과 같이 일반화한다.

시퀀스라고 하는 통사적 물체 개찰구 왼쪽에 있는 공식을 선행이라고 하고, 우측에 있는 공식을 성공 또는 결과라고 하며, 함께 시편 또는 속편이라고 한다.[12] 다시 말해, {\는 공식이고 n{\}과 k 음이 아닌 정수, 즉 왼쪽 또는 오른쪽(또는 둘 다)이 비어 있을 수 있다. 자연 추론에서처럼, 은 그러한 B B이며, 여기서 {\ B(는) 유효한 증명의 결론이다.

시퀀스의 표준 의미론은 모든 이 진실일 때마다 적어도 하나 도 참일 것이라는 주장이다.[13] 그러므로 두 백향목을 모두 비운 빈 속편은 거짓이다.[14] 이것을 표현하는 한 가지 방법은 개찰구 왼쪽에 있는 쉼표는 "and"로, 개찰구 오른쪽에 있는 쉼표는 "or"로 생각해야 한다는 것이다. 속편

그리고

두 시퀀스의 증명이 다른 시퀀스의 증명으로 확장될 수 있다는 강한 의미에서 동등하다.

첫눈에 이 판결 양식의 연장은 이상한 복잡성으로 보일지도 모른다. 그것은 명백한 자연 추론의 단점에 의한 것이 아니며, 처음에는 쉼표가 개찰구 양쪽에서 완전히 다른 의미를 갖는 것처럼 보이는 것이 혼란스럽다. 그러나 고전적인 맥락에서, 연속체의 의미론도 (명제적 tautology에 의해) 다음과 같이 표현될 수 있다.

(A가 하나 이상 거짓이거나 B가 하나 이상 참임)

또는 로서

(A가 모두 진실이고 B가 모두 거짓인 경우는 있을 수 없다.

이러한 공식에서 개찰구 양쪽에 있는 공식의 유일한 차이는 한쪽이 부정된다는 것이다. 따라서 시퀀스에서 오른쪽을 오른쪽으로 스와핑하는 것은 모든 구성 공식을 부정하는 것과 일치한다. 이것은 의미적 차원에서 논리적 부정으로 나타나는 De Morgan의 법칙과 같은 대칭은 시퀀스의 좌우 대칭으로 직접 번역된다는 것을 의미하며, 실제로 접속사(∧)를 처리하기 위한 시퀀스 미적분학의 추론 규칙은 분리( ()를 다루는 사람들의 거울상이다.

많은 논리학자들은 이러한 대칭적 표시는 규칙에서처럼 부정의 고전적 이중성이 뚜렷하지 않은 다른 유형의 증명 시스템보다 논리 구조에 더 깊은 통찰력을 제공한다고 느낀다[citation needed].

자연적 추론과 연속적 미적분학의 구분

겐첸은 자신의 단일 출력 자연 공제 시스템(NK와 NJ)과 다중 출력 연속 미적분 시스템(LK와 LJ)을 극명한 구별을 주장했다. 그는 직관적 자연공제 체계 NJ가 다소 추하다고 썼다.[15] 그는 고전적 자연적 공제 체계 NK에서 배제된 중간이 갖는 특별한 역할은 고전적 순차적 미적분 체계 LK에서 제거된다고 말했다.[16] 그는 고전적 논리(LK 대 NK)의 경우와 마찬가지로 직감적 논리의 경우 순열적 미적분 LJ가 자연적 추론 NJ보다 더 많은 대칭을 주었다고 말했다.[17] 그리고 그는 이러한 이유 외에도 복수의 성공적 공식을 가진 연속 미적분학은 특히 그의 주된 정리("Hauptsatz")[18]를 위해 의도된 것이라고 말했다.

"시퀀트" 단어의 기원

'시퀀트'라는 말은 겐첸의 1934년 논문에서 '시퀀츠'라는 단어에서 따온 말이다.[1] 클레네는 영어로 번역한 것에 대해 다음과 같이 말한다: "젠젠젠은 우리가 '시퀀츠'라고 번역하는 '시퀀츠'라고 말하는데, 우리는 이미 독일어가 '포기'인 어떤 사물의 계승에도 '시퀀스'를 사용했기 때문이다."[19]

논리 공식 증명

석회 미적분학에 의한 증거 찾기 절차를 설명하는 뿌리 나무

환원나무

시퀀스 미적분은 분석표법과 유사하게 명제 논리학에서 공식을 증명하는 도구로 볼 수 있다. 그것은 사소한 공식에 도달할 때까지 논리적 공식을 증명하는 문제를 단순하고 단순한 공식으로 줄일 수 있는 일련의 단계를 제공한다.[20]

다음 공식을 고려하십시오.

이것은 다음과 같은 형태로 쓰여 있는데, 여기서 증명되어야 할 명제는 개찰구 기호 의 오른쪽에 있다

이제 이것을 공리로부터 증명하기보다는 함축의 전제를 가정하고 그 결론을 증명하려고 노력하는 것으로 충분하다.[21] 따라서 다음 시퀀스로 이동한다.

다시 한 번 우측에는 함축성이 포함되며, 그 전제는 그 결론만 입증될 필요가 있도록 추가로 가정될 수 있다.

왼쪽의 주장은 접속사에 의해 관련되는 것으로 가정하므로, 이것은 다음과 같이 대체할 수 있다.

이는 왼쪽의 첫 번째 주장에 대한 분리의 두 경우에서 모두 결론을 입증하는 것과 같다. 따라서 우리는 두 개의 시퀀스를 나눌 수 있다. 여기서 우리는 각각 따로따로 증명해야 한다.

첫 번째 판단의 경우 을(를)as r p 다시 작성하고 시퀀트를 다시 분할하여 다음을 얻는다.

두 번째 시퀀스가 수행되며, 첫 번째 시퀀스는 다음과 같이 더욱 단순화할 수 있다.

이 과정은 항상 양쪽에 원자 공식만 있을 때까지 계속될 수 있다. 그 과정은 오른쪽에 묘사된 바와 같이 뿌리가 있는 나무 그래프로 그래픽으로 설명할 수 있다. 나무의 뿌리는 우리가 증명하고 싶은 공식이다; 잎은 오직 원자 공식으로만 구성된다. 그 나무는 축소 나무로 알려져 있다.[20][22]

개찰구 왼쪽에 있는 항목은 접속사로, 오른쪽에 있는 것은 분리해서 연결되는 것으로 이해한다. 따라서 두 가지 모두 원자 기호로만 구성되었을 때, 오른쪽의 기호 중 적어도 하나라도 왼쪽에 나타나는 경우에만 시퀀스가 자명하게(그리고 항상 참) 받아들여진다.

나무를 따라 진행하는 규칙은 다음과 같다. 한 개의 시퀀스가 둘로 분할될 때마다 나무 꼭지점은 두 개의 하위 정점이 있고, 나무는 분기된다. 또한, 각 측면의 논쟁 순서를 자유롭게 변경할 수 있다. γ과 Δ는 가능한 추가 논쟁을 나타낸다.[20]

자연 공제를 위해 겐첸식 레이아웃에서 사용되는 수평선의 통상적인 용어는 추론선이다.[23]

왼쪽: 오른쪽:

공리:

명제 논리학의 어떤 공식에서 출발하여 일련의 단계에 의해 개찰구의 오른쪽은 원자 기호만 포함할 때까지 처리될 수 있다. 그리고 나서, 왼쪽 측면도 마찬가지야. 모든 논리 연산자는 위의 규칙 중 하나에 나타나며 규칙에 의해 제거되기 때문에 논리 연산자가 남아 있지 않을 때 프로세스는 종료된다. 그 공식은 이미 분해되었다.

따라서 나무 잎의 속편에는 오른쪽의 기호 중 하나가 왼쪽에도 나타나는지 여부에 따라 공리에 의해 증명될 수 있는 원자 기호만 포함되어 있다.

나무의 단계들은 분할이 있을 때마다 나무의 다른 가지들 사이에서 이해되는 결합과 함께 그들이 암시하는 공식의 의미론적 진실 가치를 보존하고 있음을 쉽게 알 수 있다. 또한 공리가 원자 기호에 대한 진리 값의 모든 할당에 대해 진실일 경우에만 증명할 수 있다는 것은 명백하다. 따라서 이 시스템은 고전적인 명제 논리에 대해 건전하고 완전하다.

표준 공리와 관련

시퀀스 미적분은 프리지의 명제 미적분학 또는 얀 우카시오비치의 공리화(그 자체가 표준 힐버트 시스템의 일부)와 같은 명제 미적분의 다른 공리와 관련이 있다. 이것들에서 증명될 수 있는 모든 공식은 감소 트리를 가지고 있다.

이를 다음과 같이 나타낼 수 있다. 명제 미적분학의 모든 증거는 공리와 추론 규칙만을 사용한다. 각 공리 설계의 사용은 참된 논리 공식을 산출하며, 따라서 순차 미적분학에서 증명될 수 있다. 이에 대한 예는 다음과 같다. 위에서 언급된 시스템에서 유일한 추론 규칙은 컷 룰에 의해 구현되는 모드스 폰이다.

시스템 LK

이 절에서는 1934년 겐첸이 도입한 순열 미적분 LK의 규칙을 소개한다.(LK는, 무해하게, "Klassische Prédikatenlogik"를 의미한다.) 이 미적분학의 A(공식) 증명서는 다음 규칙 중 하나를 사용하여 순열에서 앞서 나타나는 순열에서 각각 파생할 수 있는 순열이다.

추론 규칙

다음과 같은 표기법이 사용된다.

  • 【\displaystyle 개찰구로 알려진 \vdash 】 왼쪽의 가정과 오른쪽의 제안을 구분한다.
  • 은 1차 술어 논리 공식(이것을 명제 논리로 제한할 수도 있음)을 나타낸다.
  • , , ,\,\ {\은 공식의 유한(사실, 공식의 순서는 중요하지 않다; 하위섹션 규칙 참조) 순서(문맥락 참조)라고 한다.
    • 왼쪽에 있는 경우 공식의 순서는 결절적으로 간주된다(모두 동시에 유지되는 것으로 가정됨).
    • 오른쪽에 있는 동안 공식의 순서는 분리적으로 간주된다(변수의 할당에 대해 적어도 하나의 공식은 유지되어야 함).
  • 임의의 용어를 의미한다.
  • 은(는) 변수를 나타낸다.
  • 변수가 정량자 {\ 또는 {\displaystyle 의 범위를 벗어나면 공식 내에서 자유롭게 발생한다고 한다
  • 공식 에서 변수 가) 발생할 때마다 t을(를) 대신하여 얻은 공식으로, t }에 대해 자유여야 함을 의미한다 t {\에서 변수가 발생하지 않음)는 [ / 에 바인딩된다.
  • , , , , , : These six stand for the two versions of each of three structural rules; one for use on the left ('L') of a , and the other on 그것의 오른쪽('R') 규칙은 약화를 위한 'W'(좌/우), 수축의 경우 'C', 순열화의 경우 'P'로 약칭된다.

위에 제시된 감소 트리를 따라 진행하기 위한 규칙과는 반대로, 다음 규칙은 공리에서 이론으로, 반대 방향으로 이동하기 위한 것이라는 점에 유의한다. 따라서 이 대칭은 암묵적으로 가정되지 않고 계량화에 관한 규칙이 추가된다는 점을 제외하고, 위 규칙의 정확한 거울상이다.

공리: 잘라내기:

왼쪽 논리 규칙: 올바른 논리 규칙:

왼쪽 구조 규칙: 올바른 구조 규칙:

제한 사항: 규칙 ) ( L) 에서 변수 이(가) 각각의 하위 시퀀스에서 자유롭게 발생해서는 안 된다

직관적인 설명

위의 규칙은 크게 논리적인 그룹과 구조적인 그룹 두 가지로 나눌 수 있다. 각각의 논리규칙은 개찰구 }의 왼쪽이나 오른쪽에 새로운 논리공식을 도입한다 대조적으로 구조규칙은 공식의 정확한 모양을 무시한 채 속절구조에 작용한다. 이 일반적인 체계에 대한 두 가지 예외는 정체성(I)과 (Cut)의 법칙이다.

비록 형식적인 방법으로 명시되어 있지만, 위의 규칙들은 고전적인 논리적인 측면에서 매우 직관적인 읽기를 허용한다. Consider, for example, the rule . It says that, whenever one can prove that can be concluded from some sequence of formulae that contain , then one can also conclude from the (stronger) assumption th (가) 버티고 있다. Likewise, the rule states that, if and suffice to conclude , then from alone one can either still conclude or mus거짓이 아니다. 즉, (가) 버티고 있다. 모든 규칙은 이런 식으로 해석될 수 있다.

정량화 규칙에 대한 직관은 규칙 ( )을 고려하십시오 물론A[ y / (가) 단지 A [ /] {\이(으)라는 사실만으로 결론을 내리는 것은 일반적으로 가능하지 않다. 그러나 변수 y가 다른 곳에 언급되지 않은 경우(즉, 다른 공식에 영향을 미치지 않고 자유롭게 선택될 수 있다)에 A [ / ]{\이(가) y의 어떤 값도 보유한다고 가정할 수 있다. 그렇다면 다른 규칙들은 꽤 간단해야 한다.

규칙들을 술어 논리의 법적 파생에 대한 설명으로 보는 대신에, 사람들은 또한 규칙을 주어진 진술에 대한 증명서 작성에 대한 지침으로 여길 수도 있다. In this case the rules can be read bottom-up; for example, says that, to prove that follows from the assumptions and , it suffices to prove that can be concluded from (와) 에서 각각 결론을 내릴 수 있다 일부 선행조건에 따라 로 분할하는 방법이 명확하지 않지만, 가정에 의한 선행조건은 유한하기 때문에 확인할 수 있는 가능성은 매우 많다 이것은 또한 증명 이론이 어떻게 조합적인 방식으로 증명들에 작용하는 것으로 보일 수 있는지를 보여준다: A 둘 다에 대한 증명이 주어진다면 B에 대한 증빙을 구성할 수 있다

어떤 증거를 찾을 때, 대부분의 규칙들은 이것을 어떻게 하는지에 대한 다소 직접적인 레시피를 제공한다. 컷의 규칙은 다르다: A 이(가) 결론날 수 있고 이 공식도 다른 문장의 결론에 전제될 수 있을 때 공식 이(가) "컷아웃"되고 각각의 파생어가 결합될 수 있다고 명시한다. 증명 하단을 구성할 때, 이것은 을(아래에 전혀 나타나지 않기 때문에) 추측하는 문제를 야기한다. 따라서 컷 엘리미네이션 정리자동화된 추론에서 시퀀스 미적분학의 적용에 결정적이다. 즉, 컷 규칙의 모든 용도는 증거에서 제거될 수 있다고 명시하고 있어, 모든 입증 가능한 시퀀스에는 컷 프리 증명이 주어질 수 있음을 시사한다.

다소 특별한 두 번째 규칙은 정체성의 공리(I)이다. 이것을 직관적으로 읽는 것은 명백하다: 모든 공식은 그 자체를 증명한다. 절단 규칙처럼, 정체성의 공리는 다소 중복된다: 원자 초기 시퀀스의 완전성은 그 규칙이 어떠한 검증 가능성 손실 없이 원자 공식으로 제한될 수 있다고 말한다.

함축성 있는 규칙만 제외하고 모든 규칙에는 거울 동반자가 있다는 것을 준수하십시오. 이는 1차 논리학의 통상적인 언어가 "내포되지 않음" 연결성 포함하지 않는다는 사실을 반영한다. 그러한 결합체를 자연 법칙에 추가하면 미적분학이 완전히 좌우 대칭이 된다.

파생 예

제외된 중간(라틴어로 tertium non datur)의 법칙으로 알려진 " A {\A\lor 의 파생어는 다음과 같다.

다음은 정량자를 포함하는 간단한 사실의 증명이다. 기존 자유 변수를 규칙 ) R 대체하여 사용할 수 없으므로, 역은 사실이 아니며, 상향으로 유도하려고 할 때 거짓을 볼 수 있다는 점에 유의하십시오

For something more interesting we shall prove . It is straightforward to find th자동화된 증명에서 LK의 유용성을 예시하는 e 파생.

These derivations also emphasize the strictly formal structure of the sequent calculus. For example, the logical rules as defined above always act on a formula immediately adjacent to the turnstile, such that the permutation rules are necessary. Note, however, that this is in part an artifact of the presentation, in the original style of Gentzen. A common simplification involves the use of multisets of formulas in the interpretation of the sequent, rather than sequences, eliminating the need for an explicit permutation rule. This corresponds to shifting commutativity of assumptions and derivations outside the sequent calculus, whereas LK embeds it within the system itself.

Relation to analytic tableaux

For certain formulations (i.e. variants) of the sequent calculus, a proof in such a calculus is isomorphic to an upside-down, closed analytic tableau.[25]

Structural rules

The structural rules deserve some additional discussion.

Weakening (W) allows the addition of arbitrary elements to a sequence. Intuitively, this is allowed in the antecedent because we can always restrict the scope of our proof (if all cars have wheels, then it's safe to say that all black cars have wheels); and in the succedent because we can always allow for alternative conclusions (if all cars have wheels, then it's safe to say that all cars have either wheels or wings).

Contraction (C) and Permutation (P) assure that neither the order (P) nor the multiplicity of occurrences (C) of elements of the sequences matters. Thus, one could instead of sequences also consider sets.

The extra effort of using sequences, however, is justified since part or all of the structural rules may be omitted. Doing so, one obtains the so-called substructural logics.

Properties of the system LK

This system of rules can be shown to be both sound and complete with respect to first-order logic, i.e. a statement follows semantically from a set of premises if and only if the sequent can be derived by the above rules.[26]

In the sequent calculus, the rule of cut is admissible. This result is also referred to as Gentzen's Hauptsatz ("Main Theorem").[2][3]

Variants

The above rules can be modified in various ways:

Minor structural alternatives

There is some freedom of choice regarding the technical details of how sequents and structural rules are formalized. As long as every derivation in LK can be effectively transformed to a derivation using the new rules and vice versa, the modified rules may still be called LK.

First of all, as mentioned above, the sequents can be viewed to consist of sets or multisets. In this case, the rules for permuting and (when using sets) contracting formulae are obsolete.

The rule of weakening will become admissible, when the axiom (I) is changed, such that any sequent of the form can be concluded. This means that proves in any context. Any weakening that appears in a derivation can then be performed right at the start. This may be a convenient change when constructing proofs bottom-up.

Independent of these one may also change the way in which contexts are split within the rules: In the cases , and the left context is somehow split into and when going upwards. Since contraction allows for the duplication of these, one may assume that the full context is used in both branches of the derivation. By doing this, one assures that no important premises are lost in the wrong branch. Using weakening, the irrelevant parts of the context can be eliminated later.

Absurdity

One can introduce , the absurdity constant representing false, with the axiom:

Or if, as described above, weakening is to be an admissible rule, then with the axiom:

With , negation can be subsumed as a special case of implication, via the definition .

Substructural logics

Alternatively, one may restrict or forbid the use of some of the structural rules. This yields a variety of substructural logic systems. They are generally weaker than LK (i.e., they have fewer theorems), and thus not complete with respect to the standard semantics of first-order logic. However, they have other interesting properties that have led to applications in theoretical computer science and artificial intelligence.

Intuitionistic sequent calculus: System LJ

Surprisingly, some small changes in the rules of LK suffice to turn it into a proof system for intuitionistic logic.[27] To this end, one has to restrict to sequents with at most one formula on the right-hand side, and modify the rules to maintain this invariant. For example, is reformulated as follows (where C is an arbitrary formula):

The resulting system is called LJ. It is sound and complete with respect to intuitionistic logic and admits a similar cut-elimination proof. This can be used in proving disjunction and existence properties.

In fact, the only two rules in LK that need to be restricted to single-formula consequents are and [28] (and the latter can be seen as a special case of the former, via as described above). When multi-formula consequents are interpreted as disjunctions, all of the other inference rules of LK are actually derivable in LJ, while the offending rule is

This amounts to the propositional formula , a classical tautology that is not constructively valid.

See also

Notes

  1. ^ a b Gentzen 1934, Gentzen 1935.
  2. ^ a b Curry 1977, pp. 208–213, gives a 5-page proof of the elimination theorem. See also pages 188, 250.
  3. ^ a b Kleene 2009, pp. 453, gives a very brief proof of the cut-elimination theorem.
  4. ^ Curry 1977, pp. 189–244, calls Gentzen systems LC systems. Curry's emphasis is more on theory than on practical logic proofs.
  5. ^ Kleene 2009, pp. 440–516. This book is much more concerned with the theoretical, metamathematical implications of Gentzen-style sequent calculus than applications to practical logic proofs.
  6. ^ Kleene 2002, pp. 283–312, 331–361, defines Gentzen systems and proves various theorems within these systems, including Gödel's completeness theorem and Gentzen's theorem.
  7. ^ Smullyan 1995, pp. 101–127, gives a brief theoretical presentation of Gentzen systems. He uses the tableau proof layout style.
  8. ^ Curry 1977, pp. 184–244, compares natural deduction systems, denoted LA, and Gentzen systems, denoted LC. Curry's emphasis is more theoretical than practical.
  9. ^ Suppes 1999, pp. 25–150, is an introductory presentation of practical natural deduction of this kind. This became the basis of System L.
  10. ^ Lemmon 1965 is an elementary introduction to practical natural deduction based on the convenient abbreviated proof layout style System L based on Suppes 1999, pp. 25–150.
  11. ^ Here, "whenever" is used as an informal abbreviation "for every assignment of values to the free variables in the judgment"
  12. ^ Shankar, Natarajan; Owre, Sam; Rushby, John M.; Stringer-Calvert, David W. J. (2001-11-01). "PVS Prover Guide" (PDF). User guide. SRI International. Retrieved 2015-05-29.
  13. ^ For explanations of the disjunctive semantics for the right side of sequents, see Curry 1977, pp. 189–190, Kleene 2002, pp. 290, 297, Kleene 2009, p. 441, Hilbert & Bernays 1970, p. 385, Smullyan 1995, pp. 104–105 and Gentzen 1934, p. 180.
  14. ^ Buss 1998, p. 10
  15. ^ Gentzen 1934, p. 188. "Der Kalkül NJ hat manche formale Unschönheiten."
  16. ^ Gentzen 1934, p. 191. "In dem klassischen Kalkül NK nahm der Satz vom ausgeschlossenen Dritten eine Sonderstellung unter den Schlußweisen ein [...], indem er sich der Einführungs- und Beseitigungssystematik nicht einfügte. Bei dem im folgenden anzugebenden logistischen klassichen Kalkül LK wird diese Sonderstellung aufgehoben."
  17. ^ Gentzen 1934, p. 191. "Die damit erreichte Symmetrie erweist sich als für die klassische Logik angemessener."
  18. ^ Gentzen 1934, p. 191. "Hiermit haben wir einige Gesichtspunkte zur Begründung der Aufstellung der folgenden Kalküle angegeben. Im wesentlichen ist ihre Form jedoch durch die Rücksicht auf den nachher zu beweisenden 'Hauptsatz' bestimmt und kann daher vorläufig nicht näher begründet werden."
  19. ^ Kleene 2002, p. 441.
  20. ^ a b c Applied Logic, Univ. of Cornell: Lecture 9. Last Retrieved: 2016-06-25
  21. ^ "Remember, the way that you prove an implication is by assuming the hypothesis."—Philip Wadler, on 2 November 2015, in his Keynote: "Propositions as Types". Minute 14:36 /55:28 of Code Mesh video clip
  22. ^ Tait WW (2010). "Gentzen's original consistency proof and the Bar Theorem" (PDF). In Kahle R, Rathjen M (eds.). Gentzen's Centenary: The Quest for Consistency. New York: Springer. pp. 213–228.
  23. ^ Jan von Plato, Elements of Logical Reasoning, Cambridge University Press, 2014, p. 32.
  24. ^ Gentzen 1934, pp. 190–193.
  25. ^ Smullyan 1995, p. 107
  26. ^ Kleene 2002, p. 336, wrote in 1967 that "it was a major logical discovery by Gentzen 1934–5 that, when there is any (purely logical) proof of a proposition, there is a direct proof. The implications of this discovery are in theoretical logical investigations, rather than in building collections of proved formulas."
  27. ^ Gentzen 1934, p. 194, wrote: "Der Unterschied zwischen intuitionistischer und klassischer Logik ist bei den Kalkülen LJ und LK äußerlich ganz anderer Art als bei NJ und NK. Dort bestand er in Weglassung bzw. Hinzunahme des Satzes vom ausgeschlossenen Dritten, während er hier durch die Sukzedensbedingung ausgedrückt wird." English translation: "The difference between intuitionistic and classical logic is in the case of the calculi LJ and LK of an extremely, totally different kind to the case of NJ and NK. In the latter case, it consisted of the removal or addition respectively of the excluded middle rule, whereas in the former case, it is expressed through the succedent conditions."
  28. ^ Structural Proof Theory (CUP, 2001), Sara Negri and Jan van Plato

References

External links