命題論理の「自然演繹」の推論規則 : トピック一覧・命題論理の自然演繹:推論規則公理一覧・推論規則:⇒導入則・⇒除去則・∧導入則・∧除去則・∨導入則・∨除去則・¬導入則・¬除去則(¬の定義) 背理法・二重否定除去律・矛盾除去 ・公理 :排中律 ・命題論理の公理系の諸タイプ : ヒルベルト流の公理系/ゲンツェン流の公理系(自然演繹) ※命題論理関連ページ:命題論理の論理式 /命題論理の意味論[真理値/真理関数/真理値表/論理式の真理値の決定原理/真理値分析/恒真式・恒偽式 ] ※論理関連ページ : 論理記号 * 論理目次/総目次/更新履歴 ※述語論理の場合は、林晋,鹿島亮を参照。 |
推論規則【二重否定除去律】のもとで【排中律】は定理 |
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
【命題論理における自然演繹の必要最小限のセット:type2】 ⇒導入則・⇒除去則・∧導入則・∧除去則・∨導入則・∨ 除去則・¬導入則・¬除去則 ¬¬除去則 において、 ・排中律 が定理として成り立つ。 【どうして?】 ・∨導入則・¬導入則・¬除去則・¬¬除去則のみを用いた排中律 の導出。 [前原『記号論理入門』§8(p.58)] [step1]
(⇒導入則をつかうと、A⇒A∨¬A [無前提]となるが、まだ変形するので、そうしない) [step2]
[step3]
¬(A∨¬A)という前提の下で、¬A [step4]
|
|
|
仮定2 ¬(A∨¬A) |
||||||||||||||||||||||||||||
|
(¬除去 ) |
||||||||||||||||||||||||||||
⋏ |
|
|||||||||||||||||||||||||||||||||||||
|
( ¬導入)仮定2を解消 |
||||||||||||||||||||||||||||||||||||
¬¬(A∨¬A) |
|
|||||||||||||||||||||||||||||||||||||
|
( ¬導入)仮定2を解消 |
||||||||||||||||||||||||||||||||||||
¬¬(A∨¬A) | |||||||||||||||||||||||||||||||||||||
|
(¬¬除去則) |
||||||||||||||||||||||||||||||||||||
A∨¬A |
→ 命題論理の自然演繹 :トピック一覧 → 命題論理のシンタックス :トピック一覧 → 総目次 |
|
→ 命題論理の自然演繹 :トピック一覧 → 命題論理のシンタックス :トピック一覧 → 総目次 |