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

・命題論理の自然演繹：推論規則公理一覧　
　・推論規則：⇒導入則・⇒除去則・∧導入則・∧除去則・∨導入則・∨除去則・¬導入則・¬除去則・背理法・二重否定除去律・矛盾除去
　・公理　　：排中律　
　※命題論理関連ページ：命題論理の論理式/命題論理の意味論/命題論理のシンタックス　 　　
　※論理関連ページ ：  論理記号　
　*　論理目次/総目次/更新履歴　

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



命題論理の形式的体系「自然演繹」における推論規則：「二重否定除去律」





【二重否定除去律】

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

　(1)　論理式「¬¬A」を、論理式「A」に書き換えてよい。

　(2)　書き換え後に引き継ぐ仮定は、書き換え前の仮定のすべて。



　




【文献】
　・戸田山『論理学をつくる』9.2.1(p.227);9.3.2矛盾記号の導入(p.235)
　・野矢『論理学』1-2-3公理系LP(pp.66-7)
　・野矢『入門！論理学』第5章「標準的な命題論理の体系」(p.146).



　　
・二重否定除去律は、下図で表される。



【推論規則：二重否定除去】　

　
 ¬¬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)]
　　などと呼ばれる。

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


　　　*　排中律の代わりに
　　　　　二重否定の除去法則「¬¬A⇒A」を公理としてもよいし、
　　　　　
　　　　　　　　　　
   ¬¬A　

(¬¬除去)
 
 A
  　　　　を推論規則としてもよい。(前原昭二『記号論理入門』2章演繹§8.排中律についてpp.52-59証明付)


　　　　　・7.8古典論理の体系HK(pp.165-173):ヒルベルト流
　　　　　　　　　　　　　HK=HM+DNE二重否定除去律 = HM+EFQ矛盾に関する推論規則+LEM排中律(pp.172-3)