命題論理の自然演繹における諸定理 【8】分配律1-2 の証明

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


【証明1-2】( (AB)∨(AC) ) ⇒ ( A∧(BC) )

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


 →step01
 →step02
 →step03
 →step04
 →step05
 →step06
 →step07


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

 仮定1 
AB





  
 仮定2 
AC 










【文献】
 ・前原『記号論理入門』7章§1.4(pp.121-2):( A(BC) )( (AB)(AC) )
 ・野矢『論理学』1-2-3-LP-命題論理の諸定理-定理12(1-a)(1-b)(2-a)(2-b)(p.70);付録-定理12(1-a)(1-b)(2-a)(2-b)(pp.220-22):二項目とも両方向。
 ・van Dalen,Logic and Structure(3rd ed.) 1.6(pp.50-51)
 ・林『数理論理学』例1.10(p.32)


 
   

[step2] 自然演繹で認められた操作(3)推論規則による書き換え
  ・推論規則「∧除去則」にしたがって、
    仮定1「AB」を「A」 へ 
    仮定1「AB」を「B」 へ
   書き換える。
  ・推論規則「∧除去則」により、
   書き換え後に引き継がれる仮定は、書き換え前の仮定のすべてとなるから、
    書き換え後の「A」「B」は、それぞれ、仮定1「AB」 のもとにある。
  ・これで、推論規則「∧除去則」による書き換えによって、
   仮定1「AB」から、
   「仮定1『AB』のもとで『A』」
   「仮定1『AB』のもとで『B』」
   が導出されたことになる。

  
  

 仮定1 
AB




(∧除去)


A

  

 仮定1 
AB




(∧除去)


B

  

 仮定2 
AC





  ・推論規則「∧除去則」にしたがって、
    仮定2「AC」を「A」 へ 
    仮定2「AC」を「C」 へ
   書き換える。
  ・推論規則「∧除去則」により、
   書き換え後に引き継がれる仮定は、書き換え前の仮定のすべてとなるから、
    書き換え後の「A」「C」は、それぞれ、仮定2「AC」 のもとにある。
  ・これで、推論規則「∧除去則」による書き換えによって、
   仮定2「AC」から、
   「仮定2『AC』のもとで『A』」
   「仮定2『AC』のもとで『C』」
   が導出されたことになる。

  
  

 仮定1 
AB




(∧除去)


A

  

 仮定1 
AB




(∧除去)


B

  

 仮定2 
AC




(∧除去)


A

  

 仮定2 
AC




(∧除去)


C



[step3] 自然演繹で認められた操作(3)推論規則による書き換え

  ・推論規則「∨導入則」にしたがって、
   「仮定1『AB』のもとで『B』」を
   「BC」へ書き換える。

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

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

  
  

 仮定1 
AB




(∧除去)


A

  

 仮定1 
AB




(∧除去)


B



(∨導入)


BC


  

 仮定2 
AC




(∧除去)


A

  

 仮定2 
AC




(∧除去)


C







  ・推論規則「∨導入則」にしたがって、
   「仮定2『AC』のもとで『C』」を
   「BC」へ書き換える。

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

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

  
  

 仮定1 
AB




(∧除去)


A

  

 仮定1 
AB




(∧除去)


B



(∨導入)


BC


  

 仮定2 
AC




(∧除去)


A

  

 仮定2 
AC




(∧除去)


C



(∨導入)


BC




 → 自然演繹における分配律1-2証明冒頭
 → 自然演繹の定理:分配律
 → 自然演繹の定理:トピック一覧
 → 論理記号:トピック一覧 
 → 総目次  


  
[step4] 自然演繹で認められた操作(3)推論規則による書き換え

  ・推論規則「∧導入則」にしたがって、
    「仮定1『AB』のもとで『A』」 「仮定1『AB』のもとで『BC』」
   を
    「A(BC)」
   へ書き換える。

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

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

  
  

 仮定1 
AB




(∧除去)


A

  

 仮定1 
AB




(∧除去)


B



(∨導入)


BC



 仮定2 
AC



(∧除去)

A

  

 仮定2 
AC




(∧除去)


C



(∨導入)


BC





(∧導入)  


(∧導入) 


A∧(BC)




  ・推論規則「∧導入則」にしたがって、
    「仮定2『AC』のもとで『A』」 「仮定2『AC』のもとで『BC』」
   を
    「A(BC)」
   へ書き換える。

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

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

  
  

 仮定1 
AB




(∧除去)


A

  

 仮定1 
AB




(∧除去)


B



(∨導入)


BC



 仮定2 
AC



(∧除去)

A

  

 仮定2 
AC




(∧除去)


C



(∨導入)


BC





(∧導入) 


(∧導入)  


A∧(BC)


A∧(BC)



[step5] 自然演繹で認められた操作(2)仮定の書き出し
論理式「(AB)(AC)」を仮定3として書き出す。
  

  

 仮定1 
AB




(∧除去)


A

  

 仮定1 
AB




(∧除去)


B



(∨導入)


BC



 仮定2 
AC



(∧除去)

A

  

 仮定2 
AC




(∧除去)


C



(∨導入)


BC




仮定3


(∧導入) 


(∧導入) 


 (AB)∨(AC)  

A(BC)
A(BC)



 → 自然演繹における分配律1-2証明冒頭
 → 自然演繹の定理:分配律
 → 自然演繹の定理:トピック一覧
 → 論理記号:トピック一覧 
 → 総目次  


  

[step6]自然演繹で認められた操作(3)推論規則による書き換え

  ・推論規則「∨除去則」にしたがって、
   仮定3「(AB)(AC)」
   「仮定1『AB』のもとで『A(BC)』」
   「仮定2『AC』のもとで『A(BC)』」
   を
   「A(BC)」
   へ書き換える。

  ・推論規則「∨除去則」の規定により、
     《書き換え後に引き継がれる仮定》は、
       《「書き換え前の仮定」から仮定1『AB,仮定2『ACを差し引いた分》だけ
     となるから、
      書き換え後の「A(BC)」 は、仮定3「(AB)(AC)」だけ のもとにある。

  ・これで、推論規則「∨除去則」による書き換えで、
    ・仮定3「(AB)(AC)」
    ・「仮定1『AB』のもとで『A(BC)』」
    ・「仮定2『AC』のもとで『A(BC)』」
   から、
   「仮定3『(AB)(AC)』のもとで『A(BC)』」
   が、導出されたことになる。

  

  

 [仮定1] 
[AB]




(∧除去)


A

  

 [仮定1] 
[AB]




(∧除去)


B



(∨導入)


BC



 [仮定2] 
[AC]



(∧除去)

A

  

 [仮定2] 
[AC]




(∧除去)


C



(∨導入)


BC




仮定3


(∧導入) 


(∧導入) 


 (AB)(AC)  

A(BC)
A(BC)


(∨除去) 仮定1仮定2を解消


A(BC)


 ここまでで、派生推論規則
       

 (AB)(AC) 




A(BC)
 は示されたことになる。次のステップで、定理になる。

[step7]  自然演繹で認められた操作(3)推論規則による書き換え

推論規則「⇒導入則」にしたがって、
  「仮定3『(AB)(AC)』のもとで『A(BC)』」を
  「(AB)(AC) ( A(BC) )」へ書き換える。
推論規則「⇒導入則」の規定にしたがうと、
   「(AB)(AC) ( A(BC) )」への書き換え後に引き継がれる仮定は、
   書き換え前の仮定「(AB)(AC)」から、仮定「(AB)(AC)」 を差し引いた分だけとなるから、   
   「(AB)(AC) ( A(BC) )」への書き換え後に仮定はすべて差し引かれてなくなって しまい、
    仮定なしの「(AB)(AC) ( A(BC) )」が得られる。
・これで、推論規則「⇒導入則」による書き換えで、
  「仮定3『(AB)(AC)』のもとで『A(BC)』」から、
  仮定なしの「(AB)(AC) ( A(BC) )」が導出されたことになる。

  

  

 [仮定1] 
[AB]




(∧除去)


A

  

 [仮定1] 
[AB]




(∧除去)


B



(∨導入)


BC



 [仮定2] 
[AC]



(∧除去)

A

  

 [仮定2] 
[AC]




(∧除去)


C



(∨導入)


BC




[仮定3]


(∧導入) 


(∧導入) 


 (AB)∨(AC)  

A(BC)
A(BC)


(∨除去) 仮定1仮定2を解消


A(BC)




(⇒導入)仮定3を解消


( (AB)∨(AC) ) ⇒ ( A∧(BC) )




 → 自然演繹における分配律1-2証明冒頭
 → 自然演繹の定理:分配律
 → 自然演繹の定理:トピック一覧
 → 論理記号:トピック一覧 
 → 総目次