0

I've been trying to prove a Lemma in Coq that like this,

Goal forall (X : Type) (p : X -> Prop), 
(exists x, ~ p x) <-> ~ (forall x, p x).

This is my attempt at it,

Proof.
  intros X p. split.
  - intros [x B] C. apply B. apply C.
  - simpl. intros H.

I got stuck, with this.

1 subgoal
X : Type
p : X -> Prop
H : ~ (forall x : X, p x)
______________________________________(1/1)
exists x : X, ~ p x

And now, my thinking is that maybe i could destruct H in a certain way to progress. Or maybe there's a better way of finishing this? Please help, thanks in advance!

Karlo Kampić
  • 11
  • 4
  • You need classical logic to prove this direction (the law of excluded middle or double negation elimination or any other equivalent formula). – Anton Trunov Apr 29 '21 at 20:49
  • So, I can try asserting a new function that will H into forall x:X, ~px? – Karlo Kampić Apr 29 '21 at 20:53
  • This is related to : https://stackoverflow.com/questions/35518303/is-this-relationship-between-forall-and-exists-provable-in-coq-intuitionistic-lo – Lolo Apr 29 '21 at 21:07
  • @Lolo So does that mean that this is unprovable? – Karlo Kampić Apr 29 '21 at 21:14
  • It is unprovable in the base logic of Coq, however it is not a problem to extend the logic with excluded middle and prove it; but it makes sense the base logic of Coq is more general as to also accomodate worlds that conflict with classical axioms. – ejgallego Apr 30 '21 at 22:50

1 Answers1

0

yep, you need an extra axiom If you do :

Require Import Classical.
Check classic.

now using classic, you can do the proof.

Lolo
  • 604
  • 2
  • 7