Can you prove Excluded Middle is wrong in Coq if I do not import classical logic

Question

I know excluded middle is impossible in the logic of construction. However, I am stuck when I try to show it in Coq.

Theorem em: forall P : Prop, ~P \/ P -> False.

My approach is:

intros P H.
unfold not in H.
intuition.

The system says following:

2 subgoals
P : Prop
H0 : P -> False
______________________________________(1/2)
False
______________________________________(2/2)
False

How should I proceed? Thanks

Answer 1

One cannot refute the law of excluded middle (LEM) in Coq. Let's suppose you proved your refutation of LEM. We model this kind of situation by postulating it as an axiom:

Axiom not_lem : forall (P : Prop), ~ (P \/ ~ P).

But then we also have a weaker version (double-negated) of LEM:

Lemma not_not_lem (P : Prop) :
  ~ ~ (P \/ ~ P).
Proof.
  intros nlem. apply nlem.
  right. intros p. apply nlem.
  left. exact p.
Qed.

These two facts together would make Coq's logic inconsistent:

Lemma Coq_would_be_inconsistent :
  False.
Proof.
  apply (not_not_lem True).
  apply not_lem.
Qed.