쌍조건문 도입
1. 개요
쌍조건문 도입은 논리학의 추론 규칙 중 하나로, 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. 정의
쌍조건문 도입은 다음과 같은 추론 규칙이다.
:
또는
:
여기서
* , 는 논리식을 나타내는 메타 변수이다.
* 는 함의이다.
* 는 동치이다.
* 수평선은 증명 과정의 이웃한 두 단계를 구분하는 메타 논리 기호이다.
* 는 왼쪽에 놓인 논리식들로부터 오른쪽에 놓인 논리식을 증명할 수 있음을 나타내는 메타 논리 기호이다.
3. 형식 표기법
쌍조건문 도입은 다음과 같은 추론 규칙이다.
:
또는
:
여기서
* , 는 논리식을 나타내는 메타 변수이다.
* 는 함의이다.
* 는 동치이다.
* 수평선은 증명 과정의 이웃한 두 단계를 구분하는 메타 논리 기호이다.
* 는 왼쪽에 놓인 논리식들로부터 오른쪽에 놓인 논리식을 증명할 수 있음을 나타내는 메타 논리 기호이다.
쌍조건문 도입 규칙은 시퀀트 표기법으로 다음과 같이 나타낼 수 있다.
:
여기서 는 와 가 증명에 모두 포함될 때 가 구문론적 함의임을 의미하는 메타논리 기호이다.
또는 명제 논리의 진리 함수적 항진명제 또는 정리의 진술로 나타낼 수 있다.
:
여기서 와 는 일부 형식 체계에서 표현된 명제이다.