연역 정리 문서 원본 보기

{{위키데이터 속성 추적}}
[[수리논리학]]에서 '''연역 정리'''({{llang|en|deduction theorem}})는 [[술어 논리]] 및 [[1차 논리]]의 [[메타 정리]](metatheorem)로, 전제된 논리식 E로부터 논리식 F를 [[연역]]가능하다면 [[함의]] E → F가 증명가능(공집합으로부터 연역 가능)하다는 정리이다. 기호로 나타내면 <math> E \vdash F </math>이면 <math> \vdash E \rightarrow F </math>이라는 것이다.

연역 정리는 다음과 같이 임의의 개수의 유한한 전제 논리식들로 일반화할 수 있다:

<math> E_1, E_2, ... , E_{n-1}, E_n \vdash F </math> 로부터
<math> E_1, E_2, ... , E_{n-1} \vdash E_n \rightarrow F </math>를 추론가능하며, 결국

<math> \vdash E_1\rightarrow(...(E_{n-1} \rightarrow (E_n \rightarrow F))...) </math> 로 된다.

연역 정리는 왜 수학에 있어서 조건절의 증명이 논리적으로 참이 되는가를 설명해준다. 이는 직관적으로 '자명하다'고 받아들여져 왔으나, 20세기 초에 [[자크 에르브랑|에르브랑]]과 [[타르스키]]는 (제각각) 이것이 일반적인 경우에 논리적으로 올바르다는 것을 보였다.

== 같이 보기 ==
* [[명제 논리]]

{{토막글|수학}}

[[분류:연역]]
[[분류:논리학]]
[[분류:수학기초론 정리]]