命題論理の自然演繹における諸定理 【10】ド・モルガンの法則 の証明(1)

 A,B に、どのような論理式(命題変数単体に限らない)をいれても、
   ( (AB)(AC) )  ( A(BC) )  
 は、【命題論理における自然演繹】の定理

【証明】( ¬(AB) ) ⇒ (¬A)∨(¬B)


 命題論理の形式的体系自然演繹に準拠した操作   
   端的には、
    ・仮定の書き出し 
    ・推論規則「∧導入則」による書き換え 
    ・推論規則「∨導入則」による書き換え
    ・推論規則「∨除去則」による書き換え   
    ・推論規則「¬導入則」による書き換え 
    ・推論規則「¬除去則」による書き換え
    ・推論規則「¬¬除去則」による書き換え   
    ・推論規則「⇒導入則」による書き換え 
 のみで、
 論理式「( ¬(AB) ) (¬A)(¬B)」が得られる  
 ことを示す。[前原p.184]

 → step01 / step02 / step03 / step04 / step05
 → step06 / step07 / step08 / step09 / step10
 → step11 / step12 / step13 / step14 / step15



[step1]自然演繹で認められた操作(2)仮定の書き出し
論理式A」を仮定1として書き出す。
論理式B」を仮定2として書き出す。
  
 仮定1 
  A   
仮定2
  B  



[step2]自然演繹で認められた操作(3)推論規則による書き換え
  ・推論規則「∧導入則」にしたがって、
    仮定1「A」 仮定2「B
   を
    「AB
   へ書き換える。

  ・推論規則「∧導入則」の規定により、
     書き換え後に引き継がれる仮定は、書き換え前の仮定のすべてとなるから、
      書き換え後の「AB」は、仮定1「A」 仮定2「B」 のもとにある。

  ・これで、推論規則「∧導入則」による書き換えで、
   ・仮定1「A
   ・仮定2「B
   から、
   「仮定1『A』仮定2『A』のもとで『AB』」
   が、導出されたことになる。
  
 仮定1 
   A    
仮定2
  B  



(∧導入) 


AB





【文献】
 ・野矢『論理学』1-2-3-LP-命題論理の諸定理-定理9(1-a)(1-b)(2-a)(2-b)(p.70);付録-定理9(1-a)(1-b)(2-a)(2-b)(pp.218-9):二項目とも両方向。
 ・戸田山『論理学をつくる』練習問題69(p.230);9.3.1-9.3.2(pp.233-5)練習問題71(1)(p.235):
 ・前原『記号論理入門』6章§1問(pp.107-8)( ¬(AB) ) (¬A)(¬B) ;解答(p.184)( ¬(AB) ) (¬A)(¬B)
 ・van Dalen,Logic and Structure(3rd ed.) 1.6(p.52)
 ・高崎金久『数理論理学入門VII.2.2基本的な恒真式・演繹関係を形式的に確かめること[例4][例5];3.1排中律に依存する定理と依存しない定理


 
   


[step3]
  
 仮定1 
   A    
仮定2
  B  




∧導入  

 仮定3 

AB

¬(AB)




[step4]
  
 仮定1 
  A   
仮定2
  B  





∧導入  

 仮定3 


AB

¬(AB)




¬除去  



[step5]
  
 [仮定1] 
  [A]   
仮定2
  B  





∧導入  

 仮定3 


AB

¬(AB)




¬除去 





¬導入 仮定1を解消

¬A


[step6]
  
 [仮定1] 
  [A]   
仮定2
  B  





∧導入  

 仮定3 


AB

¬(AB)




¬除去 





¬導入 仮定1を解消

¬A


∨導入則


(¬A)(¬B)

[step7]
  
 [仮定1] 
  [A]   
仮定2
  B  






∧導入  

 仮定3 



AB

¬(AB)





¬除去 







¬導入 仮定1を解消

¬A



∨導入則

仮定4


(¬A)(¬B)

¬((¬A)(¬B))




[step8]
  
 [仮定1] 
  [A]   
仮定2
  B  







∧導入  

 仮定3 




AB

¬(AB)






¬除去 









¬導入 仮定1を解消


¬A




∨導入則

仮定4



(¬A)(¬B)

¬((¬A)(¬B))




¬除去 





[step9]
  

 [仮定1] 

  [A]   

[仮定2]

  [B]  








∧導入  

 仮定3 




AB

¬(AB)






¬除去 









¬導入 仮定1を解消




¬A




∨導入則

仮定4



(¬A)(¬B)

¬((¬A)(¬B))




¬除去 





¬導入 仮定2を解消


¬B

 → ド・モルガン則
 → 自然演繹の定理一覧
 → 論理記号一覧 
 → 総目次  


  

[step10]
  

 [仮定1] 

  [A]   

[仮定2]

  [B]  








∧導入  

 仮定3 




AB

¬(AB)






¬除去 









¬導入 仮定1を解消




¬A




∨導入則

仮定4



(¬A)(¬B)

¬((¬A)(¬B))




¬除去 





¬導入 仮定2を解消


¬B


∨導入則


(¬A)(¬B)

[step11]
  

 [仮定1] 

  [A]   

[仮定2]

  [B]  









∧導入  

 仮定3 





AB

¬(AB)







¬除去 











¬導入 仮定1を解消





¬A





∨導入則

仮定4




(¬A)(¬B)

¬((¬A)(¬B))





¬除去 







¬導入 仮定2を解消



¬B



∨導入則

仮定4


(¬A)(¬B)

¬((¬A)(¬B))





[step12]
  

 [仮定1] 

  [A]   

[仮定2]

  [B]  










∧導入  

 仮定3 






AB

¬(AB)








¬除去 













¬導入 仮定1を解消






¬A






∨導入則

仮定4





(¬A)(¬B)

¬((¬A)(¬B))






¬除去 









¬導入 仮定2を解消




¬B




∨導入則

仮定4



(¬A)(¬B)

¬((¬A)(¬B))




¬除去





[step13]
  

 [仮定1] 

  [A]   

[仮定2]

  [B]  










∧導入 

 仮定3 






AB

¬(AB)








¬除去 













¬導入 仮定1を解消






¬A






∨導入則

[仮定4]





(¬A)(¬B)

[¬((¬A)(¬B))]






¬除去 









¬導入 仮定2を解消




¬B




∨導入則

[仮定4]



(¬A)(¬B)

[¬((¬A)(¬B))]




¬除去





¬導入 仮定4を解消


¬¬((¬A)(¬B))

 → ド・モルガン則
 → 自然演繹の定理一覧
 → 論理記号一覧 
 → 総目次  


  
[step14]
  

 [仮定1] 

  [A]   

[仮定2]

  [B]  










∧導入 

 仮定3 






AB

¬(AB)








¬除去 













¬導入 仮定1を解消






¬A






∨導入則

[仮定4]





(¬A)(¬B)

[¬((¬A)(¬B))]






¬除去 









¬導入 仮定2を解消




¬B




∨導入則

[仮定4]



(¬A)(¬B)

[¬((¬A)(¬B))]




¬除去





¬導入 仮定4を解消


¬¬((¬A)(¬B))


¬¬除去則

(¬A)(¬B)


[step15]
  

 [仮定1] 

  [A]   

[仮定2]

  [B]  










∧導入 

 仮定3 






AB

¬(AB)








¬除去 













¬導入 仮定1を解消






¬A






∨導入則

[仮定4]





(¬A)(¬B)

[¬((¬A)(¬B))]






¬除去 









¬導入 仮定2を解消




¬B




∨導入則

[仮定4]



(¬A)(¬B)

[¬((¬A)(¬B))]




¬除去





¬導入 仮定4を解消


¬¬((¬A)(¬B))


¬¬除去則

(¬A)(¬B)


(⇒導入則)仮定3を解消


¬(AB) ) (¬A)(¬B)


 → ド・モルガン則
 → 自然演繹の定理一覧
 → 論理記号一覧 
 → 総目次