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

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

・命題論理の公理系の諸タイプ ： ヒルベルト流の公理系/ゲンツェン流の公理系（自然演繹）
　※命題論理関連ページ：命題論理の論理式 /命題論理の意味論[真理値/真理関数/真理値表/論理式の真理値の決定原理/真理値分析/恒真式・恒偽式 ] 　　
　※論理関連ページ ：  論理記号　
　*　論理目次/総目次/更新履歴　

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


推論規則【背理法】のもとで【二重否定除去律】は派生推論規則

【命題論理における自然演繹の必要最小限のセット： type1】
　　　⇒導入則・⇒除去則　
　　　∧導入則・∧除去則・∨導入則・∨ 除去則　
　　　¬導入則・¬除去則　
　　　背理法　　　　　
　において、
　¬¬除去則は派生推論規則になる。
　　
【どうして？】

【命題論理における自然演繹の必要最小限のセット：type1】に準拠した操作
　端的には、
　　・仮定の書き出し　
　　・推論規則「¬除去則」による書き換え　
　　・推論規則「背理法」による書き換え　
　のみで、

　　　
 ¬¬A

　　¬¬除去則　



A

　が得 られるから。　

[step1] 自然演繹で認められた操作(2)仮定の書き出し

　・論理式「¬A」 を仮定1として書き出す。
　・論理式「¬(¬A)」 を仮定2として書き出す。

　　
 　仮定1　
　¬A　　

　仮定2　
　¬(¬A)　

　　

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

　　・推論規則「¬除去則」にしたがって、
　　　　仮定1「¬A」
　　　　仮定2「¬(¬A)」
　　　を、「⋏(矛盾)」へ書き換える。
　　・推論規則「¬除去則」の規定により、
　　　書き換え後に引き継がれる仮定は、書き換え前の仮定のすべてだから、
　　　 書き換え後の「⋏(矛盾)」は、仮定1「¬A」仮定2「¬(¬A)」のもとにある。

　　・これで、推論規則「¬除去則」による書き換えに よって、
　　　　仮定1「¬A」
　　　　仮定2「¬(¬A)」
　　　から、
　　　　「仮定1『¬A』仮定2『¬(¬A)』のもとで『⋏(矛盾)』」
　　　が導出されたことになる。

　　
 　仮定1　
　¬A　　

　仮定2　
¬(¬A)

(¬除去)

⋏

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

・推論規則「背理法」にしたがって、
　　　　「仮定1『¬A』仮定2『¬(¬A)』のもとで『⋏(矛盾)』」
　を、「A」へ書き換える。
・推論規則「背理法」の規定によって、
　書き換え後に引き継がれる仮定は、
　　　書き換え前の仮定『¬A』仮定2『¬(¬A)』から、
　　　仮定『¬A』を差し引いた分だけ
　だから、
　書き換え後の「A」は、仮定2「¬(¬A)」のみのもとにある。

・これで、推論規則「背理法」による書き換えに よって、
　　「仮定1『¬A』仮定2『¬(¬A)』のもとで『⋏(矛盾)』」
　から、
　　「仮定2『¬(¬A)』のもとで『A』」
　が導出されたことになる。

　
　　

　[仮定1]　
　[ ¬A ]　

　仮定2　
　¬(¬A)　

(¬除去 )

⋏

(背理法)仮定1を解消　

A


・推論規則としての二重否定除去律
　　　　「¬(¬A)」を
　　　　「仮定『¬(¬A)』のもとで『A』」に書き換えてよい
　　　
 ¬¬A

　



A
　は以上で得られた。

　定理となる論理式を獲得したいときは、次のステップへ。




【文献】
　・van Dalen,Logic and Structure(3rd ed.) Theorem1.4.4(4)(pp.32-3)　:¬¬除去。背理法を用いて。　



　　






　　　　


→　命題論理の自然演繹　：トピック一覧　
→　命題論理のシンタックス　：トピック一覧
→　総目次　　
　　
  　
[step4]自然演繹で認められた操作(3)推論規則による書き換え

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


　　

　[仮定1]　
　[ ¬A ]　

　[仮定2]　
[¬¬A]

(¬除去 )

⋏

(背理法)仮定1を解消　

A

(⇒導入)仮定2を解消

¬¬A⇒A

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