함의 도입

논리학에서, 함의 도입(含意導入, 영어: implication introduction)은 가언 명제를 유도하는 추론 규칙이다.

정의

논리식 $P$ 를 가정으로 삼아 과정 ${\mathcal {D}}$ 를 통해 논리식 $Q$ 를 유도한 것을

{\begin{matrix}P\\({\mathcal {D}})\\Q\end{matrix}}

로 나타내자. 그렇다면 함의 도입은 다음과 같다.^[1]^{:183, §16.3.1}^[2]^{:29, §2.4}

{\begin{matrix}[P]\\({\mathcal {D}})\\Q\\\hline P\implies Q\end{matrix}}

여기서 $[P]$ 는 $P$ 의 가정을 취소한다는 뜻이다. 즉, 함의 도입을 사용하여 유도한 결론 $P\implies Q$ 는 $P$ 를 전제로 가정하지 않는다.

명제 논리에서 성립한다. 1차 논리에서는 ${\mathcal {D}}$ 가 $P$ 의 자유 변수에 대한 전칭 도입을 사용하지 않을 경우에 한하여 성립한다.

고전 명제 논리 또는 직관 명제 논리에서, 논리식

(P\land Q)\implies (Q\land P)

를 함의 도입을 사용하여 다음과 같이 유도할 수 있다.

{\begin{matrix}{\begin{matrix}[P\land Q]\\\hline \end{matrix}}\qquad {\begin{matrix}[P\land Q]\\\hline \end{matrix}}\\{\begin{matrix}Q\qquad \qquad \quad P\\\hline \end{matrix}}\\{\begin{matrix}\qquad \quad \;Q\land P\qquad \quad \;\\\hline \end{matrix}}\\(P\land Q)\implies (Q\land P)\end{matrix}}

둘째 줄은 첫째 줄에서 연언 소거를 사용하여 유도하며, 셋째 줄은 둘째 줄에서 연언 도입을 사용하여 유도한다. 마지막 줄은 함의 도입을 사용한다.

↑ Lover, Robert (2008). 《Elementary Logic》 (영어). London: Springer. doi:10.1007/978-1-84800-082-7. ISBN 978-1-84800-081-0. LCCN 2008928865.
↑ van Dalen, Dirk (2013). 《Logic and Structure》. Universitext (영어) 5판. London: Springer. doi:10.1007/978-1-4471-4558-5. ISBN 978-1-4471-4557-8. ISSN 0172-5939. LCCN 2012953020.