命題論理の「自然演繹」の推論規則　トピック一覧　　

・命題論理の自然演繹：推論規則公理一覧　
　・推論規則：⇒導入則・⇒除去則・∧導入則・∧除去則・∨導入則・∨除去則・¬導入則・¬除去則・背理法・二重否定除去律・矛盾除去
　・公理　　：排中律　

　※命題論理関連ページ：命題論理の論理式/命題論理の意味論/命題論理のシンタックス　 　　
　※論理関連ページ ：  論理記号　
　*　論理目次/総目次/更新履歴　

※述語論理の場合は、林晋,鹿島亮を参照。



命題論理の形式的体系「自然演繹」における推論規則：「背理法」the reductio ad absurdum rule (RAA)





【背理法】

　*　下記 A には、どんな論理式を入れてもよい。

　(1)　仮定¬Aのもとで与えられた「⋏」を、論理式「A」に書き換えてよい。

　(2)　ただし、
　　　　論理式「A」へ書き換えた際に引き継ぐ仮定は、
　　　　　書き換え前の仮定のすべてではなく、
　　　　　書き換え前の仮定から、仮定¬Aを差し引いた分だけ。

　　　つまり、
　　　　仮定Xと仮定¬Aのもとで与えられた　⋏　は、
　　　　仮定Xと仮定¬Aのもとでの「論理式A」ではなく
　　　　仮定Xのもとでの「論理式A」に書き換えられることになる。

　　　この仮定引継手続きは、
　　　　「仮定¬Aが落ちる」(discharge)[高崎『数理 論理学入門』VII.1.]
　　　　「仮定¬Aが解消される」[鹿島『数理論理学』図2.2(p.29)]
　　　　「仮定¬Aが打ち消される」(discharge)
　　　　　　　　　　[戸次 『数理論理学』8.1.2打ち消し操作(p.178)]
　　　　「仮定¬Aがキャンセルされる」
　　　　　　　　　　[戸田山『論理学をつくる』9.1.4(p.219)]
  　　　などと表現される。



　




【文献】
　・鹿島『数理論理学』図2.2(p.29)
　・戸次 『数理論理学』定義8.19NKの推論規則(p.187)
　・van Dalen,Logic and Structure(3rd ed.) 1.4Natural Deduction(pp.29-39):"the reductio ad absurdum rule (RAA)"(p.30)

　　
・背理法は、下図で表される。



【推論規則：背理法】　

　
 [¬A]
：
⋏

(背理法)

A
　




　　この図は、
　　　　・演繹図　[高崎VI. 2.1]　
　　　　・推論図　[前原p.38;高崎VI. 2.1]　
　　　　・証明図 proof diagram　[戸田山『論理学をつくる』8.1.1(p.177);飯田編(p.90);高崎VI. 2.1;向井pp15-16]proof figure[清水『記号論理学』p.97]
　　　　・導出図　[鹿島『数理論理学』図2.2(p.29)]
　　などと呼ばれる。

→　命題論理の自然演繹　：トピック一覧　
→　命題論理のシンタックス　：トピック一覧
→　総目次