Logic: excluded_middle_irrefutable

Here is the task from the book:

Proving the consistency of Coq with the general excluded middle axiom requires complicated reasoning that cannot be carried out within Coq itself. However, the following theorem implies that it is always safe to assume a decidability axiom (i.e., an instance of excluded middle) for any particular Prop [P]. Why? Because we cannot prove the negation of such an axiom. If we could, we would have both [~ (P / ~P)] and [~ ~ (P / ~P)] (since [P] implies [~ ~ P], by the exercise below), which would be a contradiction. But since we can't, it is safe to add [P / ~P] as an axiom.

As far as I understand the task, I must introduce excluded middle Axiom. But I am not sure that I did it correctly:

Axiom decidability : forall (P:Prop),
    (P \/ ~ P) = True.

(* Theorem double_neg : ∀P : Prop,
       P → ~~P. *)

Theorem excluded_middle_irrefutable: forall (P:Prop),
  ~ ~ (P \/ ~ P).
Proof.
  intros P. apply double_neg.

Now we got (P \/ ~ P), but when I try apply decidability., it gives an error:

Unable to unify "(?M1052 \/ ~ ?M1052) = True" with "P \/ ~ P".

What to do?

Solution

The exercise is asking you to prove excluded_middle_irrefutable without assuming any axioms.