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

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

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

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

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




推論規則【背理法】のもとで【排中律】は定理


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



[step1]
  
 [仮定] 
 A  



[step2]
  
 [仮定] 
 A  



(∨導入 )


 A∨¬A 

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



(∨導入 )


 A∨¬A 



  

[step4]
  
 [仮定] 
 ¬(A∨¬A)  
  
 [仮定]1 
 [A]  



(∨導入)


 A∨¬A 



(¬除去)





(¬導入)仮定1を解消

¬A

[step5]
  
 [仮定] 
 ¬(A∨¬A)  
  
 [仮定]1 
 A  



(∨導入 )


 A∨¬A 



(¬除去)





(¬導入)仮定1を解消

¬A


(∨導入)

A∨¬A






【文献】
 ・鹿島『数理論理学』2章自然演繹-2.2【導出図の例6】(p.32) 
 ・戸次 『数理論理学』練習問題8.21(p.187):証明なし
 ・van Dalen,Logic and Structure(3rd ed.) 1.6(p.50-51):左掲の証明とは、少し違う。要比較。
 ・野矢『論理学』1-2-3-LP-命題論理の諸定理-定理2(p.70);付録-定理2(p.216)背理法から導出。



  






    


[step6]
  

[仮定]
 ¬(A∨¬A)  

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



(∨導入 )


 A∨¬A 


(¬除去)



(¬導入)仮定1を解消
¬A

(∨導入)
A∨¬A



 


[step7]

  

[仮定]
 ¬(A∨¬A)  

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



(∨導入 )


 A∨¬A 


(¬除去)



(¬導入)仮定1を解消
¬A

(∨導入)
A∨¬A



(¬除去)





[step8]

  

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

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



(∨導入 )


 A∨¬A 


(¬除去)



(¬導入)仮定1を解消
¬A

(∨導入)
A∨¬A



(¬除去)





(背理法)[仮定]2を解消


A∨¬A




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






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