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

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


 命題論理関連ページ:命題論理の論理式/命題論理の意味論/命題論理のシンタックス    
 論理関連ページ :  論理記号 
 * 論理目次/総目次/更新履歴 

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



命題論理の形式的体系「自然演繹」における推論規則:「∨導入則」



∨導入則 とは、

 「自然演繹」という《命題論理の形式的体系》において、

  (1) 「 論理式A論理式B」というかたちの論理式へ書き換えてよいのは、

     どのようなかたちの論理式のセットを与えられたときか?  
    
  (2) この書き換えの際に、書き換え前の仮定をどのように引き継げばよいか?

 を明示した《自然演繹の推論規則の下記条項のこと。  




【文献】
 ・前原『記号論理入門』2章§2(pp.41-3):特にp.42 
 ・高崎『数理論理学入門VII.1.
 ・鹿島『数理論理学』図2.2(p.29)
 ・戸次 『数理論理学』定義8.10NMの推論規則(p.181)
 ・戸田山『論理学をつくる』9.2.1(p.223)
 ・野矢『論理学』1-2-3公理系LP(pp.66-7)
 ・野矢『入門!論理学』第5章「標準的な命題論理の体系」(p.146).



  






【∨導入則】

 * 下記 A,B には、どんな論理式を入れてもよい。

 (1)
  ・与えられた論理式Aを、 論理式AB」へ書き換えてよい。

  ・与えられた論理式Bを、論理式AB」へ書き換えてよい。

 (2) 論理式AB」へ書き換えた際に引き継ぐ仮定は、書き換え前の仮定のすべて。

 (例)分配律1-1の証明(step5) / 分配律1-2の証明(step3) 






∨導入則は、下図で表される。





【推論規則:∨導入 

(1)
A

(∨導入)

AB


(2) 
B

(∨導入)

AB


 





  この図は、
    ・演繹図 [高崎VI. 2.1] 
    ・推論図 [前原p.38;高崎VI. 2.1] 
    ・証明図 proof diagram [戸田山『論理学をつくる』8.1.1(p.177);飯田編(p.90);高崎VI. 2.1;向井pp15-16]proof figure[清水『記号論理学』p.97]
    ・導出図 [鹿島『数理論理学』図2.2(p.29)]
  などと呼ばれる。


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

命題論理の形式的体系「自然演繹」:推論規則「∨除去則」


∨除去則 とは、

 「自然演繹」という《命題論理の形式的体系》において、

  (1)・「 論理式A論理式B」を含む論理式のセットを
     「 論理式A論理式B」を含まない論理式に書き換えてよいのは、

      どのようなかたちの論理式のセットを与えられたときか? 

    ・また、
     そのとき、 
     どのようなかたちの論理式へ書き換えてよいのか?
    
  (2) この書き換えの際に、書き換え前の仮定をどのように引き継げばよいか?

 を明示した《自然演繹の推論規則》の下記条項のこと。  




【文献】
 ・前原『記号論理入門』2章§2(pp.41-3):特にp.42
 ・高崎『数理論理学入門VII.1.
 ・鹿島『数理論理学』図2.2(p.29) 
 ・戸次 『数理論理学』定義8.10NMの推論規則(p.181)
 ・戸田山『論理学をつくる』9.2.1(p.223)
 ・野矢『論理学』1-2-3公理系LP(pp.66-7)
 ・野矢『入門!論理学』第5章「標準的な命題論理の体系」(p.146).



  






【∨除去則】

 * 下記 A,B には、どんな論理式を入れてもよい。

 (1)   論理式AB が与えられ、
      仮定Aのもとで論理式C が与えられ、
       仮定Bのもとで論理式C が与えられているとき、
     論理式Cへ書き換えてよい。

 (2)  ただし、
    「 論理式C 」へ書き換えた際に引き継ぐ仮定は、
     書き換え前の仮定のすべてではなく、
     書き換え前の仮定から、仮定A,仮定Bを差し引いた分だけ。

   つまり、
    仮定Xのもとで論理式AB が与えられ、
    仮定Yと仮定Aのもとで論理式C が与えられ、
    仮定Zと仮定Bのもとで論理式C が与えられているとき、

    仮定X,Y,Z,A,Bのもとでの「論理式C」に書き換えるのではなく
    仮定X,Y,Zのもとでの「論理式C」に書き換えられることになる。
 
   この仮定引継手続きは、
    「仮定A,B落ちる」(discharge)[高崎『数理 論理学入門VII.1.]
    「仮定A,B解消される」[鹿島『数理論理学』図2.2(p.29)]
    「仮定A,B打ち消される」(discharge)[戸次 『数理論理学』8.1.2打ち消し操作(p.178)]
    「仮定A,Bキャンセルされる」[戸田山『論理学をつくる』9.1.4(p.219)]
     などと表現される。

 (例)分配律1-1の証明(step6) / 分配律1-2の証明(step6) / 対偶律(2)証明(step08) / 選言的三段論法の証明(step07)   







∨除去則は、下図で表される。





【推論規則:∨除去 

  

AB  

[A]

C
[B]

C



(∨除去)

 
C
 





  この図は、
    ・演繹図 [高崎VI. 2.1] 
    ・推論図 [前原p.38;高崎VI. 2.1] 
    ・証明図 proof diagram [戸田山『論理学をつくる』8.1.1(p.177);飯田編(p.90);高崎VI. 2.1;向井pp15-16]proof figure[清水『記号論理学』p.97]
    ・導出図 [鹿島『数理論理学』図2.2(p.29)]
  などと呼ばれる。

CBであるケースへの応用:
 下記のように、CBであるケースならば、
  

AB  

[A]

B
[B]

B



(∨除去)

 
B
 となるが、
 ここで、[B]…Bを、∨除去の時点で、Bを仮定して、∨除去とともにすぐ仮定Bを解消してもよい。
  (「ただちに落とす」[])
 つまり、
  

AB  

[A]

B


[B]



(∨除去)

 
B
これを、言葉で言い直すと、
 (1)   論理式AB が与えられ、
      仮定Aのもとで論理式B が与えられているとき、
     論理式Bへ書き換えてよい。
 (2)  ただし、
    「 論理式B 」へ書き換えた際に引き継ぐ仮定は、
     書き換え前の仮定のすべてではなく、
     書き換え前の仮定から、仮定A,仮定Bを差し引いた分だけ。
となる。
 *適用例:選言的三段論法の証明(step07)  

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