coq - 在 Coq 中证明 (~A -> ~B)-> (~A -> B) -> A

Question

我一直试图在 Coq 中证明以下重言式。

Theorem Axiom3: forall A B: Prop, (~A -> ~B)-> ((~A -> B) -> A).

我的计划是做以下事情

Theorem Axiom3: forall A B: Prop, (~A -> ~B)-> ((~A -> B) -> A).
Proof.
  intros A B.
  unfold not.
  intros nA_implies_nB.
  intros nA_implies_B.
  pose (proof_of_False := nA_implies_nB nA_implies_B).
  case proof_of_False.
Qed.

但是，以下是我的问题所在。

 pose (proof_of_False := nA_implies_nB nA_implies_B).

我不能简单地将以下内容组合在一起以获得错误的证据。

nA_implies_nB : (A -> False) -> B -> False
nA_implies_B : (A -> False) -> B

我的证明是否可以修改或更正，或者是否有一种简单的方法来证明这个定理？

Answer 1

这个陈述等价于排中律，它说 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.