함의 도입 문서 원본 보기

{{위키데이터 속성 추적}}
[[논리학]]에서, '''함의 도입'''(含意導入, {{llang|en|implication introduction}})은 [[가언 명제]]를 유도하는 [[추론 규칙]]이다.

== 정의 ==
[[논리식]] <math>P</math>를 가정으로 삼아 과정 <math>\mathcal D</math>를 통해 논리식 <math>Q</math>를 유도한 것을
:<math>\begin{matrix}
P \\
(\mathcal D) \\
Q
\end{matrix}</math>
로 나타내자. 그렇다면 '''함의 도입'''은 다음과 같다.<ref name="Lover">{{서적 인용
|성=Lover
|이름=Robert
|제목=Elementary Logic
|언어=en
|출판사=Springer
|위치=London
|날짜=2008
|isbn=978-1-84800-081-0
|lccn=2008928865
|doi=10.1007/978-1-84800-082-7
}}</ref>{{rp|183, §16.3.1}}<ref name="van Dalen">{{서적 인용
|성=van Dalen
|이름=Dirk
|제목=Logic and Structure
|url=https://archive.org/details/logicstructure0005dale
|언어=en
|판=5
|총서=Universitext
|출판사=Springer
|위치=London
|날짜=2013
|isbn=978-1-4471-4557-8
|issn=0172-5939
|doi=10.1007/978-1-4471-4558-5
|lccn=2012953020
}}</ref>{{rp|29, §2.4}}
:<math>\begin{matrix}
[P] \\
(\mathcal D) \\
Q \\
\hline
P\implies Q
\end{matrix}</math>
여기서 <math>[P]</math>는 <math>P</math>의 가정을 취소한다는 뜻이다. 즉, 함의 도입을 사용하여 유도한 결론 <math>P\implies Q</math>는 <math>P</math>를 전제로 가정하지 않는다.

== 성질 ==
[[명제 논리]]에서 성립한다. [[1차 논리]]에서는 <math>\mathcal D</math>가 <math>P</math>의 [[자유 변수]]에 대한 [[전칭 도입]]을 사용하지 않을 경우에 한하여 성립한다.

== 예 ==
고전 명제 논리 또는 직관 명제 논리에서, 논리식
:<math>(P\land Q)\implies(Q\land P)</math>
를 함의 도입을 사용하여 다음과 같이 유도할 수 있다.
:<math>
\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}
</math>
둘째 줄은 첫째 줄에서 [[연언 소거]]를 사용하여 유도하며, 셋째 줄은 둘째 줄에서 [[연언 도입]]을 사용하여 유도한다. 마지막 줄은 함의 도입을 사용한다.

== 같이 보기 ==
* [[함의 소거]]

== 각주 ==
{{각주}}

[[분류:추론 규칙]]
[[분류:명제 논리]]
[[분류:조건부]]