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.forall P : Prop, ~ P \/ P -> False

My approach is:

Proof.forall P : Prop, ~ P \/ P -> False
  intros P H.P: Prop
H: ~ P \/ P
False unfold not in H.P: Prop
H: (P -> False) \/ P
False intuition.P: Prop
H0: P -> False
False
P: Prop
H0: P
False

The system says following:

2 subgoals

  P : Prop
  H0 : P -> False
  ============================
  False

subgoal 2 is:
 False

How should I proceed? Thanks

A: This question is strongly related, but I think it's nevertheless different from the current one.

A: If you had a metatheory, you could prove that no Coq program proves the law of the excluded middle. This would be closest to what you are trying to prove.

Answer (Anton Trunov)

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).P: Prop
~ ~ (P \/ ~ P)
Proof.P: Prop
~ ~ (P \/ ~ P)
  intros nlem.P: Prop
nlem: ~ (P \/ ~ P)
False apply nlem.P: Prop
nlem: ~ (P \/ ~ P)
P \/ ~ P
  right.P: Prop
nlem: ~ (P \/ ~ P)
~ P intros p.P: Prop
nlem: ~ (P \/ ~ P)
p: P
False apply nlem.P: Prop
nlem: ~ (P \/ ~ P)
p: P
P \/ ~ P
  left.P: Prop
nlem: ~ (P \/ ~ P)
p: P
P exact p.
Qed.

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

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

Answer (ejgallego)

What you are trying to construct is not the negation of LEM, which would say "there exists some P such that EM doesn't hold", but the claim that says that no proposition is decidable, which of course leads to a trivial inconsistency:

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

Goal False.False
  now apply (not_lem True); left.

No need to use the fancy double-negation lemma; as this is obviously inconsistent [imagine it would hold!]

The "classical" negation of LEM is indeed:

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

and it is not provable [otherwise EM wouldn't be admissible], but you can assume it safely; however it won't be of much utility for you.

Answer (Ember Edison)

I'm coming from mathoverflow, but I don't have permission to comment on @Anton Trunov's answer. I think his answer is unjust, or at least incomplete: he hides the following "folklore":

Coq + Impredicative Set + Weak Excluded-middle -> False

This folklore is a variation of the following facts:

proof irrelevance + large elimination -> false
Coq + Impredicative Set is canonical, soundness, strong normalization, so it is consistent.

Coq + Impredicative Set is the old version of Coq. I think this at least shows that the defense of the LEM based on double negative translation is not that convincing.

If you want to get information about the solutions, you can get it from here https://github.com/FStarLang/FStar/issues/360

On the other hand, you may be interested in the story of how Coq-HoTT+UA went against LEM∞...

Ok, let's have some solutions.

use command-line flag -impredicative-set, or the install old version (<8.0) of coq.
excluded-middle -> proof-irrelevance
proof-irrelevance -> False

Or you can work with standard coq + coq-hott.

install coq-hott
Univalence + Global Excluded-middle (LEM∞) -> False

It is not recommended that you directly click on the code in question without grasping the specific concept.

I skipped a lot about meta-theoretic implementations, such as Univalence not being computable in Coq-HoTT but only in Agda-CuTT, such as the consistency proof for Coq+Impredicative Set/Coq-HoTT.

However, metatheoretical considerations are important. If we just want to get an Anti-LEM model and don't care about metatheory, then we can use "Boolean-valued forcing" in coq to wreak havoc on things that only LEM can introduce, such as "every function about real set is continuous", Dedekind infinite...

But this answer ends there.