자연 연역

논리학 및 증명이론에서 자연 연역(自然演繹, natural deduction)이란 자연스러운 논리적 추론을 나타내는 증명 연산의 일종으로, 최대한 공리를 배제하고 오직 구문적인 추론 규칙만을 사용한 증명이 이루어지는 것이 특징이다. 이는, 추론규칙의 논리적 법칙을 표현하기 위해 많은 공리들을 이용하는 힐베르트 체계와는 대조된다.

역사

자연 연역은 20세기 초 논리학자들이 명제 논리의 공리화에 문제점을 느낀 것으로부터 시작되었다 할 수 있다. 그러한 공리화된 명제논리의 가장 유명한 예로는 러셀과 화이트헤드가 고안한 수학 원리가 있었다. 폴란드 학파의 얀 우카시에비치(Jan Łukasiewicz)는 논리를 더 자연스러운 방법을 통해 다룰 필요가 있음을 주장하였고, 이에 자극받은 스타니스와프 야시코프스키(Stanisław Jaśkowski)가 1929년 다이어그램 기법을 발표한 것을 시작으로 여러 연구를 진행하여 자연연역 체계를 논문에 제시하기도 하였으나 당시에는 잘 알려지지 않았다.

한편 독일의 게르하르트 겐첸은 독립적으로 1935년 자연 연역 체계를 개발하여 학위논문에 발표하였고 이것이 현대 자연 연역의 기반이 된다. 겐첸은 페아노 공리계의 일관성을 증명하기 위하여 바로 자연연역을 이용했으나, 그 복잡성에 불만을 느껴 1938년에는 시퀀트 계산으로 불리는 새로운 증명구조를 고안한다. 1960년대의 Dag Prawitz는 일련의 강의를 진행하며 자연연역을 포괄적으로 정리하기 시작하였고, 그의 1965년 논문 Natural deduction: a proof-theoretical study에서 제시된 형태는 현재 자연연역의 최종판으로서 양상 논리나 2차 술어 논리에 대한 응용도 제시되어 있다.

자연 연역 논리

자연 연역의 체계는 보통 공리를 가지지 않고 주어진 식에 정해진 변화를 가하는 추론규칙만을 사용한다. 잘 알려진 체계 System L에서는 증명의 구문규칙에 관한 다음의 9가지 추론규칙이 존재한다.

1. 가정 규칙 "The Rule of Assumption" (A)
2. 전건 긍정 "Modus Ponendo Ponens" (MPP)
3. 이중 부정 규칙 "The Rule of Double Negation"
4. 조건 증명 규칙 "The Rule of Conditional Proof" (CP)
5. ∧-도입 규칙 "The Rule of ∧-introduction" (∧I)
6. ∧-제거 규칙 "The Rule of ∧-elimination" (∧E)
7. ∨-도입 규칙 "The Rule of ∨-introduction" (∨I)
8. ∨-제거 규칙 "The Rule of ∨-elimination" (∨E)
9. 귀류법 "Reductio Ad Absurdum" (RAA)

System L에서 증명은 다음의 조건으로 정의된다:

1. 정형논리식(wff)의 유한열로 이루어진다.
2. 각 행은 L의 규칙에 의하여 정당화(형성)된다.
3. 증명의 마지막 행이 '결론'이 되며, 이는 증명의 '전제'(들)만을 사용하여 도출된 것이어야 한다. 전제는 존재하지 않을 수도 있다.

전제가 없는 증명열을 정리(theorem)라 말한다. 곧 L에서 정리란 "L 속에서 공집합인 전제를 사용하여 증명가능한 열"로 정의될 수 있다.

흔히 각 행 옆에는 해당 행의 식의 성립의 근거가 되는 규칙과 행이 함께 표시된다. 다음은 System L (tabular)에서 증명의 예 (후건 부정):

p → q, ¬q ⊢ ¬p [Modus Tollendo Tollens (MTT)]
가정 번호	행 번호	논리식 (wff)	근거가 되는 규칙 및 행
1	(1)	(p → q)	A
2	(2)	¬q	A
3	(3)	p	A (for RAA)
1,3	(4)	q	1,3,MPP
1,2,3	(5)	q ∧ ¬q	2,4,∧I
1,2	(6)	¬p	3,5,RAA
Q.E.D

증명의 예 (배중률)

⊢p ∨ ¬p
가정 번호	행 번호	논리식 (wff)	근거가 되는 규칙 및 행
1	(1)	¬(p ∨ ¬p)	A (for RAA)
2	(2)	¬p	A (for RAA)
2	(3)	(p ∨ ¬p)	2, ∨I
1, 2	(4)	(p ∨ ¬p) ∧ ¬(p ∨ ¬p)	1, 2, ∧I
1	(5)	¬¬p	2, 4, RAA
1	(6)	p	5, DN
1	(7)	(p ∨ ¬p)	6, ∨I
1	(8)	(p ∨ ¬p) ∧ ¬(p ∨ ¬p)	1, 7, ∧I
	(9)	¬¬(p ∨ ¬p)	1, 8, RAA
	(10)	(p ∨ ¬p)	9, DN
Q.E.D

System L의 각 규칙들은 제각각 input으로 받아들일 수 있는 식의 타입을 규정해놓고 있으며 그 input에 쓰이는 가정을 다루는 법 역시 제각각 다르다.

위의 tabular 표기법과 유사한 Fitch diagram 표기법이 있는데, 근본적으로 표기방식 이외에 큰 차이는 없다. 그러나 표기법과 별개로 공리적 명제논리가 어떤 공리 또는 추론규칙을 채택하는가는 제각각 달라진다.

형식적 정의

명제의 유한열 $\beta _{1},...,\beta _{n}$ 이 전제식의 집합 $\Sigma$로부터 결론식 $\alpha$로의 연역(deduction)이라 함은, 다음이 모두 성립함을 가리킨다:

• $\beta _{n}=\alpha$
• 모든 $1\leq i\leq n$에 대하여, $\beta _{i}$가 전제식이거나(곧 $\beta _{i}\in \Sigma$이거나) $\beta _{i}$가 이전에 출현한 명제에 어떠한 추론규칙을 적용한 결과식이다.

공리적 명제논리의 종류에 따라 채택되는 공리나 추론규칙이 다르다. 예를 들어 프레게는 연역체계를 구성할 때 6개의 공리와 2개의 규칙을 정해놓았고, 프린키피아 마테마티카는 5개의 공리로부터 구성되는 체계를 보이기도 했다.

얀 우카시에비치의 명제 논리에서는 다음과 같은 공리계 A를 사용했다:

• [PL1] p → (q → p)
• [PL2] (p → (q → r)) → ((p → q) → (p → r))
• [PL3] (¬p → ¬q) → (q → p)

그리고 추론규칙계 R에는 전건긍정(MP)을 포함했다.

• [MP] α, α → β ⊢ β

추론규칙에 의해 Σ에 포함되는 논리식과 공리들로부터 새로운 논리식을 도출해낼 수 있다.

판단과 명제

자연 연역의 일련의 과정은 이미 올바른 명제들에 추론규칙(inference rule)을 적용하여 또다른 올바른 명제를 이끌어내는 것이다. 즉 연역의 일련의 과정은 결론이 되는 명제에 대한 증명을 구성하는 과정이기도 하다.

논리에서 가장 중요한 판단인 "A는 참이다"라는 형태를 보면, 문자 A는 명제를 나타내는 어떠한 표현으로도 치환될 수 있는데, 이에 따라 진위 판단은 더 기본적인 판단, "A는 명제이다"라는 판단을 필요로 한다. 가장 기본적인 두 판단 "A는 명제이다"와 "A는 참이다"는 자연연역에서 각각 "A prop" 와 "A true"라는 약자로 표기된다.

형성 규칙(formation rule)의 일반적인 형태는 다음과 같다:

${\frac {J_{1}\qquad J_{2}\qquad \cdots \qquad J_{n}}{J}}\ {\hbox{name}}$

여기서 각 $J_{i}$는 명제이고 추론 규칙의 이름이 "name" 칸에 들어간다. 직선 위의 명제를 전제(premise)라 하고, 직선 아래의 명제를 결론(conclusion)이라 한다.

두 명제 A와 B가 있다 하고 이로부터 복합 명제인 논리곱 $A\wedge B$를 구성해낸다 하자. 이 도식(꼴)을 추론규칙의 형식에 따라 이렇게 쓸 수 있다:

${\frac {A{\hbox{ prop}}\qquad B{\hbox{ prop}}}{(A\wedge B){\hbox{ prop}}}}\ \wedge _{F}$

형성 규칙에 따라 명제를 형성하는 것은 그저 그것이 구성될 수 있음을 명시하는 것이지 그것이 참임을 의미하는 것은 아니다. 따라서 연언($\wedge$), 선언($\vee$), 부정($\neg$), 함의($\implies$), 항진($\top$), 모순($\bot$)을 도입하는 다양한 formation 과정을 생각할 수 있고 이를 통해 항상 새로운 명제를 구성할 수 있다.

도입과 소거

참인 명제로부터 참인 명제를 이끌어내는 생성규칙을 추론규칙(inference rules)이라 부른다. 이 경우 각 명제가 true임이 드러나야 한다. 다만 흔히 추론규칙에 의한 연역임이 자명할 때 생략될 수 있다.

참인 명제에서 더 복합적인 참인 명제를 구성하는 추론규칙을 도입 규칙(introduction rules)이라 한다. 예컨대 논리곱을 도입한다는 것은 명제 "A true"와 "B true"에서 "A and B true"라는 결론을 이끌어낸다는 것이며, 이를 추론규칙으로 표기하면 다음과 같다:

${\frac {A{\hbox{ true}}\qquad B{\hbox{ true}}}{(A\wedge B){\hbox{ true}}}}\ \wedge _{I}$

이때 각 대상이 명제라는 것은 자명하다고 보아졌으며, 원래대로 정확히 표현하면 다음과 같이 된다:

${\frac {A{\hbox{ prop}}\qquad B{\hbox{ prop}}\qquad A{\hbox{ true}}\qquad B{\hbox{ true}}}{(A\wedge B){\hbox{ true}}}}\ \wedge _{I}$

아래는 여러 도입 규칙들이다:

논리곱을 도입하는 연언 도입:

${\frac {A\qquad B}{(A\wedge B)}}\ \wedge _{I}$

논리합을 도입하는 선언 도입. 명제의 진리치가 세워지는 과정이 1가지가 아니므로 선언 도입은 사실 2가지 규칙의 총칭이다:

${\frac {A}{(A\vee B)}}\ \vee _{I}\qquad {\frac {B}{(A\vee B)}}\ \vee _{I}$

항진 도입. 항진(참)은 전제가 전혀 없는 경우에도 도출된다: ${\frac {\ }{\top {\hbox{ true}}}}\ \top _{I}$

한편, 아무 전제도 없이 모순(거짓)을 도입하는 도입규칙은 존재하지 않는다. 따라서 더 단순한 판단으로부터 거짓을 추론해내는 것은 불가능하다.

도입규칙의 반대 꼴이 되는 소거 규칙(elimination rules)이라는 것이 존재하는데, 이는 거꾸로 복합적인 명제를 해체해내는 추론규칙이다. 예를 들어 논리곱을 제거하는 연언 소거가 있다:

${\frac {A\wedge B}{A}}\ \wedge _{E}\qquad {\frac {A\wedge B}{B}}\ \wedge _{E}$

추론규칙들을 적용하여 다음과 같이 논리곱의 교환법칙을 증명할 수 있다.

${\cfrac {{\cfrac {A\wedge B}{B}}\ \wedge _{E2}\qquad {\cfrac {A\wedge B}{A}}\ \wedge _{E1}}{B\wedge A}}\ \wedge _{I}$

가설적 도출

논리학에는 가정에 의한 추론(inferece by assumptions)이 있다. 이를 나타내기 위하여 가설적 도출의 기법이 사용된다.

A가 참임을 가정하여 B가 참임을 도출하였다는 것을, 다음과 같이 쓸 수 있다.

${\begin{matrix}[A]\\\vdots \\B\\\end{matrix}}$

이에 관한 추론규칙으로는 함의 도입이 있다. A true를 가정했을 때 B true가 도출되면 (A ⊃ B) ture를 인정한다.

${\begin{matrix}[A]\\\vdots \\B\\\hline (A\supset B)\end{matrix}}$

이와 연관된 규칙으로써 후건 부정, 즉 not B인 상황에서 A를 가정했을 때 B가 도출된다면 not A를 추론하는 것 등이 있다.

일관성, 완전성, 정규형

수리논리에서는 형식적 이론에서 모순이 추론될 수 없으면 그 이론은 일관적 또는 무모순적(consistent)이라 하고, 참인 문장을 추론 규칙에 의해 도출할 수 있으면 완전(complete)하다고 한다. 흔히 이들은 모델론적 방식으로 이해되지만 증명론에서 제한적 의미의(local) 무모순성과 완전성은 순수하게 구문론적인 방식만으로 확인될 수 있다.

local consistency는 도입규칙이 이어지다가 바로 뒤에 소거규칙이 사용된 도출은 반드시 이러한 '우회'가 없는(즉, 이 소거규칙이 없는) 도출로도 대체될 수 있음을 말한다. 예를 들어 A와 B에서 연언 도입으로 A∧B를 도출하고 다시 연언 소거로 A를 도출했다고 하자. 이는 A에서 A를 도출하는 것으로 축약될 수 있다. 이 성질은 소거규칙의 '강도'를 확인해주는 것이다. 그말인즉슨 소거규칙이 '너무 강하면' 이미 언급되지 않은 정보를 도출하게 되어버려 local consistency가 성립할 수 없다.

한편 local completeness는 그 쌍대(dual)가 되는 개념으로 소거규칙이 '충분히 강해서' 본래의 식을 다시 도입할 수 있는 정도가 됨을 확인해준다. 예를 들어 A∧B를 도출하는 과정은, A∧B에 연언 소거를 적용하여 A와 B를 각각 도출하고 이 둘로부터 연언 도입으로 다시 A∧B를 도출하는 더 복잡한 과정으로 대체될 수 있다.

커리-하워드 대응(Curry-Howard correspondence)에 의하면 local consistency와 local completeness는 각각 람다 계산의 베타 축약(β-reduction)과 에타 변환(η-conversion)과 일치하는 개념이다. completeness에 나온 것처럼 소거와 도입을 차례로 적용하는 과정으로만 이루어진 도출을 표준형(normal form)이라 하며, 모든 도출은 대응하는 표준형을 가짐이 여러 방법으로 증명되어 있다. 이는 추상 재작성 시스템 연구와 연관된다.

같이 보기

• 시퀀트 계산
• 1차 논리
• 양상 논리
• 연역