쌍조건문 소거

틀:위키데이터 속성 추적 논리학에서, 쌍조건문 소거(雙條件文消去, 틀:Llang)는 두 명제의 동치로부터 두 명제의 서로 함의를 유도하는 추론 규칙이다.

정의

쌍조건문 소거는 다음과 같은 두 개의 추론 규칙이다.틀:Rp

$\begin{array}{c}P⟺Q\\ P⟹Q\end{array}\begin{array}{c}P⟺Q\\ Q⟹P\end{array}$

또는

$P⟺Q⊢P⟹QP⟺Q⊢Q⟹P$

여기서

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

성질

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

같이 보기

• 쌍조건문 도입