쌍조건문 도입

"오늘의AI위키"는 AI 기술로 일관성 있고 체계적인 최신 지식을 제공하는 혁신 플랫폼입니다.
"오늘의AI위키"의 AI를 통해 더욱 풍부하고 폭넓은 지식 경험을 누리세요.

1. 개요

쌍조건문 도입은 논리학의 추론 규칙 중 하나로, P → Q와 Q → P가 참일 때 P ↔ Q를 결론으로 도출한다. 시퀀트 표기법으로는 (P → Q), (Q → P) ⊢ (P ↔ Q)로 나타낼 수 있으며, 명제 논리의 항진명제 또는 정리로 ((P → Q) ∧ (Q → P)) → (P ↔ Q)로 표현할 수 있다. 이 규칙은 직관 논리에서 성립하며, 고전 논리를 포함한 모든 초직관 논리에서도 유효하다.

쌍조건문 도입
규칙 정보
종류추론 규칙
분야명제 논리
설명만약 P → Q가 참이고 Q → P가 참이라면, P ↔ Q가 참이라고 추론할 수 있음.
형식P → Q, Q → P ∴ P ↔ Q
📚 더 읽어볼만한 페이지
  • 추론 규칙 - 드 모르간의 법칙
    드 모르간의 법칙은 명제 논리, 술어 논리, 집합론, 부울 대수 등에서 결합 또는 분리의 부정을 각 요소의 부정의 분리 또는 결합으로 표현하는 논리적 원리이다.
  • 추론 규칙 - 부정 도입
    부정 도입은 기호 논리학의 추론 규칙으로, P가 참일 경우 모순된 결론이 도출되므로 P가 거짓임을 이끌어내는 방법이다.
  • 고전 논리 - 명제 논리
    명제 논리는 진릿값을 갖는 명제를 다루는 형식 논리 체계로, 논리 연결사를 사용하여 명제를 결합하고 논증을 분석하며, 다양한 논리학자들의 연구를 통해 발전하여 컴퓨터 과학 및 수리 논리학에서 활용된다.
  • 고전 논리 - 동일성
    동일성은 철학에서 자기 자신과 일치하고 자기 동일적으로 존재하며 다른 것에 의존하지 않는 개념으로, 고대부터 현대까지 다양한 철학자와 여러 분야에서 논의되고 활용되어 왔다.
  • 직관 논리 - 에밀 보렐
    프랑스의 수학자이자 정치인인 에밀 보렐은 측도론과 확률론에 기여하고 보렐 집합 개념으로 알려져 있으며, 무한 원숭이 정리와 같은 사고 실험과 게임 이론 연구, 프랑스 하원 의원 및 해군부 장관 역임, 레지스탕스 운동 참여, 파리 통계 연구소 및 앙리 푸앵카레 연구소 설립 기여 등으로 다양한 업적을 남겼다.
  • 직관 논리 - 후건 부정
    후건 부정은 "P이면 Q이다"라는 조건문과 "Q가 아니다"라는 명제를 통해 "P가 아니다"라는 결론을 내리는 추론 규칙으로, 논리적 사고의 중요한 도구이며 다양한 방식으로 표현되고 증명될 수 있다.

2. 정의

쌍조건문 도입은 다음과 같은 추론 규칙이다.
:
\begin{matrix}
P\implies Q\qquad Q\implies P \\
\hline
P\iff Q
\end{matrix}

또는
:P\implies Q,Q\implies P\vdash P\iff Q
여기서
* P, Q논리식을 나타내는 메타 변수이다.
* \implies는 함의이다.
* \iff는 동치이다.
* 수평선은 증명 과정의 이웃한 두 단계를 구분하는 메타 논리 기호이다.
* \vdash는 왼쪽에 놓인 논리식들로부터 오른쪽에 놓인 논리식을 증명할 수 있음을 나타내는 메타 논리 기호이다.

3. 형식 표기법

쌍조건문 도입은 다음과 같은 추론 규칙이다.

:\begin{matrix}
P\implies Q\qquad Q\implies P \\
\hline
P\iff Q
\end{matrix}

또는

:P\implies Q,Q\implies P\vdash P\iff Q

여기서

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

쌍조건문 도입 규칙은 시퀀트 표기법으로 다음과 같이 나타낼 수 있다.

:(P \to Q), (Q \to P) \vdash (P \leftrightarrow Q)

여기서 \vdashP \to QQ \to P가 증명에 모두 포함될 때 P \leftrightarrow Q가 구문론적 함의임을 의미하는 메타논리 기호이다.

또는 명제 논리의 진리 함수적 항진명제 또는 정리의 진술로 나타낼 수 있다.

:((P \to Q) \land (Q \to P)) \to (P \leftrightarrow Q)

여기서 PQ는 일부 형식 체계에서 표현된 명제이다.

4. 성질

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