Логика: excid_middle_irrefutable

Question

Вот задание из книги:

Доказательство соответствия Coq общей исключенной средней аксиоме требует сложных рассуждений, которые не могут быть выполнены в самой Coq. Однако следующая теорема подразумевает, что всегда безопасно принять аксиому разрешимости (т. Е. Случай исключенного среднего) для любого конкретного пропа [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 без принятия каких-либо аксиом.