逻辑：excluded_middle_irrefutable

Question

这是书中的任务：

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.

据我理解的任务，我必须介绍排中公理。 但我不确定我做对了:

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。