述語論理で、ドモルガンに相当すんのが以下の4つ ¬(∃x,P x) -> ∀x,¬ P x ∀x,¬ P x -> ¬(∃x,P x) ∃x, ¬ P x -> ¬(∀x,P x) ¬(∀x,P x) -> ∃x, ¬ P x 例によって最後のやつが排中律or二重否定則とかないと証明出来ないらしい。 Require Import Coq.Logic.Classic…

命題論理ドモルガン4兄弟 ¬(A ∨ B) → ¬A ∧ ¬B. ¬A ∧ ¬B → ¬(A ∨ B). ¬A ∨ ¬B → ¬(A ∧ B). ¬(A ∧ B) → ¬A ∨ ¬B.のうち、直観主義論理の範囲で証明出来ないらしい ¬(A ∧ B) → ¬A ∨ ¬B.の証明。 排中律を前提とする。排中律を使って、A∨¬AとB∨¬Bをコンテキスト…