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

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

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

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



推論規則【二重否定除去律】のもとで、【背理法】【排中律】【矛盾に関する規則】は派生推論規則

【命題論理における自然演繹の必要最小限のセット：type2】
　　　⇒導入則・⇒除去則・∧導入則・∧除去則・∨導入則・∨ 除去則・¬導入則・¬除去則　
　　　¬¬除去則
　において、

　　・背理法　
　　・矛盾に関する規則　
　　・排中律　

　は、派生推論規則・定理になる。
　　
【どうして？】
　→　∨導入則・¬導入則・¬除去則・¬¬除去則のみを用いた【排中律】の導出。
　→　∨導入則・¬導入則・¬除去則・¬¬除去則のみを用いた【矛盾に関する規則】の導出。
　→　∨導入則・¬導入則・¬除去則・¬¬除去則のみを用いた【背理法】の導出。




【文献】
　・前原『記号論理入門』§8　
　　　　　　・「二重否定の除去というものは、排中律と矛盾の公理の双方を合わせたものと同等ということになります」(p.59)
　　　　　　　　　　　・排中律を公理とせず、二重否定除去を推論規則とした【type2】において、排中律の証明(p.58)
　　　　　　　　　　　・排中律を公理とせず、二重否定除去を推論規則とした【type2】において、矛盾の公理の証明(pp.58-9)



　　



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