逻辑:排除中间不可辩驳

这是本书的任务:

证明coq与一般排除中间公理的一致性 需要复杂的推理,不能在质量成本内进行。 本身。然而,下面的定理意味着它总是安全的 假设一个可判定公理(即排除中间的一个实例) 对于任何 特别 道具[P]。为什么?因为我们不能证明 否定这样一个公理。如果可以的话,我们两个都有/ ~p)和[~~(p/~p)](因为[p]通过练习暗示了[~~p]。 这是一个矛盾。但既然我们不能,那就是 作为一个公理添加[p/~p]是安全的。

就我所理解的任务而言,我必须引入被排除的中间公理。 但我不确定我做得是否正确:

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.

现在我们有了 (P \/ ~ P) 但是当我尝试的时候 apply decidability. ,它给出一个错误:

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

怎么办?