주 메뉴 열기

논리학증명이론에서, 자연 연역(自然演繹, natural deduction)이란 증명 연산의 일종으로, 논리적 추론이 "자연스러운" 추론 방법과 밀접히 연관된 추론 규칙으로 표현된다. 이는, 추론규칙의 논리적 법칙을 표현하기 위해 많은 공리들을 이용하는 힐베르트 체계와는 대조된다.

목차

판단과 명제편집

자연 연역의 일련의 과정은 이미 자명한 명제인 판단(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도 참이다. 이 도출과정에서는, 아래에 대한 전제가 되는 추론이 앞에 대해서는 결론이 되는 방식의 기법이 보인다.

 

가설적 도출편집

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

논리에서의 확장편집

같이 보기편집