coq - 逻辑：excluded_middle_irrefutable

Question

这是书中的任务：

证明 Coq 与一般排中公理的一致性需要复杂的推理，而 Coq 本身无法进行。然而，下面的定理暗示对于任何特定的Prop [P] ，假设一个可判定性公理（即排中的一个实例）总是安全的。为什么？因为我们无法证明对这样一个公理的否定。如果可以，我们将同时拥有 [~ (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".

该怎么办？

Answer 1

excluded_middle_irrefutable该练习要求您在不假设任何公理的情况下进行证明。