Это утверждение эквивалентно принципу исключенного среднего , который гласит, что A \/ ~A
выполняется для любого предложения A
. Исключенная середина печально известна своим отсутствием в Coq и других системах, основанных на конструктивной математике. Чтобы доказать утверждение в Coq, вы должны явно объявить, что вы хотите принять неконструктивные рассуждения.
Require Import Coq.Logic.Classical.
Theorem Axiom3: forall A B: Prop, (~A -> ~B)-> ((~A -> B) -> A).
Proof. intros A B. tauto. Qed.
Если вы закомментируете первую строку, вы увидите, что доказательство не удалось, потому что Coq не будет пытаться использовать исключенную середину в доказательстве.
Если вам интересно, вот более явное доказательство того, как Axiom3
подразумевает исключенную середину:
Axiom Axiom3: forall A B: Prop, (~A -> ~B)-> ((~A -> B) -> A).
Lemma classical : forall A : Prop, A \/ ~ A.
Proof.
intros A.
apply (Axiom3 (A \/ ~A) (A \/ ~A)).
- trivial.
- intros H. exfalso.
assert (H' : ~ ~ A).
{ intros HA. apply H. right. trivial. }
apply H'. intros HA. apply H. left. trivial.
Qed.