否定導入

否定導入（ひていどうにゅう、テンプレート:Lang-en-short）は、命題論理の分野における推論規則、あるいはテンプレート:仮リンクである。

否定導入は、ある前件が後件とその補元の両方を含意するならば、これは前件の否定を含意するということを述べる。

形式的記法

これは次のように書くことができる。

$((P\to Q)\wedge (P\to \mathrm{\neg }Q))\to \mathrm{\neg }P$

その使用例としては、単一の事実から2つの矛盾する言明を証明しようとする試みが挙げられる。例えば、ある人が「電話が鳴るのを聞くといつも私は幸せだ」と述べ、次に「電話が鳴るのを聞くといつも私は幸せではない」と述べたとすると、その人は電話が鳴るのを聞くことは決してないと推論することができる。

多くの背理法による証明は、否定導入を推論図式として用いる。すなわち、¬P を証明するために、矛盾を導くために P を仮定し、そこから Q と ¬Q という2つの矛盾する帰結を導く。後者の矛盾は P を不可能にするので、¬P が成り立たなければならない。

証明

$\mathrm{\neg }P$ を $P\to \mathrm{\perp }$ として同定すると、この原理は、すでにテンプレート:仮リンクにおけるフレーゲの定理の特殊な場合として得られる。

別の導出では、$\mathrm{\neg }(A\wedge B)$ のカリー化された同値な形として $A\to \mathrm{\neg }B$ を利用する。これを2回用いると、この原理は $(P\wedge (P\to Q))\wedge \mathrm{\neg }(P\wedge Q)$ の否定と同値であることがわかり、これはモーダスポネンスと連言に関する規則により、$P\wedge Q$ についての妥当な無矛盾律それ自体と同値である。

選言の導入を経由する古典的な導出は、次のように与えられる。

段階	命題	導出
1	$(P\to Q)\wedge (P\to \mathrm{\neg }Q)$	前提
2	$(\mathrm{\neg }P\vee Q)\wedge (\mathrm{\neg }P\vee \mathrm{\neg }Q)$	テンプレート:仮リンクの古典的な同値変形
3	$\mathrm{\neg }P\vee (Q\wedge \mathrm{\neg }Q)$	分配律
4	$\mathrm{\neg }P\vee \mathrm{\perp }$	$Q$ についての無矛盾律
5	$\mathrm{\neg }P$	選言三段論法 (3,4)

関連項目

• 背理法