2018-05-13から1日間の記事一覧
述語論理で、ドモルガンに相当すんのが以下の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つ ¬(∃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…