주 메뉴 열기

논리학증명이론에서, 자연 연역(自然演繹, 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)에서 증명의 예 (후건 부정):

pq, ¬q ⊢ ¬p [Modus Tollendo Tollens (MTT)]
가정 번호 행 번호 논리식 (wff) 근거가 되는 규칙 및 행
1 (1) (pq) 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 표기법이 있는데, 근본적으로 표기방식 이외에 큰 차이는 없다. 그러나 표기법과 별개로 공리적 명제논리가 어떤 공리 또는 추론규칙을 채택하는가는 제각각 달라진다.

형식적 정의편집

명제의 유한열   이 전제식의 집합  로부터 결론식  로의 연역(deduction)이라 함은, 다음이 모두 성립함을 가리킨다:

  •  
  • 모든  에 대하여,  가 전제식이거나(곧  이거나)  가 이전에 출현한 명제에 어떠한 추론규칙을 적용한 결과식이다.

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

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

  • [PL1] p → (qp)
  • [PL2] (p → (qr)) → ((pq) → (pr))
  • [PL3] (¬p → ¬q) → (qp)

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

  • [MP] α, α → β ⊢ β

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

판단과 명제편집

자연 연역의 일련의 과정은 이미 자명한 명제인 판단(judjment)들로부터 또다른 판단을 이끌어내는 것이다. 연역에 있어서 판단이 자명하다는 것은, 그것에 대한 증명이 존재한다는 것이다. 즉 연역의 일련의 과정은 결론에 대한 증명을 구성하는 과정이기도 하다.

논리에서 가장 중요한 판단인 "A는 참이다"라는 형태를 보면, 문자 A는 명제를 나타내는 어떠한 표현으로도 치환될 수 있는데, 이에 따라 진위 판단은 더 기본적인 판단, "A는 명제이다"라는 판단을 필요로 한다. 가장 기본적인 두 판단 "A는 명제이다"와 "A는 참이다"는 자연연역에서 각각 "A prop" 와 "A true"라는 약자로 표기된다. 먼저 판단 "A prop"가 A의 타당한 증명의 구조를 정의하고, 이로부터 명제의 구조가 정의된다. 이 때문에, 이 판단에 대한 추론 규칙들은 생성 규칙(formation rule)이라고 불리기도 한다. 추론 규칙(inference rule)의 일반적인 형태는 다음과 같다:

 

여기서 각  는 판단이고 추론 규칙의 이름이 "name" 칸에 들어간다. 직선 위의 판단을 전제(premise)라 하고, 직선 아래의 판단을 결론(conclusion)이라 한다.

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

 

이외의 일반적인 논리 명제들, 곧 논리합( ), 부정( ), 함의( )와 논리 상수 "참"( )과 "거짓"( )의 생성 규칙은 각각 아래와 같다:

 
 

도입과 제거편집

논리 결합자를 결론으로써 도입하는 추론규칙을 도입규칙(introduction rules)이라 부른다. 예컨대 논리곱을 도입한다는 것은 명제 A와 B에서 A and B true라는 결론을 이끌어낸다는 것인데, 이 때 A trueB true라는 증거가 필요하며, 이를 추론규칙으로 표기하면 다음과 같다:

 

이러한 규칙에서 각 오브젝트는 명제여야 한다는 것은 자명하다고 치며, 원래대로 정확히 표현하면 다음과 같이 된다:

 

다음과 같이도 쓸 수 있다:

 

이 형식에서 첫번째 전제는   생성 규칙에 따라 얻어진 것이다. 이하에서는 판단 "prop"는 자명하다고 보고 생략한다. 또한, 참은 전제가 전혀 없는 경우에서도 도출된다.

 

명제의 진리치가 세워지는 과정이 1가지가 아니라면, 대응하는 결합자는 여러 개의 추론 규칙을 가지게 된다.

 

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


도입규칙의 반대 꼴이 되는 제거 규칙(elimination rules)이라는 것이 존재하는데, 이는 거꾸로 복합적인 명제를 해체해내는 추론규칙이다. 예를 들어, 다음과 같이 A∧B true로부터 A trueB true라는 결론을 이끌어내는 것이 가능하다:

 

추론규칙의 적용례로서 논리곱의 교환법칙을 나타내어보자. A∧B가 참이라면, B∧A도 참이다. 이 도출과정에서는, 아래에 대한 전제가 되는 추론이 앞에 대해서는 결론이 되는 방식의 기법이 보인다.

 

가설적 도출편집

일관성, 완전성, 정규형편집

논리에서의 확장편집

같이 보기편집