자연 연역
- 연역 체계
자연 연역은 논리 체계의 종류 중 하나로, 도입과 소거 규칙을 통해 정의되는 특징을 가지고 있다. 게르하르트 겐첸이 그의 1935년 논문 [1–3]에서 시퀀트 계산과 함께 발표하였다.
도입과 소거 규칙
도입 규칙 (introduction rule)은 개별 명제들에 대한 판단으로부터 이들로 구성된 복합적인 명제에 대한 판단을 이끌어 내는 추론 규칙이다. 반대로 소거 규칙 (elimination rule)은 복합적인 명제에 대한 판단에서 이를 구성하는 개별 명제에 대한 판단을 이끌어 낸다.
아래에 소개된 추론규칙에선 [4, 5, 8]등을 따라 명제
연언
연언은 한개의 도입 규칙
선언
선언은 두개의 도입 규칙
함언
함언은 도입 규칙
참 연결사
참 연결사는 도입 규칙
거짓 연결사
거짓 연결사는 도입 규칙이 존재하지 않으며 소거 규칙
부정
부정은 도입 규칙
부정
보편 양화사
존재 양화사
NJ
겐첸의 자연 연역 체계 NJ는
예시
다음은 겐첸의 논문에서 제시된 NJ-증명의 예시이다.
NK
겐첸은 NJ에 배중률을 추가한 고전적 자연 연역 체계 NK를 제시하였다. 즉 다음과 같은 공리꼴을 도입한다.
고전적 체계를 얻기 위해, 배중률과 동치인 이중 부정 소거(double negation elimination)를 추론 규칙으로 추가하는 방법도 있다.
그러나 이중 부정 소거 규칙은 부정의 도입 규칙으로부터 정당화 되지 않음에 주의하여야 한다. 겐첸은 이에 대해 다음과 같이 언급했다[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) 이라고 한다.
본 문서에서는 국소적 축약을
연언
선언
함언
참 연결사
참 연결사는 소거 규칙이 없으므로 국소적 건전성을 자명하게 만족한다.
거짓 연결사
거짓 연결사는 도입 규칙이 없으므로 국소적 건전성을 자명하게 만족한다.
보편 양화사
존재 양화사
검증과 사용
검증(verification)과 국소적 축약이 불가능하고, 국소적 확장이 최대한으로 적용된 증명이다 [4, 7]. 검증은 사용(use)과 함께 서로귀납적으로 정의된다. 프로그래밍 언어론 관점에서 검증은 정규형, 사용은 중립형에 대응된다.
본 문서에서는 [7]를 따라
연언
선언
함언
참 연결사
거짓 연결사
보편 양화사
존재 양화사
명제 변수
전역적 건전성과 전역적 완전성
전역적 건전성
전역적 건전성은 시퀀트 계산에서 자름의 admissibility, 즉 자름-제거 정리와 대응된다.
전역적 완전성
전역적 건전성은 시퀀트 계산에서 항등 규칙의 admissibility에 대응된다.