부정소개

부정 도입은 명제 미적분학 분야에서 추론, 즉 변환 규칙이다.

부정 소개는 주어진 선행자가 결과물과 그 보완점을 모두 내포한다면 선행은 모순이라고 말한다.^[1][2]

형식 표기법

이것은 다음과 같이 쓸 수 있다: $({\displaystyle P}$→ ${\displaystyle Q}$ ${\displaystyle )}$ ${\displaystyle \wedge }$(${\displaystyle P}$ →${\displaystyle \mathrm{\neg }}$ ${\displaystyle Q}$)${\displaystyle }$→ $¬$ P {\$displaystyle$ (P$\rightarrow Q)\$land (P$\rightarrow \neg$ Q)\rightarrow $\neg P}$

이것의 사용의 예는 하나의 사실로부터 두 개의 모순된 진술을 증명하려는 시도일 것이다. 예를 들어 '전화벨이 울릴 때마다 나는 행복하다'고 말한 다음 '전화벨이 울릴 때마다 짜증이 난다'고 진술한다면, 전화벨이 울릴 때(아무도 행복할 수 없고 동시에 짜증이 날 수 없다고 가정하면) 전화벨이 울리는 것을 결코 듣지 않는다고 추론할 수 있다.

모순에 의한 많은 증명들은 부정 도입을 추론 체계로 사용한다: :P를 증명하기 위해, 모순 P에 대해 가정하고, 그것으로부터 두 개의 모순된 추론 Q와 ¬Q를 도출한다. 후자의 모순은 P를 불가능하게 만들기 때문에, pP는 버텨야 한다.

증명

스텝	프로포지션	파생
1	$(P\displaystyle (P\to Q)\land (P\to \neg Q)}$	주어진
2	$(\displaystyle(\neg P\lor Q)\land(\neg P\lor \neg Q)}$	물질적 함축성
3	$\displaystyle \neg P\lor (Q\land \neg Q)}$	분배성
4	$\displaystyle \neg(Q\land \neg Q)}$	비반전성의 법칙
5	$\displaystyle \neg P}$	이절 삼단논법 (3,4)

참조