논리학에서, 쌍조건문 도입(雙條件文導入, 영어: biconditional introduction)은 두 명제가 서로 함의한다는 것으로부터 두 명제의 동치를 유도하는 추론 규칙이다. 명제 논리에서 타당한 추론 규칙(rule of inference)에 해당하며, 자연 연역(natural deduction) 체계에서 쌍조건문을 증명에 도입할 때 사용된다.
정의
쌍조건문 도입은 다음과 같이 형식화된다.
$$ \frac{P \to Q \quad Q \to P}{\therefore P \leftrightarrow Q} $$
즉, 'P이면 Q이다'와 'Q이면 P이다'가 모두 참일 때, 'P이면 그리고 오직 그때만 Q이다'(P iff Q)를 결론으로 내릴 수 있다. 예를 들어, "내가 숨을 쉰다면 나는 살아 있다"와 "내가 살아 있다면 나는 숨을 쉰다"라는 두 조건문이 모두 참일 때, "나는 숨을 쉰다면 그리고 오직 그때만 살아 있다"라는 쌍조건문을 추론할 수 있다.
표기법
쌍조건문 도입은 시퀀트(sequent) 표기법으로 다음과 같이 나타낼 수 있다.
$$ (P \to Q), (Q \to P) \vdash (P \leftrightarrow Q) $$
여기서 $\vdash$는 메타 논리 기호로, 왼쪽의 논리식들로부터 오른쪽의 논리식을 증명할 수 있음을 의미한다.
또한 명제 논리의 항진식(tautology)으로서 다음과 같이 표현되기도 한다.
$$ ((P \to Q) \land (Q \to P)) \to (P \leftrightarrow Q) $$
성질
쌍조건문 도입은 쌍조건문 제거(biconditional elimination)의 역(inverse)에 해당한다. 직관 논리(intuitionistic logic)에서도 성립하므로, 고전 논리(classical logic)를 비롯한 모든 초직관 논리(superintuitionistic logic)에서 성립한다.
같이 보기
- 쌍조건문 (biconditional)
- 조건문 도입 (conditional introduction)
- 조건문 제거 (modus ponens)
- 추론 규칙 (rule of inference)
