연역 정리

수리논리학에서 연역 정리(영어: deduction theorem)는 술어 논리 및 1차 논리의 메타 정리(metatheorem)로, 전제된 논리식 E로부터 논리식 F를 연역가능하다면 함의 E → F가 증명가능(공집합으로부터 연역 가능)하다는 정리이다. 기호로 나타내면 ${\displaystyle E\vdash F}$이면 ${\displaystyle \vdash E\rightarrow F}$이라는 것이다.

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

${\displaystyle E_{1},E_{2},...,E_{n-1},E_{n}\vdash F}$ 로부터 ${\displaystyle E_{1},E_{2},...,E_{n-1}\vdash E_{n}\rightarrow F}$를 추론가능하며, 결국

${\displaystyle \vdash E_{1}\rightarrow (...(E_{n-1}\rightarrow (E_{n}\rightarrow F))...)}$ 로 된다.

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

같이 보기

• 명제 논리