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

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

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



命題論理の形式的体系「自然演繹」における公理：「排中律」
・「自然演繹」という《命題論理の形式的体系》は、
　　下記論理式を、その《公理》に指定している。　

・つまり、
　下記は、
　「自然演繹」という《命題論理の形式的体系》のなかで、　
　　無条件に作成してよい論理式。




【文献】
　・前原昭二『記号論理入門』2章§8(pp.52-9)特にp.40;
　・高崎金久『数理論理学入門』VII. 自然演繹（その１）1. 命題論理の形式化（NK,NJ）　　



　　






【排中律】

　A∨¬A　





　*　使用例は？→対偶律(2)証明(step07)

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

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

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


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