补对合的协q证明

Question

如何证明集合的补是对合的？

  Require Import Ensembles. Arguments In {_}. Arguments Complement {_}.

  Variables (T:Type) (A:Ensemble T).
  Axiom set_eq: forall (E1 E2:Ensemble T), (forall x, E1 x <-> E2 x) -> E1 = E2.

  Lemma complement_involutive: 
      forall x, In (Complement (Complement A)) x -> In A x.

编辑:假设decidable (In A x)使firstorder能够完全证明引理。

Answer 1

complement_involutive正是~ ~ A x -> A x，众所周知，它等价于排除的中间，在Type中是如此，因此在Coq中是不可证明的，而不假设它是公理。见这个答案https://math.stackexchange.com/questions/1370805/why-cant-you-prove-the-law-of-the-excluded-middle-in-intuitionistic-logic-for