Вот задание из книги:
Доказательство согласованности 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".
Чтоделать?