선언 도입

1. 개요

선언 도입은 두 개의 추론 규칙으로, 논리식 P로부터 P ∨ Q를 유도하거나 Q ∨ P를 유도할 수 있다. 이는 시퀀트 표기법으로 P ⊢ (P ∨ Q)로, 또는 명제 논리의 항진명제 P → (P ∨ Q)로 표현될 수 있다. 선언 도입은 직관 논리에서 성립하며, 고전 논리를 포함한 모든 초직관 논리에서도 성립한다.

2. 정의

선언 도입은 이미 증명된 명제에 논리합을 이용하여 새로운 명제를 도출하는 추론 규칙이다. 어떤 명제가 참이면, 그 명제에 다른 명제를 '또는'으로 연결해도 여전히 참이라는 규칙이다.

예를 들어 "오늘 비가 온다"라는 명제가 참이라면, "오늘 비가 온다" 또는 "오늘 눈이 온다"라는 명제도 참이다. 이는 전자가 이미 참이기 때문에, 후자의 참/거짓 여부와 관계없이 전체 명제는 참이 되기 때문이다.

선언 도입은 명제 논리에서 복잡한 논리적 추론을 단순화하는 데 사용된다.

2.1. 형식 표기법

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

2.1.1. 시퀀트 표기법

:$P\; \backslash vdash\; (P\; \backslash lor\; Q)$
여기서 $\backslash vdash$는 어떤 논리 체계에서 $P\; \backslash lor\; Q$가 $P$의 구문론적 결과임을 의미하는 메타논리 기호이다.

2.1.2. 명제 논리

명제 논리에서 선언 도입 규칙은 항진명제 또는 정리로 다음과 같이 표현할 수 있다.

:$P\; \backslash to\; (P\; \backslash lor\; Q)$

여기서 $P$와 $Q$는 어떤 형식 체계에서 표현된 명제이다.

3. 성질

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