자연공제

Natural deduction

논리증명 이론에서 자연 추론논리적 추리가 "자연적" 추론 방식과 밀접한 관련이 있는 추론 규칙에 의해 표현되는 일종의 증명 미적분학이다. 는 연역적 추론의 논리적 법칙을 표현하기 위해 가능한 한 공리를 사용하는 힐버트식 시스템과 대비된다.

동기

자연 공제는 힐버트, 프레지, 러셀(예: 힐버트 시스템 참조)의 시스템에 공통적인 연역적 추론의 공리화에 대한 불만족이라는 맥락에서 성장했다. 그러한 공리학은 러셀화이트헤드가 수학적 논문인 프린키니아 매스매티카에서 가장 잘 사용하였다. 1926년 폴란드에서 열린 일련의 세미나에서 보다 자연적인 논리 처리를 주창했던 우카시오비츠에 의해 자극을 받아, 자우코프스키는 보다 자연적인 추론을 정의하기 위해 가장 먼저 1929년에 도식화된 표기법을 사용했고, 이후 1934년과 1935년에 일련의 논문에서 그의 제안을 갱신했다.[1] 그의 제안은 렘몬시스템 L이라고 불리는 변종에게 준 피치 스타일의 미적분학(또는 피치의 도표)이나 서페스의 방법과 같은 다른 논조로 이어졌다.

현대적 형태의 자연 공제는 독일의 수학자 게르하르트 겐첸이 1934년 괴팅겐 대학의 수리과학 교수진에게 전달한 논문에서 독자적으로 제안했다.[2] 자연공제(또는 독일어로 동등한 자연공제 Schließen)라는 용어는 이 논문에서 다음과 같이 만들어졌다.

Ich Wolte nunechst einmal einnen Formalismus aufstellen, der dem Wirklichen Schlieenen Möglichst nah Kommt. 그래서 ergab sich ein "Kalkül des naturlichen Schließens".[3]
(먼저 나는 실제 추리에 가능한 한 가까이 다가가는 형식주의를 건설하고 싶었다. 따라서 "자연적 차감의 계산"이 일어났다.

겐젠은 수론의 일관성을 확립하려는 욕망에 동기부여가 되었다. 그는 자연적인 추론을 위해 직접적으로 일관성 있는 결과인 컷 탈락 정리인 하우프트사츠에 필요한 주요 결과를 증명할 수 없었다. 이러한 이유로 그는 자신의 대안 체계인 순열 미적분학을 도입하였는데, 그 결과 고전적 논리나 직관적 논리로 하우프트사츠를 증명하였다. 1961년과 1962년 일련의 세미나에서 프라위츠는 자연 공제 캘커리에 대한 포괄적인 요약을 했고, 겐첸의 작품 중 상당 부분을 속편 캘커리로 자연 공제 틀로 운반했다. 1965년 그의 모노그래프 자연공제: 증명이론적 연구[4] 자연공제에 관한 참고서적이 되는 것이었고, 모달2차 논리 출원을 포함했다.

자연적 추론에서는 추론 규칙을 반복적으로 적용함으로써 전제의 집합에서 명제를 추론한다. 이 글에서 제시된 시스템은 겐첸이나 프라위츠의 공식의 사소한 변형이지만, 논리적인 판단과 연결에 대한 마틴 뢰프의 설명을 더 잘 따르는 것이다.[5]

판단과 제안

판단은 알 수 있는 것, 즉 지식의 대상이다. 그것을 아는 사람이 있다면 그것은 명백하다.[6] 그러므로 "비가 내리고 있다"는 것은 실제로 비가 내리고 있다는 것을 아는 사람에게는 명백한 판단이다. 이 경우 창문 밖을 보거나 집을 나서면 판결에 대한 증거를 쉽게 찾을 수 있을 것이다. 그러나 수학 논리학에서 증거는 종종 직접적으로 관찰할 수 있는 것이 아니라 보다 기본적인 명백한 판단으로부터 추론된다. 추론의 과정은 증거를 구성하는 것이다. 즉, 그것에 대한 증거가 있으면 판단이 명백하다.

논리학에서 가장 중요한 판단은 "A는 참이다"라는 형식이다. A라는 글자는 명제를 대표하는 어떤 표현을 의미하며, 따라서 진실 판단은 "A는 명제"라는 보다 원초적인 판단을 필요로 한다. 많은 다른 판단이 연구되어 왔다. 예를 들어, "A는 거짓이다"(고전 논리 참조), "A는 시간 t에 참이다"(시간 논리 참조), "A는 반드시 이다" 또는 "A는 유형 τ" (프로그래밍 언어유형 이론 참조), "A는 가용 자원으로부터 달성 가능하다"(선형 논리 참조), 그리고 많은 o먼저, 우리는 "A명제"와 "A"으로 각각 약칭되는 "A는 참"이라는 가장 간단한 두 가지 판단에 대해 우리 스스로 고민해야 한다.

판결문 "소개서"는 A의 유효증거의 구조를 규정하며, 이는 다시 명제의 구조를 규정한다. 이러한 이유로, 이 판결에 대한 추론규칙때때로 형성규칙으로 알려져 있다. 예를 들어, 만약 우리에게 두 가지 명제 A와 B(즉, "A 소품"과 "B 소품"이 명백하다)가 있다면, 우리는 " B {\로 상징적으로 쓰여진 복합 명제 A와 B를 형성한다. 우리는 이것을 추론 규칙의 형태로 쓸 수 있다.

추론 규칙을 보다 간명하게 만들기 위해 괄호를 생략하는 경우:

이 추론 규칙은 개략적인 것이다: AB는 어떤 표현으로도 인스턴스화할 수 있다. 추론 규칙의 일반적인 형태는 다음과 같다.

여기서 각 는 판단이고 추론 규칙은 "이름"으로 명명된다. 선 위의 판단은 전제로 알려져 있으며, 선 아래의 판단은 결론이다. Other common logical propositions are disjunction (), negation (), implication (), and the logical constants truth () and falsehood (). 그들의 형성 규칙은 아래에 있다.

도입 및 제거

이제 우리는 "A true" 판단에 대해 논한다. 결론에 논리적 결합을 도입하는 추론 규칙을 도입 규칙이라고 한다. 접속사 도입, 즉 명제 AB에 대한 "A와 B 참"을 결론짓기 위해서는 "A 참"과 "B 참"에 대한 증거가 필요하다. 추론 규칙으로:

그러한 규칙에서 사물은 명제라는 것을 이해해야 한다. 즉, 위의 규칙은 실제로 다음을 가리키는 약칭이다.

또한 다음과 같이 기록될 수 있다.

이 형태에서 편성 규칙에 의해 첫 번째 전제가 충족될 수 있으며, 이전 양식의 처음 두 전제가 주어진다. 이 글에서 우리는 "제안" 판단이 이해되는 곳에 이를 것이다. 무효인 경우에는 어떤 전제로부터도 진리를 이끌어낼 수 있다.

명제의 진리가 하나 이상의 방법으로 확립될 수 있는 경우, 해당 결합자는 복수의 도입 규칙을 가진다.

무효의 경우, 즉 허위의 경우 도입 규칙이 없다는 점에 유의한다. 그러므로 사람은 결코 단순한 판단에서 거짓을 추론할 수 없다.

도입 규칙에 대한 이중은 복합 명제에 대한 정보를 그 구성원에 대한 정보로 분해하는 방법을 설명하는 제거 규칙이다. 따라서 "A B true"에서 "A true"와 "B true"로 결론을 내릴 수 있다.

추론 규칙의 사용의 예로서, 접속사의 공통성을 고려한다. 만약 A b B가 사실이라면, BA는 진실이다; 이 파생은 낮은 추론의 전제들이 차상위 추론의 결론과 일치하도록 추론 규칙을 구성함으로써 그려질 수 있다.

우리가 지금까지 보아온 추론 수치는 시사 도입이나 분리 제거의 규칙을 기술하기에 충분하지 않다; 이것들을 위해서, 우리는 가상의 파생에 대한 더 일반적인 개념이 필요하다.

가상의 파생

수학 논리학의 만연된 연산은 가정으로부터 추론하는 것이다. 예를 들어 다음과 같은 파생을 고려하십시오.

이 파생은 B의 진리를 그와 같이 정립하지 않는다. 오히려 다음과 같은 사실을 정립한다.

A ∧ (B C)이 참이라면 B는 참이다.

논리학에서는 "A ∧ (B ∧ C)가 사실이라고 가정하면 우리는 B가 사실임을 보여준다"고 말하고, 즉 "B true"는 가정된 판단 "A ( (B c C) true"에 달려 있다. 이것은 가상의 파생어로, 우리는 다음과 같이 쓰고 있다.

해석은 다음과 같다: "B true는 A (B true C) true에서 파생될 수 있다." 물론 이 구체적인 예에서 우리는 실제로 "A ∧ (B C) true"에서 "B true"의 유래를 알고 있지만, 일반적으로 우리는 선험자가 그 유래를 알지 못할 수도 있다. 가정적 파생의 일반적인 형태는 다음과 같다.

각 가상의 파생에는 상선에 쓰여진 선행적 파생(Di)과 하단에 쓰여진 성공적 판단(J)의 집합이 있다. 각 전제 자체가 가상의 파생일 수도 있다.(단순함을 위해 우리는 판단을 전제 없는 파생으로 취급한다.)

가상적 판단의 개념은 함축적 의미로서 내면화된다. 도입 및 제거 규칙은 다음과 같다.

도입규정에서는 u라는 선행자가 결론에서 제대한다. 이것은 가설의 범위를 구분하기 위한 메커니즘이다. 가설의 유일한 존재 이유는 "B true"를 확립하기 위한 것이다. 다른 목적으로는 사용할 수 없으며, 특히 도입부 이하에서는 사용할 수 없다. 예를 들어 "A ⊃ (B (A B) true)"의 파생어를 고려하십시오.

이 완전한 파생은 불만족스러운 전제가 없다. 그러나 하위 파생은 가상이다. 예를 들어 "B ⊃ (A ∧ B) true"의 유래는 선행 "A true"(u라는 이름)를 가진 가상이다.

가상의 파생어로, 우리는 이제 분리를 위한 제거 규칙을 작성할 수 있다.

다시 말해 A b B가 진실이고, 우리는 "A true"와 "B true"에서 모두 "C true"를 도출할 수 있다면, C는 정말 진실이다. 이 규칙은 "" 또는 "B 참"을 적용하지 않는다는 점에 유의하십시오. 제로 아리의 경우, 즉 거짓의 경우, 다음과 같은 제거 규칙을 얻는다.

이것은 다음과 같이 읽힌다: 거짓이 진실이라면, 어떤 명제 C도 진실이다.

부정은 함축성과 비슷하다.

도입 규칙은 가설 u의 이름을 모두 배출하며, 성공 p,명제 p는 결론 A에서 발생해서는 안 된다. 이러한 규칙들이 도식적이기 때문에 도입 규칙의 해석은 "진실"에서 "진실"이라는 모든 명제 p에 대해 우리가 도출할 수 있다면, "진실"이 아닌 "진실"이어야 한다. 소거의 경우, A와 A가 모두 참인 것으로 판명되면 모순이 있는데, 이 경우 모든 명제 C가 참이다. 함축적 규칙과 부정적 규칙들이 너무 비슷하기 때문에 A와 A 이 동등하지 않다는 것을, 즉 각각이 다른 것들로부터 파생될 수 있다는 것을 꽤 쉽게 알 수 있어야 한다.

일관성, 완전성 및 정상적인 형태

어떤 이론은 거짓이 증명할 수 없는 경우(무 가정으로부터) 일관성이 있고, 모든 정리나 그 부정이 논리의 추론 규칙을 사용하여 증명될 수 있다면 완전하다고 한다. 이것들은 전체 논리에 대한 진술이며, 대개 모형의 개념과 관련이 있다. 그러나 추론 규칙에 대한 순수하게 통사적 점검이며 모델에 대한 호소가 필요 없는 일관성과 완전성에 대한 국지적 관념이 있다. 첫 번째는 국소 환원성이라고도 하는 국소적 일관성인데, 연결체의 도입에 따른 즉시 제거를 포함하는 모든 파생은 이 우회 없이 동등한 파생으로 변할 수 있다고 말한다. 그것은 제거 규칙의 강도에 대한 점검이다: 그것들은 너무 강해서 그들의 구내에 이미 포함되어 있지 않은 지식을 포함시켜서는 안 된다. 예를 들어, 접속사를 생각해 보십시오.

--------- u ----------------------------------------------------------------------------------------------------------------------------------- 진실1 
--------- u 진실 

지역 완성도는 제거 규칙이 결합체를 도입 규칙에 적합한 형태로 분해할 정도로 충분히 강하다고 말한다. 다시 접속사의 경우:

------------------------------- A B 사실 
----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------12 

이러한 개념은 커리-하워드 이소모르피즘을 이용하여 람다 미적분학에서 β-감소(베타 감소) and-변환(에타 변환)에 정확히 대응한다. 지역적 완전성에 의해, 우리는 모든 파생이 주요 결합체가 도입되는 동등한 파생으로 변환될 수 있음을 본다. 사실, 전체 유도체가 소개에 따른 이 제거 순서를 준수한다면, 그것은 정상이라고 한다. 정상적인 파생에서 모든 제거는 소개보다 먼저 일어난다. 대부분의 로직에서, 모든 파생은 정상 형태라고 불리는 동등한 정상적 파생을 가진다. 1961년 다그 프라위츠에 의해 가장 두드러진 문헌에 그러한 회계처리가 존재하긴 하지만, 정상적인 형태의 존재는 일반적으로 자연적 공제를 통해서만 증명하기 어렵다.[7] 이것을 컷 프리 시퀀스 미적분학 프레젠테이션을 통해 간접적으로 보여주는 것이 훨씬 더 쉽다.

1차 및 고차 확장

1차 시스템 요약

앞 절의 논리는 일변도 논리의 예로서, 즉 하나의 목적어인 명제를 갖는 논리의 예다. 이 간단한 프레임워크의 많은 연장이 제안되었다. 이 섹션에서는 두 번째 종류의 개인 또는 용어로 확장될 것이다. 좀 더 정확히 말하면, t가 도식화된 곳에 "t는 용어"(또는 "t 용어")라는 새로운 종류의 판단을 추가할 것이다. 변수계수 가능한 집합 V, 함수 기호의 계수 가능한 집합 F를 수정하고 다음과 같은 형성 규칙으로 항을 구성한다.

그리고

명제의 경우, 우리는 세 번째로 셀 수 있는 술어의 집합 P를 고려하고, 다음과 같은 형성 규칙을 가진 용어들에 대해 원자 술어를 정의한다.

비록 그 연구 분야의 초점은 자연적 추론과 상당히 다르지만, 처음의 두 형성 규칙은 용어 대수학 및 모델 이론에서 정의한 용어와 사실상 동일한 용어의 정의를 제공한다. 형성의 제3규칙은 1차 논리학에서와 같이 원자공식을 효과적으로 정의하고, 다시 모형 이론에서 정의한다.

여기에 정량화된 명제를 위한 표기법을 정의하는 한 쌍의 형성 규칙이 추가된다. 보편적(일반적)과 실존적(실존적) 정량화를 위한 한 쌍:

범용 계량기에는 다음과 같은 도입 및 제거 규칙이 있다.

실존적 정량기에는 다음과 같은 도입 및 제거 규칙이 있다.

이 규칙에서 [t/x] A라는 표기법은 A에서 x의 모든 (보이는) 인스턴스(instance)에 대해 t를 대체하는 것을 의미하며, 포획을 회피한다.[8] 이름에서 위첨자 앞부분이 방전된 구성요소를 나타내는 것과 같이, a라는 용어는 iI의 결론에서 발생할 수 없으며(그런 용어는 고유변수매개변수로 알려져 있다), eE에서 u와 v라는 가설이 가상의 파생에서 두 번째 전제로 국부화된다. 이전 절의 명제 논리는 해독할 수 있었지만, 정량자를 추가하면 그 논리는 해독할 수 없게 된다.

지금까지 정량화된 확장은 1차적인 것으로, 명제를 정량화된 물체의 종류와 구별한다. 고차 논리는 다른 접근방식을 취하며 하나의 종류의 명제만을 가지고 있다. 정량자는 구성 규칙에 반영되는 것과 매우 동일한 종류의 명제를 계량 영역으로 가지고 있다.

고차 논리를 위한 도입과 제거 양식에 대한 논의는 이 글의 범위를 벗어난다. 1차 로직과 고차 로직 사이에 있는 것이 가능하다. 예를 들어, 2차 논리는 두 가지 종류의 명제를 가지고 있는데, 하나는 용어에 대해 계량하는 것이고, 다른 하나는 제1종류의 명제에 대해 계량하는 것이다.

자연공제의 상이한 표시

나무와 같은 프리젠테이션

가정적 판단을 내면화하는 데 사용되는 겐첸의 주석 방출을 피할 수 있는 것은 증거를 A의 참된 판단의 나무 대신 γ ⊢ ⊢A의 나무로 나타냄으로써 피할 수 있다.

순차 프리젠테이션

Jaśkowski의 자연적 차감 표현은 피치식 미적분학(또는 피치의 도표)이나 서페스의 방법 등 다른 표기들로 이어졌는데, 이 중 렘몬시스템 L이라는 변종을 주었다. 표로 더 정확하게 기술되는 그러한 표시 시스템은 다음과 같은 내용을 포함한다.

  • 1940: 교과서에서 Quine은[9] Suppes의 1957 라인 번호 표기법을 예상하면서 대괄호 안의 라인 번호에 의한 선행 종속성을 나타냈다.
  • 1950: 교과서에서, Quine(1982년, 페이지 241–255)은 각 증명서의 왼쪽에 하나 이상의 별표를 사용하여 의존성을 나타내는 방법을 보여주었다. 이것은 클린의 세로 막대에 해당한다. (Quine의 별표 표기법이 1950년 원본에 등장했는지, 이후 판에 추가되었는지는 완전히 확실하지 않다.)
  • 1957: Suppes(1999, 페이지 25–150)의 교과서에서 입증된 실제 논리 정리에 대한 소개. 이것은 각 선의 왼쪽에 있는 라인 번호에 의한 의존성(즉 선행 제안)을 나타냈다.
  • 1963: 스톨(1979, 페이지 183–190, 215–2199)은 자연적 공제 추론 규칙에 기초한 순차적 논리적 원칙 라인의 선행 종속성을 나타내기 위해 일련의 라인 번호를 사용한다.
  • 1965: 렘몬(1965)의 교과서 전체는 서피스(Suppes)에 근거한 방법을 이용한 논리증거의 도입이다.
  • 1967: 교과서에서 클레네(2002, 페이지 50–58, 128–130)는 두 종류의 실용적인 논리 증거를 간략히 보여주었는데, 하나는 각 행의 왼쪽에 있는 선행 명제의 명시적 인용구를 사용한 것이고, 다른 하나는 의존성을 나타내기 위해 왼쪽의 수직 막대를 사용한 것이다.[10]

증명 및 유형 이론

지금까지 자연공제의 제시가 증명이라는 형식적 정의를 내리지 않고 명제의 본질에 집중되어 왔다. 증거의 개념을 공식화하기 위해, 우리는 가상의 파생어의 표시를 약간 수정한다. 우리는 선행계약에 증거변수(일부 카운트 가능한 변수 집합 V로부터)로 라벨을 붙이고, 실제 증명으로 성공한 것을 장식한다. 선행 조건이나 가설은 개찰구(開 turn)를 통해 성공자와 분리된다. 이 수정은 때때로 국부적인 가설의 이름으로 진행된다. 아래의 도표는 그 변화를 요약한 것이다.

---- 어... - 어12... ---- un12 J Jn J ⋮ J. 
u1:J1, u2:J2, ..., un:Jn ⊢ J. 

가설의 집합은 정확한 구성이 관련이 없을 때 Ⅱ로 기록된다. 증거를 분명히 하기 위해 우리는 증거 없는 판단인 'A true'에서 '(A true)'의 판단인 '(A true)'로 넘어가는데, 이 판단은 상징적으로 'π : A true'라고 씌어 있다. 표준 접근법에 따라, 증명들은 "증거 증명" 판결에 대한 그들 자신의 형성 규칙으로 명시된다. 가장 간단한 증거는 라벨로 표시된 가설을 사용하는 것이다. 이 경우 증거는 라벨 그 자체다.

u ∈ V ------proof-F u proof 
--------------------------------------------------------------------------------------------------------------------- 

간결성을 위해 이 글의 나머지 부분에 진실된 판단 라벨을 생략한다. 즉, " " ⊢ ⊢ : A"라고 써야 한다. 일부 커넥티브에 대해 명확한 증거를 가지고 다시 살펴보도록 하자. 접속사에서는, 접속사 증명서의 형태를 발견하기 위해 도입 규칙 iI를 살펴본다: 두 결막의 증명 쌍이어야 한다. 따라서 다음과 같다.

π1 증명 π2 증명 ------------------- 쌍-F (π1, π2) 증명 
γ1 ⊢ : A γ2 : : B ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- : : : : : A12 ∧ B 

제거 규칙 ∧E와1 ∧E는2 왼쪽 또는 오른쪽 결막 중 하나를 선택하므로, 증명은 첫 번째(fst)와 두 번째(snd)의 한 쌍의 투영이다.

π 증명 ------------ fst-Fst fst st 증명 
γ ⊢ : : A ∧ B ------------ ∧E1 γ f fst : A 
π 증명 ------------- snd-F snd 증명 
γ ⊢ : : A ∧ B -------- ---E2 sn sn snd : B 

함축적 의미를 위해, 도입 양식은 가설을 위치시키거나 결합시킨다. 이는 방출된 라벨에 해당한다. 규칙에서 " ", u:A"는 추가 가설 u와 함께 가설 γ의 집합을 의미한다.

π 증명 ------------------------ --F u. proof 
γ, u:A ⊢ : B ----------------------------------------------- ---I --- : :. : : A ⊃ B 
π1 증명 π2 증명 ---------------- 증명 ------------------ app-F π12 증명 
γ1 ⊢ : : A b B γ2 : A ---------------------------------------- --E γ12 ⊢ : : B 

증거를 명시적으로 사용할 수 있게 되면, 사람들은 증거에 대해 조작하고 추론할 수 있다. 증거에 대한 핵심 작업은 다른 증거에 사용된 가정을 위해 한 증거를 대체하는 것이다. 이것은 일반적으로 대체 정리라고 알려져 있으며, 두 번째 판단의 깊이(또는 구조)를 유도로 증명할 수 있다.

치환정리
γ1 ⊢ : A와 γ, u2:A ⊢ : B, u1/u] π2 : B.

지금까지 판결 "γ : : : A"는 순전히 논리적인 해석을 가지고 있었다. 유형 이론에서 논리적인 견해는 객체에 대한 더 계산적인 견해와 교환된다. 논리적 해석에서 명제는 현재 유형으로, 증거는 람다 미적분학에서 프로그램으로 간주된다. 따라서 "π : A"의 해석은 "프로그램 π에는 타입 A가 있다"이다. 논리 커넥티브는 다른 판독값도 주어진다: 접속사를 제품(×), 함수의 화살표로 함축(→) 등으로 본다. 그러나 그 차이는 단지 외관일 뿐이다. 유형 이론은 형성, 도입, 제거 규칙의 측면에서 자연적인 공제 제시를 가지고 있다. 사실, 독자는 이전 절에서 단순 유형 이론으로 알려진 것을 쉽게 재구성할 수 있다.

논리와 유형 이론의 차이는 주로 유형(제안)에서 프로그램(증거)으로 초점을 옮기는 것이다. 유형 이론은 주로 프로그램의 변환성 또는 축소성에 관심이 있다. 모든 유형에는 수정할 수 없는 형식의 표준 프로그램이 있다. 이러한 프로그램은 표준 형식이나 값으로 알려져 있다. 만일 모든 프로그램이 표준적인 형태로 축소될 수 있다면, 타입 이론은 정상화(또는 약하게 정규화)되고 있다고 한다. 정론적 형태가 독특하다면, 그 이론은 강하게 정상화되고 있다고 한다. Normalisability는 대부분의 비종교적 유형 이론에서 드문 특징으로, 논리 세계로부터 큰 이탈이다. (거의 모든 논리적 파생은 동등한 정상적인 파생을 가지고 있다는 것을 상기하라.) 그 이유를 요약하면, 재귀적 정의를 인정하는 타입 이론에서는, 결코 가치로 감소하지 않는 프로그램을 쓰는 것이 가능하다; 그러한 반복적인 프로그램은 일반적으로 어떤 유형이든 주어질 수 있다. 특히 루핑 프로그램에는 "사실무근"이라는 논리적인 증거는 없지만 ⊥형이 있다. 이러한 이유로, 명제는 유형으로서, 프로그램 패러다임으로서의 증명들은 한 방향으로만 작용한다. 만약 그렇다면, 유형 이론을 논리로 해석하는 것은 일반적으로 일관되지 않은 논리를 제공한다.

예: 종속형 이론

논리학처럼 유형 이론은 1차 버전과 고차 버전을 포함하여 많은 확장성과 변형을 가지고 있다. 종속형 이론으로 알려진 한 가지 분기는 다수의 컴퓨터 지원 증명 시스템에 사용된다. 종속형 이론은 정량자가 프로그램 자체보다 범위가 넓어지게 한다. 이러한 정량화된 형식은 ∀과 ∃ 대신 π과 σ으로 표기되며, 다음과 같은 형성 규칙을 가지고 있다.

γ ⊢ A형 γ, x:A ⊢ B형 ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- f-F ⊢ ⊢ x x:A B형 
γ ⊢ A형 type, x:A ⊢ B형 ------------------------------------------- ---------F γ ⊢ x:A B형 

이러한 유형은 도입 규칙과 제거 규칙에서 볼 수 있는 화살과 제품 유형의 일반화다.

γ, x:A ⊢ : B ------------------- --I i ⊢ x. π : πx:A. b 
γ1 ⊢ : : xx:A B12 γ2 ⊢ : : A ----------------------------------------------------------- --- --- --- : [---/x2] B 
γ ⊢ : A1 γ2, x:A ⊢ : B ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- x x12 : ::A b 
γ ⊢ : : xx:A B ---------------- --E1fst a : A 
γ ⊢ : : xx:A B --------------------------------------------------- -- sn2 snd π : [fst π/x] B 

완전한 일반성의 종속형 이론은 매우 강력하다. 프로그램의 유형에서 프로그램의 거의 모든 상상할 수 있는 속성을 직접적으로 표현할 수 있다. 이러한 일반성은 비싼 값으로 온다. 즉, 활자체크가 불분명하거나(확장형 이론), 확장형 추론이 더 어렵다(내성형 이론). 이러한 이유로 일부 종속형 이론은 임의 프로그램에 대한 정량화를 허용하지 않고 오히려 주어진 디커블 인덱스 영역(예: 정수, 문자열 또는 선형 프로그램)의 프로그램으로 제한한다.

종속형 이론은 프로그램에 따라 유형이 달라지는 것을 허용하기 때문에, 자연스러운 질문은 프로그램이 유형이나 다른 조합에 의존하는 것이 가능한가 하는 것이다. 그런 질문에 대한 답은 여러 종류가 있다. 형식 이론에서 인기 있는 접근방식은 파라메트릭 다형성이라고도 알려진 유형에 대해 프로그램이 정량화되도록 하는 것이다. 이 중 크게 두 가지가 있다. 유형과 프로그램이 분리되어 있으면, 사전 다형성이라고 불리는 다소 더 잘 동작하는 시스템을 얻게 된다. 프로그램과 유형의 구분이 모호해지면, 하나의 오타이가 된다.ns 고차 로직의 형식-유형 아날로그(충돌성 다형성이라고도 함). 문헌에는 의존성과 다형성의 다양한 조합이 고려되어 왔는데, 가장 유명한 것은 헨크 바렌트레트람다 큐브였다.

논리와 유형론의 교차점은 넓고 활발한 연구 영역이다. 새로운 로직은 일반적으로 논리 프레임워크라고 알려진 일반적인 유형의 이론적 환경으로 공식화된다. 건축의 미적분학이나 LF와 같은 인기 있는 현대 논리 프레임워크는 높은 순서의 종속형 이론에 기초하고 있으며, 결정성과 표현력 측면에서 다양한 절충이 있다. 이러한 논리적 프레임워크 자체는 항상 자연적 공제 시스템으로 지정되며, 이는 자연적 공제 접근법의 다용성을 증명한다.

클래식 및 모달 로직

간단히 말해서, 지금까지 제시된 논리학은 직관적이었다. 고전적 논리배제된 중간이라는 추가적인 공리 또는 원리로 직관적 논리를 확장한다.

어떤 명제 p에 대해서도, 명제 p ∨ ¬p는 사실이다.

이 진술은 명백하게 도입이나 제거가 아니다; 사실 그것은 두 개의 뚜렷한 연결고리를 포함한다. 겐첸의 배제된 중간의 원래 처리는 힐베르트헤이팅의 시스템에서 이미 유사한 형태로 존재했던 다음의 세 가지 (동등) 공식 중 하나를 규정했다.

-------------------------------------------------------------------------------------------------------------------1 
¬A true ----------- XM2 A true 
--------u trueA true p true ----- XM3u, p A true 

(XM은3 E로 표현된 XM에2 불과하다.) 배제된 중간을 이러한 취급하는 것은, 순수주의자의 입장에서 반대할 수 있을 뿐만 아니라, 정상적인 형태의 정의에 추가적인 합병증을 야기한다.

도입과 제거 규칙만으로도 비교적 만족스러운 고전 자연 공제의 처리는 1992년 패리고트byμ라 불리는 고전 람다 미적분 형태로 처음 제안했다. 그의 접근방법에 대한 핵심 통찰은 진실 중심적 판단 A 참된 판단을 속편 미적분을 연상시키는 보다 고전적인 개념으로 대체하는 것이었다: 국소화된 형태로 he ⊢ A 대신에 γ ⊢ Δ를 δ과 유사한 명제 모음 Δ와 함께 사용했다. δ은 접속사로서 취급되었고, Δ Δ는 불분해로서 취급되었다. 이 구조는 기본적으로 고전적인 시퀀스 캘커리로부터 직접 해제되지만, λμ의 혁신은 LISP와 그 후손에서 볼 수 있는 콜록 또는 투척/캐치 메커니즘의 측면에서 고전적인 자연적 공제 증명들에 연산적인 의미를 부여하는 것이었다. (제1종 제어 참조)

또 다른 중요한 연장은 모달과 진리의 기본적인 판단 이상의 것을 필요로 하는 다른 로직들을 위한 것이었다. 이것들은 1965년 프라위츠에 의해 자연적 공제 방식으로 알레르드 모달 로직 S4S5에 대해 처음 설명되었고,[4] 그 이후로 많은 관련 작업을 축적해 왔다. 간단한 예를 들면, 모달 논리 S4는 진실과 관련하여 범주화된 하나의 새로운 판단인 "유효한"을 요구한다.

"B true" 형식의 가정 하에 "A true"가 아닌 경우, "A true"가 된다.

이 범주형 판단은 다음과 같은 도입 및 제거 규칙을 가진 단항 결합형 ◻A(필요 A)로 내면화된다.

유효한 -------- ◻I ◻ A true 
◻ 참 -------- ◻E 참 

"A valid"라는 전제에는 정의 규칙이 없으며 대신 유효성에 대한 범주형 정의가 대신 사용된다. 이 모드는 가설이 명백할 때 국소화된 형태로 명확해진다. 우리는 "Ω;Ω ⊢ hypothes true"를 쓰는데 여기서 where은 전과 같이 참된 가설을 포함하고 Ω은 유효한 가설을 포함하고 있다. 오른쪽에는 "A true"라는 단 하나의 판단이 있을 뿐이다. "Ω ⊢ A 유효"는 정의상 "Ω;; ⊢ true"와 같기 때문에 여기서는 타당성이 필요하지 않다. 도입 및 제거 양식은 다음과 같다.

Ω;⋅ ⊢ π : A true ------------------------------------ --I Ω; box 박스 box : A true 
Ω;γ ⊢ π : ◻ A true -------------------------------------------------------------------------------------------------------------------------- un unbox : A true 

모달 가설은 가설 규칙과 대체 정리에 대한 그들만의 버전을 가지고 있다.

-------------------------------- valid-hyp Ω, u: (A valid); γ ⊢ u u : A true 
모달 치환 정리
Ω;; ⊢ π1 : A true and Ω, u: (a valid), γ2 ⊢ ⊢ : C true, Ω;γ [π1/u] π2 : C true.

판단을 여러 가지 영역 또는 다각형 문맥으로 알려진, 구별되는 가설 집합으로 분리하는 이 프레임워크는 매우 강력하고 확장 가능하다; 그것은 많은 다양한 모달 로직과 선형 및 기타 하위구조 로직에도 적용되어 몇 가지 예를 들어준다. 그러나 모달 논리학의 시스템은 자연적 차감에서 직접 공식화할 수 있는 것이 비교적 적다. 이러한 시스템에 대한 입증-이론적 특성을 부여하기 위해 라벨링 또는 깊은 추론의 시스템과 같은 확장.

공식에 라벨을 추가하면 규칙이 적용되는 조건을 훨씬 더 세밀하게 제어할 수 있어 라벨링된 차감의 경우처럼 분석 표의 더 유연한 기법이 적용될 수 있다. 라벨은 또한 Kripke 의미론에서 세계의 명칭을 지정할 수 있다; 심슨(1993)은 혼합 로직의 자연적 공제 공식화에서 Kripke 의미론에서 모달 로직의 프레임 조건을 추론 규칙으로 변환하는 데 영향력 있는 기법을 제시한다. 스투파(2004)는 S5와 B와 같은 모달 로직들에 에이브론이나 포틴저의 과장급, 벨납의 표시 논리 등 많은 증명 이론의 적용을 조사한다.

다른 기본 접근 방식과의 비교

시퀀스 미적분학

이열 미적분은 수학 논리의 기초로서 자연 추론의 주요한 대안이다. 자연 추론에서 정보의 흐름은 양방향이다: 제거 규칙은 탈구축에 의해 아래로, 도입 규칙은 조립에 의해 정보를 위로 흐른다. 따라서 자연적 공제 증빙은 순전히 상향식 또는 하향식 판독을 가지고 있지 않기 때문에 증명 검색에서 자동화에 적합하지 않다. 이 사실을 다루기 위해 1935년 겐첸처음에는 술어 논리의 일관성을 명확히 하기 위한 기술적 장치로 의도했음에도 불구하고 그의 속편 미적분을 제안하였다. 클렌은 1952년 저서 《변태학 개론》에서 현대식 미적분학을 최초로 공식화했다.[11]

연속 미적분학에서 모든 추론 규칙들은 순전히 상향식 읽기를 가지고 있다. 추론규칙은 개찰구 양쪽의 요소에 적용할 수 있다.(자연적 추론과 구별하기 위해 이 글은 속편에는 오른쪽 태크 ⊢ 대신 이중 화살표 ⇒을 사용한다. 자연공제의 도입규칙은 연속 미적분학에서 올바른 규칙으로 간주되며 구조적으로 매우 유사하다. 반면에 제거 규칙은 연속 미적분학에서 왼쪽 규칙으로 바뀐다. 예를 들어, 분리를 고려해 보십시오. 올바른 규칙은 다음과 같다.

γ ⇒ A -------- ∨R1 γ A ∨ B 
γ ⇒ B -------- ∨R2 γ A ∨ B 

왼쪽:

γ, u:A ⇒ C γ, v:B ⇒ C ------------------------------------------------------------------------------------------- w: (A ∨ B) ⇒ C 

지역화된 형태로 자연 공제의 deductionE 규칙을 상기한다.

γ A ∨ B γ, u:A ⊢ C γ, v:B ⊢ C --------------------------------------------------------------------------------------------------------------------------------------------------------------------- eE e C 

∨E에서 전제의 계승자인 명제 A B는 왼쪽 규칙 ∨L에서의 결론에 대한 가설로 변한다. 따라서, 왼쪽 규칙은 일종의 역삭제 규칙으로 볼 수 있다. 이 관찰은 다음과 같이 설명할 수 있다.

자연 공제 연속 미적분학
 ----- 하이프엘림. 규칙 ↓ ----------------------------------------------------------------------------------- 결론을 규칙으로 정하다.
 ----------------------------------------------------------------------------------------------------

시퀀스 미적분학에서는 최초 시퀀스에 도달할 때까지 좌우 규칙을 잠금 단계로 수행하는데, 이는 자연 공제의 제거와 도입 규칙의 만남 지점에 해당한다. 이러한 초기 규칙들은 피상적으로 자연 추론의 가설 규칙과 유사하지만, 연속적인 미적분학에서는 좌우 명제의 전환이나 악수를 묘사한다.

----------- init Ⅱ, u:A ⇒ A 

순열 미적분과 자연 추론의 일치성은 건전성과 완전성 이론의 한 쌍으로, 둘 다 귀납적 논증을 통해 증명할 수 있다.

⇒ wrt의 건전성.
만약 γ ⇒ A이면 γ ⊢ ⊢ A.
⇒ wrt의 완전성.
만약 γ ⊢ A이면 γ ⇒ ⇒ A.

이러한 이론에 따르면, 동일한 명제 집합이 진실이기 때문에, 연속적인 미적분학이 진리의 개념을 바꾸지 않는다는 것은 분명하다. 따라서, 사람들은 연속 미적분학 유도에서 이전과 같은 증명 물체를 사용할 수 있다. 예를 들어, 접속사를 생각해 보십시오. 올바른 규칙은 도입 규칙과 사실상 동일하다.

연속 미적분학 자연 공제
γ1 ⇒ : A γ2 : : B ------------------------------------------------------- ---------------- ---------------- ---------------- (----------------, π12) : A ∧ B 
γ1 ⊢ : A γ2 : : B ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- : : : : : A12 ∧ B 

그러나 왼쪽 규칙은 해당 제거 규칙에서 수행되지 않는 일부 추가 대체 작업을 수행한다.

연속 미적분학 자연 공제
γ, u:A ⇒ : C ------------------------------------------------------- ∧ (, v1: (A ∧ B) ⇒ [fst v/u] π : C 
γ ⊢ : : A ∧ B ------------ ∧E1 γ f fst : A 
γ, u:B ⇒ : C ----------------------------------------------------------- ( ( (, (A2 ∧ B) ⇒ [snd v/u] π : C 
γ ⊢ : : A ∧ B -------- ---E2 sn sn snd : B 

그러므로 연속 미적분학에서 생성되는 증명의 종류는 자연적 추론의 증상과 다소 다르다. 이열 미적분은 β-정규 normal-긴 형태라고 알려진 형태로 증명서를 생성하는데, 이는 자연적 공제 증명의 정상적인 형태를 표준적으로 나타낸 것에 해당한다. 만약 어떤 사람이 자연 공제를 그 자체로 사용하여 이러한 증명들을 기술하려고 한다면, 사람들은 소위 말하는 계산간 미적분학(John Byrnes가 처음 기술한 것)을 얻게 되는데, 이것은 자연 공제를 위한 정상적인 형태의 개념을 공식적으로 정의하는 데 사용될 수 있다.

자연 공제의 대체 정리는 연속 미적분학의 절단이라고 알려진 구조 규칙이나 구조 정리의 형태를 취한다.

절단(부위)
γ1 ⇒ : A와 γ, u2:A ⇒ : C, γ1/u] π2 : C.

대부분의 잘 행동한 논리학에서, 컷은 메타 테오렘으로 증명할 수 있지만 추론 규칙으로서 불필요하다; 컷 규칙의 불필요한 부분은 보통 컷 제거라고 알려진 계산 과정으로 제시된다. 이것은 자연 공제를 위한 흥미로운 응용을 가지고 있다; 대개는 한정되지 않은 수의 사례 때문에 자연 공제를 통해 특정 재산을 직접 증명하는 것은 극도로 지루하다. 예를 들어, 주어진 명제는 자연적 차감에서 증명할 수 없다는 것을 보여주는 것을 고려해보자. 단순한 귀납적 주장은 자의적 명제를 도입할 수 있는 likeE나 E와 같은 규칙 때문에 실패한다. 그러나 우리는 자연적 추론에 관해서 순열 미적분학이 완성되어 있다는 것을 알고 있으므로 순열 미적분학에서 이러한 비도덕성을 보이기에 충분하다. 이제, 추론 규칙으로 컷을 사용할 수 없다면, 모든 시퀀스 규칙들은 오른쪽이나 왼쪽의 결합체를 도입하기 때문에, 최종 결론에서 시퀀스 파생의 깊이는 커넥티드들에 의해 완전히 경계된다. 따라서 고려해야 할 경우의 수가 한정되어 있을 뿐이며, 각각의 경우는 전적으로 결론의 하위 제안으로 구성되기 때문에, 실현가능성을 보여주는 것이 훨씬 더 쉽다. 이것의 간단한 예는 글로벌 일관성 정리인데, ":⋅ ⊥ true"는 증명할 수 없다. 시퀀스 미적분 버전에서는, 결론으로서 「 " ⇒ ⊥」을 가질 수 있는 규칙이 없기 때문에, 이것은 명백하게 사실이다! 증명 이론가들은 종종 그러한 특성 때문에 절단되지 않은 연속 미적분 제형에 대해 일하는 것을 선호한다.

참고 항목

메모들

  1. ^ Jaowskikowski 1934.
  2. ^ 겐첸 1934년, 겐첸 1935년.
  3. ^ 겐첸 1934, 페이지 176.
  4. ^ a b 1965년 프라위츠 2006년
  5. ^ 마틴 뢰프 1996.
  6. ^ 이것은 마틴 뢰프 1996, 페이지 15에 인용된 볼자노 때문이다.
  7. ^ 그의 책 Prawitz 1965, Prawitz 2006도 보라.
  8. ^ 대체 개념에 대한 자세한 내용은 람다 미적분학 기사를 참조하십시오.
  9. ^ 퀴네(1981년). 선행 종속성에 대한 Quine의 선 번호 표기법은 특히 91-93페이지를 참조하십시오.
  10. ^ 클레네 자연공제 제도의 특별한 장점은 명제 미적분과 술어 미적분 모두에 대한 추론 규칙의 타당성을 증명한다는 것이다. 2002, 페이지 44–45, 118–119를 참조하라.
  11. ^ 클레네 2009, 페이지 440-516. Kleene 1980도 참조하십시오.

참조

외부 링크