자연 연역 문서 원본 보기

{{위키데이터 속성 추적}}
[[논리학]] 및 [[증명이론]]에서 '''자연 연역'''(自然演繹, 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가지 추론규칙이 존재한다.

# 가정 규칙 "The Rule of Assumption" (A)
# [[전건 긍정]] "Modus Ponendo Ponens" (MPP)
# 이중 부정 규칙 "The Rule of Double Negation"
# 조건 증명 규칙 "The Rule of Conditional Proof" (CP)
# ∧-도입 규칙 "The Rule of ∧-introduction" (∧I)
# ∧-제거 규칙 "The Rule of ∧-elimination" (∧E)
# ∨-도입 규칙 "The Rule of ∨-introduction" (∨I)
# ∨-제거 규칙 "The Rule of ∨-elimination" (∨E)
# [[귀류법]] "Reductio Ad Absurdum" (RAA)


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

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

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

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

{| class="wikitable"
|align="center" bgcolor="#FFEBAD" colspan="4"|''p'' → ''q'', ¬''q'' ⊢ ¬''p''  [Modus Tollendo Tollens (MTT)]
|-
!가정 번호
!행 번호
!논리식 (''wff'')
!근거가 되는 규칙 및 행
|-
|bgcolor="#bbffbb"|1
|bgcolor="#bbffbb"|(1)
|bgcolor="#bbffbb"|(''p'' → ''q'')
|bgcolor="#bbffbb"| A
|-
|bgcolor="#bbffbb"|2
|bgcolor="#bbffbb"|(2)
|bgcolor="#bbffbb"|¬''q''
|bgcolor="#bbffbb"| A
|-
|bgcolor="#bbffbb"|3
|bgcolor="#bbffbb"|(3)
|bgcolor="#bbffbb"|''p''
|bgcolor="#bbffbb"| A (for RAA)
|-
|bgcolor="#bbffbb"|1,3
|bgcolor="#bbffbb"|(4)
|bgcolor="#bbffbb"|''q''
|bgcolor="#bbffbb"| 1,3,MPP
|-
|bgcolor="#bbffbb"|1,2,3
|bgcolor="#bbffbb"|(5)
|bgcolor="#bbffbb"|''q'' ∧ ¬''q''
|bgcolor="#bbffbb"| 2,4,∧I
|-
|bgcolor="#bbffbb"|1,2
|bgcolor="#bbffbb"|(6)
|bgcolor="#bbffbb"|¬''p''
|bgcolor="#bbffbb"| 3,5,RAA
|-
|align="center" bgcolor="#BBBBFF" colspan="4"|Q.E.D
|-
|}

증명의 예 ([[배중률]])

{| class="wikitable"
|align="center" bgcolor="#FFEBAD" colspan="4"|⊢''p'' ∨  ¬''p''
|-
!가정 번호
!행 번호
!논리식 (''wff'')
!근거가 되는 규칙 및 행
|-
|bgcolor="#bbffbb"|1
|bgcolor="#bbffbb"|(1)
|bgcolor="#bbffbb"|¬(''p'' ∨  ¬''p'')
|bgcolor="#bbffbb"|A (for RAA)
|-
|bgcolor="#bbffbb"|2
|bgcolor="#bbffbb"|(2)
|bgcolor="#bbffbb"|¬''p''
|bgcolor="#bbffbb"|A (for RAA)
|-
|bgcolor="#bbffbb"|2
|bgcolor="#bbffbb"|(3)
|bgcolor="#bbffbb"|(''p'' ∨  ¬''p'')
|bgcolor="#bbffbb"|2, ∨I
|-
|bgcolor="#bbffbb"|1, 2
|bgcolor="#bbffbb"|(4)
|bgcolor="#bbffbb"|(''p'' ∨  ¬''p'') ∧ ¬(''p'' ∨  ¬''p'')
|bgcolor="#bbffbb"|1, 2, ∧I
|-
|bgcolor="#bbffbb"|1
|bgcolor="#bbffbb"|(5)
|bgcolor="#bbffbb"|¬¬''p''
|bgcolor="#bbffbb"|2, 4, RAA
|-
|bgcolor="#bbffbb"|1
|bgcolor="#bbffbb"|(6)
|bgcolor="#bbffbb"|''p''
|bgcolor="#bbffbb"|5, DN
|-
|bgcolor="#bbffbb"|1
|bgcolor="#bbffbb"|(7)
|bgcolor="#bbffbb"|(''p'' ∨  ¬''p'')
|bgcolor="#bbffbb"|6, ∨I
|-
|bgcolor="#bbffbb"|1
|bgcolor="#bbffbb"|(8)
|bgcolor="#bbffbb"|(''p'' ∨  ¬''p'') ∧ ¬(''p'' ∨  ¬''p'')
|bgcolor="#bbffbb"|1, 7, ∧I
|-
|bgcolor="#bbffbb"|
|bgcolor="#bbffbb"|(9)
|bgcolor="#bbffbb"|¬¬(''p'' ∨  ¬''p'')
|bgcolor="#bbffbb"|1, 8, RAA
|-
|bgcolor="#bbffbb"|
|bgcolor="#bbffbb"|(10)
|bgcolor="#bbffbb"|(''p'' ∨  ¬''p'')
|bgcolor="#bbffbb"|9, DN
|-
|align="center" bgcolor="#BBBBFF" colspan="4"|Q.E.D
|-
|}

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

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

== 형식적 정의 ==
명제의 유한열 <math>\beta_1, ... , \beta_n</math> 이 전제식의 집합 <math>\Sigma</math>로부터 결론식 <math>\alpha</math>로의 '''연역'''(deduction)이라 함은, 다음이 모두 성립함을 가리킨다:
:* <math>\beta_n = \alpha</math>
:* 모든 <math> 1 \le i \le n</math>에 대하여, <math>\beta_i</math>가 전제식이거나(곧 <math>\beta_i \in \Sigma</math>이거나) <math>\beta_i</math>가 이전에 출현한 명제에 어떠한 추론규칙을 적용한 결과식이다.

공리적 명제논리의 종류에 따라 채택되는 공리나 추론규칙이 다르다. 예를 들어 프레게는 연역체계를 구성할 때 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)의 일반적인 형태는 다음과 같다:
:<math>\frac{J_1 \qquad J_2 \qquad \cdots \qquad J_n}{J}\ \hbox{name}</math>

여기서 각 <math>J_i</math>는 명제이고 추론 규칙의 이름이 "name" 칸에 들어간다. 직선 위의 명제를 '''전제'''(premise)라 하고, 직선 아래의 명제를 '''결론'''(conclusion)이라 한다.

두 명제 A와 B가 있다 하고 이로부터 복합 명제인 [[논리곱]] <math>A \wedge B</math>를 구성해낸다 하자. 이 도식(꼴)을 추론규칙의 형식에 따라 이렇게 쓸 수 있다:
:<math>\frac{A\hbox{ prop} \qquad B\hbox{ prop}}{(A \wedge B)\hbox{ prop}}\ \wedge_F</math>

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

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

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

이때 각 대상이 명제라는 것은 자명하다고 보아졌으며, 원래대로 정확히 표현하면 다음과 같이 된다:
:<math>
\frac{A\hbox{ prop} \qquad B\hbox{ prop} \qquad A\hbox{ true} \qquad B\hbox{ true}}{(A \wedge B) \hbox{ true}}\ \wedge_I
</math>

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

[[논리곱]]을 도입하는 [[연언 도입]]:
:<math>\frac{A \qquad B}{(A \wedge B)}\ \wedge_I</math>

[[논리합]]을 도입하는 [[선언 도입]]. 명제의 진리치가 세워지는 과정이 1가지가 아니므로 선언 도입은 사실 2가지 규칙의 총칭이다:
:<div style="margin-left: 2em">
<math>
\frac{A}{(A \vee B)}\ \vee_I
\qquad
\frac{B}{(A \vee B)}\ \vee_I
</math>
</div>

항진 도입. [[항진명제|항진]](참)은 전제가 전혀 없는 경우에도 도출된다:
<math>
\frac{\ }{\top\hbox{ true}}\ \top_I
</math>

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


도입규칙의 반대 꼴이 되는 '''소거 규칙'''(elimination rules)이라는 것이 존재하는데, 이는 거꾸로 복합적인 명제를 해체해내는 추론규칙이다. 예를 들어 논리곱을 제거하는 [[연언 소거]]가 있다:
<div style="margin-left: 2em">
<math>
\frac{A \wedge B}{A}\ \wedge_E
\qquad
\frac{A \wedge B}{B}\ \wedge_E
</math>
</div>

추론규칙들을 적용하여 다음과 같이 논리곱의 [[교환법칙]]을 증명할 수 있다.
<div style="margin-left: 2em">
<math>
 \cfrac{\cfrac{A \wedge B}{B}\ \wedge_{E2}
 \qquad
 \cfrac{A \wedge B}{A}\ \wedge_{E1}}
 {B \wedge A}\ \wedge_I
</math>
</div>

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

A가 참임을 가정하여 B가 참임을 도출하였다는 것을, 다음과 같이 쓸 수 있다.
:<math>
\begin{matrix}
[A] \\
\vdots \\
B \\
\end{matrix}
</math>

이에 관한 추론규칙으로는 [[함의 도입]]이 있다. A true를 가정했을 때 B true가 도출되면 (A ⊃ B) ture를 인정한다.
:<math>
\begin{matrix}
[A] \\
\vdots \\
B \\
\hline
(A\supset B)
\end{matrix}
</math>

이와 연관된 규칙으로써 [[후건 부정]], 즉 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차 논리]]
* [[양상 논리]]
* [[연역]]


[[분류:연역]]
[[분류:논리학]]