함의 도입

틀:위키데이터 속성 추적 논리학에서, 함의 도입(含意導入, 틀:Llang)은 가언 명제를 유도하는 추론 규칙이다.

정의

논리식 $P$를 가정으로 삼아 과정 $𝒟$를 통해 논리식 $Q$를 유도한 것을

$\begin{array}{c}P\\ (𝒟)\\ Q\end{array}$

로 나타내자. 그렇다면 함의 도입은 다음과 같다.틀:Rp틀:Rp

$\begin{array}{c}[P]\\ (𝒟)\\ Q\\ P⟹Q\end{array}$

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

성질

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

예

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

$(P\wedge Q)⟹(Q\wedge P)$

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

$\begin{array}{c}\begin{array}{c}[P\wedge Q]\end{array}\begin{array}{c}[P\wedge Q]\end{array}\\ \begin{array}{c}QP\end{array}\\ \begin{array}{c}Q\wedge P\end{array}\\ (P\wedge Q)⟹(Q\wedge P)\end{array}$

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

같이 보기

• 함의 소거