PL wiki

자연 연역

  • 연역 체계

자연 연역은 논리 체계의 종류 중 하나로, 도입과 소거 규칙을 통해 정의되는 특징을 가지고 있다. 게르하르트 겐첸이 그의 1935년 논문 [13]에서 시퀀트 계산과 함께 발표하였다.

도입과 소거 규칙

도입 규칙 (introduction rule)은 개별 명제들에 대한 판단으로부터 이들로 구성된 복합적인 명제에 대한 판단을 이끌어 내는 추론 규칙이다. 반대로 소거 규칙 (elimination rule)은 복합적인 명제에 대한 판단에서 이를 구성하는 개별 명제에 대한 판단을 이끌어 낸다.

아래에 소개된 추론규칙에선 [4, 5, 8]등을 따라 명제 ϕ와 판단 ϕ true를 구분하였다.

연언

연언은 한개의 도입 규칙 I와 두개의 소거 규칙 E1,E2를 가진다. ϕ trueψ trueϕψ true I ϕψ trueϕ true E1 ϕψ trueψ true E2 

선언

선언은 두개의 도입 규칙 I1,I2와 한개의 소거 규칙 E를 가진다. ϕ trueϕψ true I1 ψ trueϕψ true I2 ϕψ trueϕ trueuχ trueψ truevχ trueχ true Eu,v 

함언

함언은 도입 규칙 I와 소거 규칙 E를 가진다. ϕ trueuψ trueϕψ true Iu ϕψ trueϕ trueψ true E 

참 연결사

참 연결사는 도입 규칙 I를 가지며 소거 규칙이 존재하지 않는다.  true I 

거짓 연결사

거짓 연결사는 도입 규칙이 존재하지 않으며 소거 규칙 E를 가진다.  trueχ true E 

부정

부정은 도입 규칙 ¬I와 소거 규칙 ¬E를 가진다. ϕ trueu true¬ϕ true ¬Iu ¬ϕ trueϕ true true ¬E 

부정 ¬ϕϕ과 동치이기 때문에, 부정 연결사를 별도로 넣지 않는 경우도 있다.

보편 양화사

ϕa truex.ϕx true I x.ϕx trueϕt true E  I 규칙의 고유변수(eigenvariable) ax.ϕx나 다른 가정에 나타나선 안된다.

존재 양화사

ϕt truex.ϕx true I x.ϕx trueϕa trueuχ trueχ true Eu  E 규칙의 고유변수 ax.ϕxχ, 다른 가정에 나타나선 안된다.

NJ

겐첸의 자연 연역 체계 NJ는 ,,,,¬,,로 구성된 직관주의적 1차 자연 연역 체계 이다.

예시

다음은 겐첸의 논문에서 제시된 NJ-증명의 예시이다. P(QR) true u P true v PQ true I1 P true v PR true I1 (PQ)(PR) true I QR true w Q true E1 PQ true I2 QR true w R true E2 PR true I2 (PQ)(PR) true I (PQ)(PR) true Ev,w P(QR)(PQ)(PR) true Iu 

x.y.Fxy trueuy.Fay truevFab trueEx.Fxb trueIy.x.Fxy trueIy.x.Fxy trueEv(x.y.Fxy)(y.x.Fxy) trueIu

¬x.Fx trueuFa truevx.Fx trueI true¬E¬Fa true¬Ivy.¬Fy trueI(¬x.Fx)(y.¬Fy) trueIu

NK

겐첸은 NJ에 배중률을 추가한 고전적 자연 연역 체계 NK를 제시하였다. 즉 다음과 같은 공리꼴을 도입한다. ϕ¬ϕ true LEM 

고전적 체계를 얻기 위해, 배중률과 동치인 이중 부정 소거(double negation elimination)를 추론 규칙으로 추가하는 방법도 있다. ¬¬ϕ trueϕ true ¬¬E 

그러나 이중 부정 소거 규칙은 부정의 도입 규칙으로부터 정당화 되지 않음에 주의하여야 한다. 겐첸은 이에 대해 다음과 같이 언급했다[3].

However, such a schema still falls outside the framework of the NJ-inference figures, because it represents a new elimination of the negation whose admissibility does not follow at all from our method of introducing the ¬-symbol by the ¬-I.

국소적 건전성과 국소적 완전성

자연 연역의 각 연결사들은 국소적 건전성(local soundness)과 국소적 완전성(local completeness)을 만족한다 [6]. 국소적 건전성은 어떤 증명에서 한 연결사를 도입하고 즉시 소거한 경우 도입과 소거 규칙 쌍을 제거한 더 직접적인 증명을 얻을 수 있음을 말한다. 이러한 증명의 변환을 국소적 축약(local reduction) 이라고 한다. 반대로 국소적 완전성은 어떤 증명에서 한 연결사를 소거시키고 다시 도입해 본래의 명제에 대한 증명을 얻을 수 있음을 말한다. 이러한 증명의 변환을 국소적 확장(local expansion) 이라고 한다.

본 문서에서는 국소적 축약을 R, 국소적 확장을 E로 표기한다.

연언

Dϕ trueEψ trueϕψ true I ϕ true E1 RDϕ true Dϕ trueEψ trueϕψ true I ψ true E2 REψ true Dϕψ trueEDϕψ trueϕ true E1 Dϕψ trueψ true E2 ϕψ true I 

선언

Dϕ trueϕψ true I1 ϕ trueuEχ trueψ truevFχ trueχ true Eu,v RDϕ trueEχ true Dψ trueϕψ true I2 ϕ trueuEχ trueψ truevFχ trueχ true Eu,v RDψ trueFχ true Dϕψ trueEDϕψ trueϕ trueuϕψ trueI1ψ truevϕψ trueI2ϕψ trueEu,v

함언

ϕ trueuDψ trueϕψ trueIuEϕ trueψ trueEREϕ trueDψ true Dϕψ trueEDϕψ trueϕ trueuψ trueEϕψ trueIu

참 연결사

참 연결사는 소거 규칙이 없으므로 국소적 건전성을 자명하게 만족한다. D trueE true I 

거짓 연결사

거짓 연결사는 도입 규칙이 없으므로 국소적 건전성을 자명하게 만족한다. D trueED true trueE

보편 양화사

Dϕa truex.ϕx trueIϕt trueERD[t/a]ϕt true Dx.ϕx trueEDx.ϕx trueϕaEx.ϕxI

존재 양화사

Dϕt truex.ϕx true I ϕa trueuEχ trueχ true Eu RDϕt trueE[t/a]χ true Dx.ϕx trueEDx.ϕx trueϕa trueux.ϕx trueIx.ϕx true Eu 

검증과 사용

검증(verification)과 국소적 축약이 불가능하고, 국소적 확장이 최대한으로 적용된 증명이다 [4, 7]. 검증은 사용(use)과 함께 서로귀납적으로 정의된다. 프로그래밍 언어론 관점에서 검증은 정규형, 사용은 중립형에 대응된다.

본 문서에서는 [7]를 따라 ϕ의 검증을 ϕ로, ϕ의 사용을 ϕ로 표기한다.

연언

ϕψϕψ I ϕψϕ E1 ϕψψ E2 

선언

ϕϕψ I1 ψϕψ I2 ϕψϕuχψvχχ Eu,v 

함언

ϕuψϕψ Iu ϕψϕψ E 

참 연결사

 I 

거짓 연결사

χ E 

보편 양화사

ϕax.ϕx I x.ϕxϕt E 

존재 양화사

ϕtx.ϕx I x.ϕxϕauχχ Eu 

명제 변수

PP  

전역적 건전성과 전역적 완전성

전역적 건전성

전역적 건전성은 시퀀트 계산에서 자름의 admissibility, 즉 자름-제거 정리와 대응된다.

Ifϕand  ϕψthenψ

전역적 완전성

전역적 건전성은 시퀀트 계산에서 항등 규칙의 admissibility에 대응된다. ϕϕ

참고문헌

[1]
Gerhard Gentzen. 1935. Untersuchungen über das logische schließen. I. Mathematische Zeitschrift 39, (December 1935), 176–210. https://doi.org/10.1007/BF01201353
[2]
Gerhard Gentzen. 1935. Untersuchungen über das logische schließen. II. Mathematische Zeitschrift 39, (December 1935), 405–431. https://doi.org/10.1007/BF01201363
[3]
Gerhard Gentzen. 1969. Investigations into logical deduction. In The collected papers of gerhard gentzen, M. E. Szabo (ed.). 68–131.
[4]
Per Martin-Löf. 1996. On the meanings of the logical constants and the justifications of the logical laws. Nordic Journal of Philosophical Logic 1, 1 (1996), 11–60. Retrieved from http://www.hf.uio.no/ifikk/forskning/publikasjoner/tidsskrifter/njpl/vol1no1/meaning.pdf
[5]
Frank Pfenning. 2023. Lecture notes on natural deduction. (2023). Retrieved from https://www.cs.cmu.edu/~fp/courses/15317-s23/lectures/02-natded.pdf
[6]
Frank Pfenning. 2023. Lecture notes on harmony. (2023). Retrieved from https://www.cs.cmu.edu/~fp/courses/15317-s23/lectures/03-harmony.pdf
[7]
Frank Pfenning. 2023. Lecture notes on verifications. (2023). Retrieved from https://www.cs.cmu.edu/~fp/courses/15317-s23/lectures/05-verifications.pdf
[8]
Frank Pfenning and Rowan Davies. 2001. A judgmental reconstruction of modal logic. Mathematical Structures in Computer Science 11, 4 (2001), 511–540. https://doi.org/10.1017/S0960129501003322