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

・命題論理の自然演繹：推論規則公理一覧　
　・推論規則：⇒導入則・⇒除去則・∧導入則・∧除去則・∨導入則・∨除去則・¬導入則・¬除去則・背理法・二重否定除去律・矛盾除去
　・公理　　：排中律　
　※命題論理関連ページ：命題論理の論理式/命題論理の意味論/命題論理のシンタックス　 　　
　※論理関連ページ ：  論理記号　
　*　論理目次/総目次/更新履歴　

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



命題論理の形式的体系「自然演繹」：推論規則「⇒導入則」


・⇒導入則　とは、

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

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

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

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




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

　　






【⇒導入則】

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

　(1)　仮定Aのもとで与えられた論理式Bを、
　　　　「　論理式A⇒論理式B　」
　　　　へ書き換えてよい。

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

　　　つまり、
　　　　仮定Xと仮定Aのもとで与えられた論理式Bは、
　　　　仮定Xと仮定Aのもとでの「論理式A⇒論理式B」ではなく
　　　　仮定Xのもとでの「論理式A⇒論理式B」に書き換えられることになる。

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

　（例）二重否定除去律の証明(step03)/二重否定導入律の証明(step04)
　　　　冪等律1-1の証明step03/冪等律1-2の証明step03/分配律1-1の証明step07/　　




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



【推論規則：⇒導入】　

　　　
 [A]
：
B

(⇒-導入)

A⇒B
　




　　この図は、
　　　　・演繹図　[高崎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)]
　　などと呼ばれる。

*　使用例　→ 二重否定除去律の証明(step03)/二重否定導入律の証明(step04)/冪等律1-1の証明step03/冪等律1-2の証明step03  　　 　


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

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

・⇒除去則　とは、

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

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

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

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

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




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

　　






【⇒除去則】

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

　(1)　与えられた二つの論理式「論理式A」「論理式A⇒論理式B」を、
　　　　「論理式B」へ書き換えてよい。　

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




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



【推論規則：⇒除去】　

　　　　
  A　A⇒B 

(⇒-除去)
 
 B
　




　　この図は、
　　　　・演繹図　[高崎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)step02 / 対偶律の証明(2)(step02) / 推移律の証明(step04) / 推移律の証明(step05)  /  前件肯定式の証明　



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