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

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

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

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



推論規則【二重否定除去律】のもとで【矛盾に関する規則】は派生推論規則

【命題論理における自然演繹の必要最小限のセット：type2】
　　　⇒導入則・⇒除去則・∧導入則・∧除去則・∨導入則・∨ 除去則・¬導入則・¬除去則　
　　　¬¬除去則
　において、
　　　矛盾に関する規則　
　が派生推論規則になる。
　　
【どうして？】

　　[前原『記号論理入門』§8(pp.58-9)]


[step0]
　[¬A]1　[⋏]2　　　

(∧導入)
¬A∧⋏　
(∧除去)
⋏
(¬導入)1
¬¬A
(⇒導入)2
(⋏⇒¬¬A)
[step1]

　⋏　  
　[¬A]1　[⋏]2　　　

(∧導入)
¬A∧⋏　
(∧除去)
⋏
(¬導入)1
¬¬A
(⇒導入)2
⋏⇒¬¬A　

( ⇒除去)

¬¬A

[step2]

　⋏　  
　[¬A]1　[⋏]2　　　

(∧導入)
¬A∧⋏　
(∧除去)
⋏
(¬導入)1
¬¬A
(⇒導入)2
⋏⇒¬¬A　

( ⇒除去)

¬¬A
(二重否定除去)
A

ここで、止めると、
　矛盾に関する規則　
　　　
  ⋏　


 
 A
　になっている。

[step3]

　[⋏]3  
　[¬A]1　[⋏]2　　　

(∧導入)
¬A∧⋏　
(∧除去)
⋏
(¬導入)1
¬¬A
(⇒導入)2
⋏⇒¬¬A　

( ⇒除去)

¬¬A
(二重否定除去)
A
(⇒導入)3
⋏⇒A






【文献】
　・前原『記号論理入門』§8.4排中律を公理とせず、二重否定除去を推論規則とした【type2】において、矛盾の公理の証明(pp.58-9)



　　






　　　　

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





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