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

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

命題論理の公理系の諸タイプ : ヒルベルト流の公理系/ゲンツェン流の公理系(自然演繹)

 命題論理関連ページ:命題論理の論理式 /命題論理の意味論[真理値/真理関数/真理値表/論理式の真理値の決定原理/真理値分析/恒真式・恒偽式 ]   
 論理関連ページ :  論理記号 
 * 論理目次/総目次/更新履歴 

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




推論規則【二重否定除去律】のもとで【排中律】は定理


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

 ・∨導入則¬導入則¬除去則¬¬除去則のみを用いた排中律 の導出。
  [前原『記号論理入門』§8(p.58)]

[step1]
 
仮定1
A


( ∨導入)

A∨¬A


  (⇒導入則をつかうと、A⇒A∨¬A [無前提]となるが、まだ変形するので、そうしない)

[step2]

仮定1
A


( ∨導入)

A∨¬A
 仮定2 
 ¬(A∨¬A) 


(¬除去 )


 Aと¬(A∨¬A)という前提の下で、  

[step3]
[仮定1]
[A]


( ∨導入)

A∨¬A
   仮定2  
 ¬(A∨¬A) 


(¬除去 )




( ¬導入)仮定1を解消

¬A

  ¬(A∨¬A)という前提の下で、¬A

[step4]
[仮定1]
[A]


( ∨導入)

A∨¬A
 仮定2 
 ¬(A∨¬A) 


(¬除去 )




( ¬導入)仮定1を解消

¬A


( ∨導入)

A∨¬A





【文献】
 ・前原『記号論理入門』§8 
      ・「二重否定の除去というものは、排中律と矛盾の公理の双方を合わせたものと同等ということになります」(p.59)
           ・排中律を公理とせず、二重否定除去を推論規則とした【type2】において、排中律の証明(p.58)
           ・排中律を公理とせず、二重否定除去を推論規則とした【type2】において、矛盾の公理の証明(pp.58-9)

  ・戸田山『論理学をつくる』 9.2.5は、【必要最小限のセットtype2】において、排中律を証明(p.232)。
 ・林『数理論理学』例1.11(p.33):二重否定除去律を公理のかたちにした場合。



  






    

  ¬(A∨¬A)という前提の下で、A∨¬A

[step5]

[仮定1]
[A]


( ∨導入)

A∨¬A
 仮定2 
 ¬(A∨¬A) 


(¬除去 )




( ¬導入)仮定1を解消

¬A


( ∨導入)

A∨¬A
  仮定2 
¬(A∨¬A)


(¬除去 )



  ¬(A∨¬A)という前提の下で、 


[step6]

[仮定1]
[A]


( ∨導入)

A∨¬A
 [仮定2] 
 [¬(A∨¬A)] 


(¬除去 )




( ¬導入)仮定1を解消

¬A


( ∨導入)

A∨¬A
 [仮定2] 
[¬(A∨¬A)]


(¬除去 )




( ¬導入)仮定2を解消

¬¬(A∨¬A)

 前提なしに、 ¬¬(A∨¬A) 

[step7]
[仮定1]
[A]


( ∨導入)

A∨¬A
 [仮定2] 
 [¬(A∨¬A)] 


(¬除去 )




( ¬導入)仮定1を解消

¬A


( ∨導入)

A∨¬A
 [仮定2] 
[¬(A∨¬A)]


(¬除去 )




( ¬導入)仮定2を解消

¬¬(A∨¬A)

(¬¬除去則)
A∨¬A

 前提なしに、 (A∨¬A) 



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






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