자연 연역

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

도입과 소거 규칙

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

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

연언

연언은 한개의 도입 규칙 \(\wedge I\)와 두개의 소거 규칙 \(\wedge E_1, \wedge E_2\)를 가진다. \[ \newcommand{\true}[1] {#1 \ \text{true}} \begin{prooftree} \AxiomC{ $\true{\phi}$ } \AxiomC{ $\true{\psi}$ } \RightLabel{ $\wedge I$ } \BinaryInfC{ $\true{\phi \wedge \psi}$ } \end{prooftree} \quad \begin{prooftree} \AxiomC{ $\true{\phi \wedge \psi}$ } \RightLabel{ $\wedge E_1$ } \UnaryInfC{ $\true{\phi}$ } \end{prooftree} \quad \begin{prooftree} \AxiomC{ $\true{\phi \wedge \psi}$ } \RightLabel{ $\wedge E_2$ } \UnaryInfC{ $\true{\psi}$ } \end{prooftree} \]

선언

선언은 두개의 도입 규칙 \(\vee I_1, \vee I_2\)와 한개의 소거 규칙 \(\vee E\)를 가진다. \[ \newcommand{\Hyp}[2] {\AxiomC{}\RightLabel{#1}\UnaryInfC{#2}} \newcommand{\HypJ}[3] {\Hyp{#1}{#2}\noLine\UnaryInfC{$\vdots$}\noLine\UnaryInfC{#3}} \begin{prooftree} \AxiomC{ $\true{\phi}$ } \RightLabel{ $\vee I_1$ } \UnaryInfC{ $\true{\phi \vee \psi}$ } \end{prooftree} \quad \begin{prooftree} \AxiomC{ $\true{\psi}$ } \RightLabel{ $\vee I_2$ } \UnaryInfC{ $\true{\phi \vee \psi}$ } \end{prooftree} \quad \begin{prooftree} \AxiomC{ $\true{\phi \vee \psi}$ } \HypJ{$u$}{$\true{\phi}$}{$\true{\chi}$} \HypJ{$v$}{$\true{\psi}$}{$\true{\chi}$} \RightLabel{ $\vee E^{u,v}$ } \TrinaryInfC{ $\true{\chi}$ } \end{prooftree} \]

함언

함언은 도입 규칙 \({\to} I\)와 소거 규칙 \({\to} E\)를 가진다. \[ \begin{prooftree} \HypJ{$u$}{$\true{\phi}$}{$\true{\psi}$} \RightLabel{ ${\to} I^u$ } \UnaryInfC{ $\true{\phi \to \psi}$ } \end{prooftree} \quad\quad\qquad \begin{prooftree} \AxiomC{ $\true{\phi \to \psi}$ } \AxiomC{ $\true{\phi}$ } \RightLabel{ ${\to} E$ } \BinaryInfC{ $\true{\psi}$ } \end{prooftree} \]

참 연결사

참 연결사는 도입 규칙 \(\top I\)를 가지며 소거 규칙이 존재하지 않는다. \[ \begin{prooftree} \AxiomC{ } \RightLabel{ $\top I$ } \UnaryInfC{ $\true{\top}$ } \end{prooftree} \]

거짓 연결사

거짓 연결사는 도입 규칙이 존재하지 않으며 소거 규칙 \(\bot E\)를 가진다. \[ \begin{prooftree} \AxiomC{ $\true{\bot}$ } \RightLabel{ $\bot E$ } \UnaryInfC{ $\true{\chi}$ } \end{prooftree} \]

부정

부정은 도입 규칙 \(\neg I\)와 소거 규칙 \(\neg E\)를 가진다. \[ \begin{prooftree} \HypJ{$u$}{$\true{\phi}$}{$\true{\bot}$} \RightLabel{ $\neg I^u$ } \UnaryInfC{ $\true{\neg \phi}$ } \end{prooftree} \quad\quad\quad \begin{prooftree} \AxiomC{ $\true{\neg \phi}$ } \AxiomC{ $\true{\phi}$ } \RightLabel{ $\neg E$ } \BinaryInfC{ $\true{\bot}$ } \end{prooftree} \]

부정 \(\neg \phi\)는 \(\phi \to \bot\)과 동치이기 때문에, 부정 연결사를 별도로 넣지 않는 경우도 있다.

보편 양화사

\[ \begin{prooftree} \AxiomC{ $\true{\phi a}$ } \RightLabel{ $\forall I$ } \UnaryInfC{ $\true{\forall x. \phi x}$ } \end{prooftree} \quad \begin{prooftree} \AxiomC{ $\true{\forall x. \phi x}$ } \RightLabel{ $\forall E$ } \UnaryInfC{ $\true{\phi t}$ } \end{prooftree} \] \(\forall I\) 규칙의 고유변수(eigenvariable) \(a\)는 \(\forall x. \phi x\)나 다른 가정에 나타나선 안된다.

존재 양화사

\[ \begin{prooftree} \AxiomC{ $\true{\phi t}$ } \RightLabel{ $\exists I$ } \UnaryInfC{ $\true{\exists x. \phi x}$ } \end{prooftree} \quad \begin{prooftree} \AxiomC{ $\true{\exists x. \phi x}$ } \HypJ{$u$}{$\true{\phi a}$}{$\true{\chi}$} \RightLabel{ $\exists E^u$ } \BinaryInfC{ $\true{\chi}$ } \end{prooftree} \] \(\exists E\) 규칙의 고유변수 \(a\)는 \(\exists x. \phi x\)와 \(\chi\), 다른 가정에 나타나선 안된다.

NJ

겐첸의 자연 연역 체계 NJ는 \(\wedge, \vee, \to, \bot, \neg, \forall, \exists\)로 구성된 직관주의적 1차 자연 연역 체계 이다.

예시

다음은 겐첸의 논문에서 제시된 NJ-증명의 예시이다. \[ \begin{prooftree} \Hyp{ $u$ }{ $\true{P \vee (Q \wedge R)}$ } \Hyp{ $v$ }{ $\true{P}$ } \RightLabel{ $\vee I_1$ } \UnaryInfC{ $\true{P \vee Q}$ } \Hyp{ $v$ }{ $\true{P}$ } \RightLabel{ $\vee I_1$ } \UnaryInfC{ $\true{P \vee R}$ } \RightLabel{ $\wedge I$ } \BinaryInfC{ $\true{(P \vee Q) \wedge (P \vee R)}$ } \Hyp{ $w$ }{ $\true{Q \wedge R}$ } \RightLabel{ $\wedge E_1$ } \UnaryInfC{ $\true{Q}$ } \RightLabel{ $\vee I_2$ } \UnaryInfC{ $\true{P \vee Q}$ } \Hyp{ $w$ }{ $\true{Q \wedge R}$ } \RightLabel{ $\wedge E_2$ } \UnaryInfC{ $\true{R}$ } \RightLabel{ $\vee I_2$ } \UnaryInfC{ $\true{P \vee R}$ } \RightLabel{ $\wedge I$ } \BinaryInfC{ $\true{(P\vee Q)\wedge(P\vee R)}$ } \RightLabel{ $\vee E^{v,w}$ } \TrinaryInfC{ $\true{(P\vee Q)\wedge(P\vee R)}$ } \RightLabel{ ${\to} I^u$ } \UnaryInfC{ $\true{P \vee (Q \wedge R) \to (P\vee Q)\wedge(P\vee R)}$ } \end{prooftree} \]

\[ \begin{prooftree} \Hyp{$u$}{$\true{\exists x. \forall y. Fxy}$} \Hyp{$v$}{$\true{\forall y. Fay}$} \RL{$\forall E$} \UIC{$\true{Fab}$} \RL{$\exists I$} \UIC{$\true{\exists x. Fxb}$} \RL{$\forall I$} \UIC{$\true{\forall y. \exists x. Fxy}$} \RL{$\exists E^v$} \BIC{$\true{\forall y. \exists x. Fxy}$} \RL{${\to} I^u$} \UIC{$\true{(\exists x. \forall y. Fxy) \to (\forall y. \exists x. Fxy)}$} \end{prooftree} \]

\[ \begin{prooftree} \Hyp{$u$}{$\true{\neg \exists x. Fx}$} \Hyp{$v$}{$\true{Fa}$} \RL{$\exists I$} \UIC{$\true{\exists x. Fx}$} \RL{$\neg E$} \BIC{$\true{\bot}$} \RL{$\neg I^v$} \UIC{$\true{\neg Fa}$} \RL{$\forall I$} \UIC{$\true{\forall y. \neg Fy}$} \RL{${\to} I^u$} \UIC{$\true{(\neg \exists x. Fx) \to (\forall y. \neg Fy)}$} \end{prooftree} \]

NK

겐첸은 NJ에 배중률을 추가한 고전적 자연 연역 체계 NK를 제시하였다. 즉 다음과 같은 공리꼴을 도입한다. \[ \begin{prooftree} \AXC{} \RL{ $\mathrm{LEM}$ } \UIC{ $\true{\phi \vee \neg \phi}$ } \end{prooftree} \]

고전적 체계를 얻기 위해, 배중률과 동치인 이중 부정 소거(double negation elimination)를 추론 규칙으로 추가하는 방법도 있다. \[ \begin{prooftree} \AxiomC{ $\true{\neg\neg\phi}$ } \RightLabel{ $\neg\neg E$ } \UnaryInfC{ $\true{\phi}$ } \end{prooftree} \]

그러나 이중 부정 소거 규칙은 부정의 도입 규칙으로부터 정당화 되지 않음에 주의하여야 한다. 겐첸은 이에 대해 다음과 같이 언급했다[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) 이라고 한다.

본 문서에서는 국소적 축약을 \(\Longrightarrow_R\), 국소적 확장을 \(\Longrightarrow_E\)로 표기한다.

연언

\[ \newcommand{\Deriv}[2] {\AXC{#1} \noLine \UIC{#2}} \begin{prooftree} \Deriv{ $\mathcal{D}$ }{ $\true{\phi}$ } \Deriv{ $\mathcal{E}$ }{ $\true{\psi}$ } \RL{ $\wedge I$ } \BIC{ $\true{\phi \wedge \psi}$ } \RL{ $\wedge E_1$ } \UIC{ $\true{\phi}$ } \end{prooftree} \quad\Longrightarrow_R\quad \begin{prooftree} \Deriv{ $\mathcal{D}$ }{ $\true{\phi}$ } \end{prooftree} \] \[ \begin{prooftree} \Deriv{ $\mathcal{D}$ }{ $\true{\phi}$ } \Deriv{ $\mathcal{E}$ }{ $\true{\psi}$ } \RL{ $\wedge I$ } \BIC{ $\true{\phi \wedge \psi}$ } \RL{ $\wedge E_2$ } \UIC{ $\true{\psi}$ } \end{prooftree} \quad\Longrightarrow_R\quad \begin{prooftree} \Deriv{ $\mathcal{E}$ }{ $\true{\psi}$ } \end{prooftree} \] \[ \begin{prooftree} \Deriv{ $\mathcal{D}$ }{ $\true{\phi \wedge \psi}$ } \end{prooftree} \quad\Longrightarrow_E\quad \begin{prooftree} \Deriv{ $\mathcal{D}$ }{ $\true{\phi \wedge \psi}$ } \RL{ $\wedge E_1$ } \UIC{ $\true{\phi}$ } \Deriv{ $\mathcal{D}$ }{ $\true{\phi \wedge \psi}$ } \RL{ $\wedge E_2$ } \UIC{ $\true{\psi}$ } \RL{ $\wedge I$ } \BIC{ $\true{\phi \wedge \psi}$ } \end{prooftree} \]

선언

\[ \begin{prooftree} \Deriv{ $\mathcal{D}$ }{ $\true{\phi}$ } \RL{ $\vee I_1$ } \UIC{ $\true{\phi \vee \psi}$ } \Hyp{$u$}{ $\true{\phi}$ } \noLine \UIC{$\mathcal{E}$} \noLine \UIC{ $\true{\chi}$ } \Hyp{$v$}{ $\true{\psi}$ } \noLine \UIC{$\mathcal{F}$} \noLine \UIC{ $\true{\chi}$ } \RL{ $\vee E^{u,v}$ } \TIC{ $\true{\chi}$ } \end{prooftree} \qquad\qquad\Longrightarrow_R\quad \begin{prooftree} \Deriv{$\mathcal{D}$}{ $\true{\phi}$ } \noLine \UIC{$\mathcal{E}$} \noLine \UIC{ $\true{\chi}$ } \end{prooftree} \] \[ \begin{prooftree} \Deriv{ $\mathcal{D}$ }{ $\true{\psi}$ } \RL{ $\vee I_2$ } \UIC{ $\true{\phi \vee \psi}$ } \Hyp{$u$}{ $\true{\phi}$ } \noLine \UIC{$\mathcal{E}$} \noLine \UIC{ $\true{\chi}$ } \Hyp{$v$}{ $\true{\psi}$ } \noLine \UIC{$\mathcal{F}$} \noLine \UIC{ $\true{\chi}$ } \RL{ $\vee E^{u,v}$ } \TIC{ $\true{\chi}$ } \end{prooftree} \qquad\qquad\Longrightarrow_R\quad \begin{prooftree} \Deriv{$\mathcal{D}$}{ $\true{\psi}$ } \noLine \UIC{$\mathcal{F}$} \noLine \UIC{ $\true{\chi}$ } \end{prooftree} \] \[ \begin{prooftree} \Deriv{$\mathcal{D}$}{$\true{\phi\vee\psi}$} \end{prooftree} \quad\Longrightarrow_E\quad \begin{prooftree} \Deriv{$\mathcal{D}$}{$\true{\phi\vee\psi}$} \Hyp{$u$}{$\true{\phi}$} \RL{$\vee I_1$} \UIC{$\true{\phi\vee\psi}$} \Hyp{$v$}{$\true{\psi}$} \RL{$\vee I_2$} \UIC{$\true{\phi\vee\psi}$} \RL{$\vee E^{u,v}$} \TIC{$\true{\phi\vee\psi}$} \end{prooftree} \]

함언

\[ \begin{prooftree} \Hyp{$u$}{$\true{\phi}$} \noLine \UIC{$\mathcal{D}$} \noLine \UIC{$\true{\psi}$} \RL{${\to}I^u$} \UIC{$\true{\phi \to \psi}$} \Deriv{$\mathcal{E}$}{$\true{\phi}$} \RL{${\to}E$} \BIC{$\true{\psi}$} \end{prooftree} \qquad\qquad\Longrightarrow_R\quad \begin{prooftree} \Deriv{$\mathcal{E}$}{ $\true{\phi}$ } \noLine \UIC{$\mathcal{D}$} \noLine \UIC{ $\true{\psi}$ } \end{prooftree} \] \[ \begin{prooftree} \Deriv{$\mathcal{D}$}{$\true{\phi\to\psi}$} \end{prooftree} \quad\Longrightarrow_E\quad \begin{prooftree} \Deriv{$\mathcal{D}$}{$\true{\phi\to\psi}$} \Hyp{$u$}{$\true{\phi}$} \RL{${\to}E$} \BIC{$\true{\psi}$} \RL{${\to}I^u$} \UIC{$\true{\phi\to\psi}$} \end{prooftree} \]

참 연결사

참 연결사는 소거 규칙이 없으므로 국소적 건전성을 자명하게 만족한다. \[ \begin{prooftree} \Deriv{$\mathcal{D}$}{$\true{\top}$} \end{prooftree} \quad\Longrightarrow_E\quad \begin{prooftree} \AXC{ } \RL{ $\top I$ } \UIC{ $\true{\top}$ } \end{prooftree} \]

거짓 연결사

거짓 연결사는 도입 규칙이 없으므로 국소적 건전성을 자명하게 만족한다. \[ \begin{prooftree} \Deriv{$\mathcal{D}$}{$\true{\bot}$} \end{prooftree} \quad\Longrightarrow_E\quad \begin{prooftree} \Deriv{$\mathcal{D}$}{$\true{\bot}$} \RL{$\bot E$} \UIC{$\true{\bot}$} \end{prooftree} \]

보편 양화사

\[ \begin{prooftree} \Deriv{$\mathcal{D}$}{$\true{\phi a}$} \RL{$\forall I$} \UIC{$\true{\forall x. \phi x}$} \RL{$\forall E$} \UIC{$\true{\phi t}$} \end{prooftree} \quad\Longrightarrow_R\quad \begin{prooftree} \Deriv{$\mathcal{D}[t/a]$}{$\true{\phi t}$} \end{prooftree} \] \[ \begin{prooftree} \Deriv{$\mathcal{D}$}{$\true{\forall x. \phi x}$} \end{prooftree} \quad\Longrightarrow_E\quad \begin{prooftree} \Deriv{$\mathcal{D}$}{$\true{\forall x. \phi x}$} \RL{$\forall E$} \UIC{$\phi a$} \RL{$\forall I$} \UIC{$\forall x. \phi x$} \end{prooftree} \]

존재 양화사

\[ \begin{prooftree} \Deriv{$\mathcal{D}$}{ $\true{\phi t}$ } \RL{ $\exists I$ } \UIC{ $\true{\exists x. \phi x}$ } \Hyp{$u$}{$\true{\phi a}$} \noLine \UIC{$\mathcal{E}$} \noLine \UIC{$\true{\chi}$} \RL{ $\exists E^u$ } \BIC{ $\true{\chi}$ } \end{prooftree} \qquad\Longrightarrow_R\quad \begin{prooftree} \Deriv{$\mathcal{D}$}{$\true{\phi t}$} \noLine \UIC{$\mathcal{E}[t/a]$} \noLine \UIC{$\true{\chi}$} \end{prooftree} \] \[ \begin{prooftree} \Deriv{$\mathcal{D}$}{$\true{\exists x. \phi x}$} \end{prooftree} \qquad\Longrightarrow_E\quad \begin{prooftree} \Deriv{$\mathcal{D}$}{$\true{\exists x. \phi x}$} \Hyp{$u$}{$\true{\phi a}$} \RL{$\exists I$} \UIC{$\true{\exists x. \phi x}$} \RL{ $\exists E^u$ } \BIC{ $\true{\exists x. \phi x}$ } \end{prooftree} \]

검증과 사용

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

본 문서에서는 [7]를 따라 \(\phi\)의 검증을 \(\phi \uparrow\)로, \(\phi\)의 사용을 \(\phi \downarrow\)로 표기한다.

연언

\[ \newcommand{\verif}[1] {#1 \uparrow} \newcommand{\use}[1] {#1 \downarrow} \begin{prooftree} \AxiomC{ $\verif{\phi}$ } \AxiomC{ $\verif{\psi}$ } \RightLabel{ $\wedge I$ } \BinaryInfC{ $\verif{\phi \wedge \psi}$ } \end{prooftree} \quad \begin{prooftree} \AxiomC{ $\use{\phi \wedge \psi}$ } \RightLabel{ $\wedge E_1$ } \UnaryInfC{ $\use{\phi}$ } \end{prooftree} \quad \begin{prooftree} \AxiomC{ $\use{\phi \wedge \psi}$ } \RightLabel{ $\wedge E_2$ } \UnaryInfC{ $\use{\psi}$ } \end{prooftree} \]

선언

\[ \begin{prooftree} \AxiomC{ $\verif{\phi}$ } \RightLabel{ $\vee I_1$ } \UnaryInfC{ $\verif{\phi \vee \psi}$ } \end{prooftree} \quad \begin{prooftree} \AxiomC{ $\verif{\psi}$ } \RightLabel{ $\vee I_2$ } \UnaryInfC{ $\verif{\phi \vee \psi}$ } \end{prooftree} \quad \begin{prooftree} \AxiomC{ $\use{\phi \vee \psi}$ } \HypJ{$u$}{$\use{\phi}$}{$\verif{\chi}$} \HypJ{$v$}{$\use{\psi}$}{$\verif{\chi}$} \RightLabel{ $\vee E^{u,v}$ } \TrinaryInfC{ $\verif{\chi}$ } \end{prooftree} \]

함언

\[ \begin{prooftree} \HypJ{$u$}{$\use{\phi}$}{$\verif{\psi}$} \RightLabel{ ${\to} I^u$ } \UnaryInfC{ $\verif{\phi \to \psi}$ } \end{prooftree} \quad\quad\qquad \begin{prooftree} \AxiomC{ $\use{\phi \to \psi}$ } \AxiomC{ $\verif{\phi}$ } \RightLabel{ ${\to} E$ } \BinaryInfC{ $\use{\psi}$ } \end{prooftree} \]

참 연결사

\[ \begin{prooftree} \AxiomC{ } \RightLabel{ $\top I$ } \UnaryInfC{ $\verif{\top}$ } \end{prooftree} \]

거짓 연결사

\[ \begin{prooftree} \AxiomC{ $\use{\bot}$ } \RightLabel{ $\bot E$ } \UnaryInfC{ $\verif{\chi}$ } \end{prooftree} \]

보편 양화사

\[ \begin{prooftree} \AxiomC{ $\verif{\phi a}$ } \RightLabel{ $\forall I$ } \UnaryInfC{ $\verif{\forall x. \phi x}$ } \end{prooftree} \quad \begin{prooftree} \AxiomC{ $\use{\forall x. \phi x}$ } \RightLabel{ $\forall E$ } \UnaryInfC{ $\use{\phi t}$ } \end{prooftree} \]

존재 양화사

\[ \begin{prooftree} \AxiomC{ $\verif{\phi t}$ } \RightLabel{ $\exists I$ } \UnaryInfC{ $\verif{\exists x. \phi x}$ } \end{prooftree} \quad \begin{prooftree} \AxiomC{ $\use{\exists x. \phi x}$ } \HypJ{$u$}{$\use{\phi a}$}{$\verif{\chi}$} \RightLabel{ $\exists E^u$ } \BinaryInfC{ $\verif{\chi}$ } \end{prooftree} \]

명제 변수

\[ \begin{prooftree} \AXC{ $\use{P}$ } \RL{ $\downarrow\uparrow^*$ } \UIC{ $\verif{P}$ } \end{prooftree} \]

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

전역적 건전성

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

\[ \begin{prooftree} \AXC{If} \AXC{$\verif{\phi}$} \AXC{and} \noLine \TrinaryInfC{} \end{prooftree} \quad \ \ \begin{prooftree} \AXC{$\use{\phi}$} \noLine \UIC{$\vdots$} \noLine \UIC{$\verif{\psi}$} \AXC{then} \AXC{$\verif{\psi}$} \noLine \TrinaryInfC{} \end{prooftree} \]

전역적 완전성

전역적 건전성은 시퀀트 계산에서 항등 규칙의 admissibility에 대응된다. \[ \begin{prooftree} \AXC{$\use{\phi}$} \noLine \UIC{$\vdots$} \noLine \UIC{$\verif{\phi}$} \end{prooftree} \]

참고문헌