선언 도입 문서 원본 보기

{{위키데이터 속성 추적}}
[[논리학]]에서 '''선언 도입'''(選言導入, {{llang|en|disjunction introduction}})은 주어진 명제로부터 이를 한 성분으로 하는 [[선언 명제]]를 유도하는 [[추론 규칙]]이다.

== 정의 ==
'''선언 도입'''은 다음과 같은 두 개의 [[추론 규칙]]이다.<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}}
:<math>\begin{matrix}
P \\
\hline
P\lor Q
\end{matrix}\qquad\begin{matrix}
P \\
\hline
Q\lor P
\end{matrix}</math>
또는
:<math>P\vdash P\lor Q\qquad P\vdash Q\lor P</math>
여기서
* <math>P</math>, <math>Q</math>는 [[논리식]]을 나타내는 메타 변수이다.
* <math>\lor</math>는 [[논리합]]이다.
* 수평선은 증명 과정의 이웃한 두 단계를 구분하는 메타 논리 기호이다.
* <math>\vdash</math>는 왼쪽에 놓인 논리식들로부터 오른쪽에 놓인 논리식을 증명할 수 있음을 나타내는 메타 논리 기호이다.

== 성질 ==
[[직관 논리]]에서 성립하며, 따라서 [[고전 논리]]를 비롯한 모든 [[초직관 논리]]에서 성립한다.

== 같이 보기 ==
* [[선언 소거]]
* [[연언 도입]]

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

[[분류:추론 규칙]]
[[분류:고전 논리]]
[[분류:직관 논리]]
[[분류:명제 논리 정리]]