선언 도입

논리학에서 선언 도입(選言導入, 영어: disjunction introduction)은 주어진 명제로부터 이를 한 성분으로 하는 선언 명제를 유도하는 추론 규칙이다.

정의

선언 도입은 다음과 같은 두 개의 추론 규칙이다.^{:183, §16.3.1}

${\begin{matrix}P\\\hline P\lor Q\end{matrix}}\qquad {\begin{matrix}P\\\hline Q\lor P\end{matrix}}$

또는

$P\vdash P\lor Q\qquad P\vdash Q\lor P$

여기서

• $P$, $Q$는 논리식을 나타내는 메타 변수이다.
• $\lor$는 논리합이다.
• 수평선은 증명 과정의 이웃한 두 단계를 구분하는 메타 논리 기호이다.
• $\vdash$는 왼쪽에 놓인 논리식들로부터 오른쪽에 놓인 논리식을 증명할 수 있음을 나타내는 메타 논리 기호이다.

성질

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

같이 보기

• 선언 소거
• 연언 도입