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

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

・命題論理の公理系の諸タイプ ： ヒルベルト流の公理系/ゲンツェン流の公理系（自然演繹）
　※命題論理関連ページ：命題論理の論理式 /命題論理の意味論[真理値/真理関数/真理値表/論理式の真理値の決定原理/真理値分析/恒真式・恒偽式 ] 　　
　※論理関連ページ ：  論理記号　
　*　論理目次/総目次/更新履歴　

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




推論規則【矛盾についての規則】・公理【排中律】のもとで【二重否定除去律】は派生推論規則

【命題論理における自然演繹の必要最小限のセット：type3】
　　　⇒導入則・⇒除去則・∧導入則・∧除去則・∨導入則・∨ 除去則・¬導入則・¬除去則　
　　　矛盾に関する規則・排中律　
　において、
　　¬¬除去則　
　が定理として成り立つ。
　　
【どうして？】

　∨除去則・¬除去則・矛盾に関する規則・¬¬除去則のみを用いた　¬¬除去則の導出。

[step1]
　
　　
 　[仮定]　
　¬A　　

　[仮定]　
¬¬A

(¬除去 )

⋏



[step2]

　　
 　[仮定]　
　¬A　　

　[仮定]　
¬¬A

(¬除去 )

⋏

(矛盾に関する規則 )
A
　Aと¬(A∨¬A)という前提の下で、⋏　　

[step3]

　　
 [排中律]
A∨¬A

[仮定]
 A 
　　
 　[仮定]　
　¬A　　

　[仮定]　
¬¬A

(¬除去 )

⋏

(矛盾に関する規則 )
A








[step4]
　　
 [排中律]
A∨¬A

[仮定]
 [A]1

　　
 　[仮定]　
　[¬A]1　

　[仮定]　
¬¬A

(¬除去 )

⋏

(矛盾に関する規則 )
A


(∨除去則)1

A

　推論規則としての二重否定除去律
　　　
 ¬¬A

　



A
　は以上で得られた。

　定理となる論理式を獲得したいときは、次のステップへ。

[step5]
　　
 [排中律]
A∨¬A

[仮定]
 [A]1

　　
 　[仮定]　
　[¬A]1　

　[仮定]　
 [¬¬A]2

(¬除去 )

⋏

(矛盾に関する規則 )
A


(∨除去則)1

A

(⇒導入則)2

¬¬A　⇒　A







【文献】
　・前原『記号論理入門』§8(p.57);
　・高崎『数理論理学入門』III. VII. 自然演繹（その１）1. 命題論理の形式化（NK,NJ）2.1[例5]
　・林『数理論理学』例1.11(p.33)



　　






　　　　

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





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