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

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

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



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

・¬導入則　とは、

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

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

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

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




【文献】
　・前原『記号論理入門』2章§4(pp.45-6):特にp.45;
　・高崎『数理論理学入門』VII.1.
　・鹿島『数理論理学』図2.2(p.29)
　・戸次 『数理論理学』定義8.8(p.180)
　・戸田山『論理学をつくる』9.2.1(p.227);9.3.2矛盾記号の導入(p.235)

　・野矢『入門！論理学』第5章「標準的な命題論理の体系」(p.146)..






【¬導入則】

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

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

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

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

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






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



【推論規則：¬導入】　

　　　
 [A]
：
⋏

(¬導入)
 
 ¬A
　




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

*　どうして？→　《¬の定義》と《¬導入則の起源》　　
*　使用例　→ 矛盾律の証明 (step04)/二重否定律の証明(step03)/対偶律の証明1(step06)/　




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

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

・¬除去則　とは、

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

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

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

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

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




【文献】
　・前原『記号論理入門』2章§4(pp.45-6):特にp.45;
　・高崎『数理論理学入門』VII.1.
　・鹿島『数理論理学』図2.2(p.29)
　・戸田山『論理学をつくる』9.3.2矛盾記号の導入(p.235).

　　






【¬除去則】

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

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

　(2)　書き換え後に引き継ぐ仮定は、書き換え前の仮定のすべて。




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



【推論規則：¬除去】　

　　　
   A ¬A　

(¬除去)
 
 ⋏
　




　　この図は、
　　　　・演繹図　[高崎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)/対偶律の証明1(step04)/選言的三段論法の証明(step04)/ /　


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

¬の定義。¬導入則・¬除去則の起源。　
【定義】　

・「自然演繹」という《命題論理の形式的体系》において、
　　論理式「¬A」は、論理式「A⇒⋏」の略記として、定義される。


【¬導入則について】　　

・上記定義より、
　「¬A」とは「A⇒⋏」の略記に過ぎないのだから、
　「¬A」への書き換え(¬導入)とは、実質的には、「A⇒⋏」への書き換え(⇒導入)に他ならない。

・したがって、
　　¬導入則とは、実質上、　
　　⇒導入則　　
 [A]
：
B
　

(⇒-導入)

A⇒B

　　において、
　　Bを「⋏」に指定した
　　　　　　　　
 [A]
：
⋏

(⇒-導入)

A⇒⋏
　　に他ならず、
　　このなかの「A⇒⋏」を上記定義にしたがって「¬A」と略記したのが、
　　¬導入則になる。




【文献：《¬導入則》＋《¬除去則》は《¬の定義》と同じと指摘】
　・前原『記号論理入門』§7(p.53)
【文献：《¬の定義》を採用し、《¬導入則》＋《¬除去則》をつかわないテキスト】
　・戸次 『数理論理学』定義8.19NKの推論規則(p.187)
　・van Dalen,Logic and Structure(3rd ed.) 1.4Natural Deduction(pp.29-39)



　　

【¬除去則について】　　

・上記定義より、
　「¬A」とは「A⇒⋏」の略記に過ぎないのだから、
　「¬A」からの書き換え(¬除去)とは、実質的には、「A⇒⋏」からの書き換え(¬除去)に他ならない。

・したがって、
　　¬除去則とは、実質上、　
　　　⇒除去則　　
 A　A⇒B

(⇒-除去)

B
　　において、
　　Bを「⋏」に指定した
　　　⇒除去則　　
 A　A⇒⋏

(⇒-除去)

⋏
　　に他ならず、
　　このなかの「A⇒⋏」を上記定義にしたがって「¬A」と略記したのが、
　　¬除去則になる。