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

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

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

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




推論規則【矛盾についての規則】・公理【排中律】のもとで【背理法】は派生推論規則

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



　　　　下記のようになっているが、これでほんとにいいの？
　　　　step1が与えられるというのが、へん。

[step1]

　　　　　
 [前提]
¬A
：
⋏

[step2]
　
　　　　　
 [前提]
¬A
：
⋏

(推論規則⋏)
 
 A

[step3]

　　　　　

[前提]
¬A
：
⋏

　[排中律]　 　[前提]　
(推論規則⋏)
 
 A∨¬A A A



[step4]

　　　　　

[前提]
[¬A]1
：
⋏

　[排中律]　 　[前提]　
(推論規則⋏)
 
 A∨¬A [A]1 A

(∨除去則)1

A




【文献】
　・高崎『数理論理学入門』VII. 自然演繹（その１）2.2基本的な恒真式・演繹関係を形式的に確かめること[例6]



　　






　　　　

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





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