함의 도입(含意導入, 영어: implication introduction)은 논리학에서 가언 명제(조건문)를 유도하는 추론 규칙이다. 형식 논리학에서 사용되는 기본적인 추론 규칙 가운데 하나로, 어떤 가정으로부터 결론을 이끌어낸 뒤 그 가정을 조건의 전제로 하는 함의문(→)을 도출하는 절차를 말한다.
정의
논리식 $P$를 가정으로 삼아 추론 과정 $\mathcal{D}$를 통해 논리식 $Q$를 유도한 것을 다음과 같이 나타낸다.
$$ \begin{matrix} P \ (\mathcal{D}) \ Q \end{matrix} $$
이때 함의 도입은 아래와 같이 표현된다.
$$ \begin{matrix} [P] \ (\mathcal{D}) \ Q \ \hline P \implies Q \end{matrix} $$
여기서 $[P]$는 가정 $P$가 취소(cancel)되었음을 의미한다. 즉, 함의 도입을 통해 얻은 결론 $P \implies Q$는 더 이상 $P$를 전제로 가정하지 않으며, 조건문의 형태로 독립적인 명제가 된다.
성질
명제 논리(propositional logic)에서는 제약 없이 성립한다. 1차 논리(first-order logic)에서는 추론 과정 $\mathcal{D}$가 $P$의 자유 변수(free variable)에 대한 전칭 도입(universal introduction)을 사용하지 않은 경우에 한하여 성립한다. 이는 자유 변수가 조건문의 전제 밖으로 벗어나 전칭화되는 것을 방지하기 위한 제약 조건이다.
예시
고전 명제 논리 또는 직관 명제 논리에서 논리식 $(P \land Q) \implies (Q \land P)$는 함의 도입을 사용하여 다음과 같이 유도할 수 있다.
- $[P \land Q]$를 가정한다.
- 연언 소거(conjunction elimination)를 통해 각각 $P$와 $Q$를 얻는다.
- 연언 도입(conjunction introduction)을 통해 $Q \land P$를 얻는다.
- 함의 도입을 적용하여 $(P \land Q) \implies (Q \land P)$를 결론으로 도출한다.
의의
함의 도입은 조건 증명(conditional proof)이라고도 불리며, 수학적 증명에서 가정법(假定法)에 해당하는 논리적 근거를 제공한다. 어떤 명제 $P$를 가정한 상태에서 $Q$가 증명된다면, $P$라는 가정 없이도 $P \implies Q$라는 조건명제를 참으로 주장할 수 있게 해준다. 이는 자연 연역(natural deduction) 체계에서 핵심적인 추론 규칙 중 하나이다.
