연역 정리

틀:위키데이터 속성 추적 수리논리학에서 연역 정리(틀:Llang)는 술어 논리 및 1차 논리의 메타 정리(metatheorem)로, 전제된 논리식 E로부터 논리식 F를 연역가능하다면 함의 E → F가 증명가능(공집합으로부터 연역 가능)하다는 정리이다. 기호로 나타내면 $E⊢F$이면 $⊢E\to F$이라는 것이다.

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

$E_1,E_2,...,E_{n-1},E_n⊢F$ 로부터 $E_1,E_2,...,E_{n-1}⊢E_n\to F$를 추론가능하며, 결국

$⊢E_1\to (...(E_{n-1}\to (E_n\to F))...)$ 로 된다.

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

같이 보기

• 명제 논리