如何证明(~Q -> ~P) -> (P -> Q)

Question

我试图在coq中证明(~Q -> ~P) -> (P-> Q)，这是反正定理(P -> Q) (~Q -> ~P)的逆。目前我正在考虑使用同样的逻辑来证明反正定理，如下所示：

不展开。介绍A。B。C。申请B。申请A。

然而，我在一开始就被卡住了。也许我需要额外的公理来证明反正定理的逆。有谁可以帮我？

Answer 1

Require Import Classical.

Lemma myproof :  forall (P Q : Prop), (~Q -> ~P) -> (P -> Q) . 
unfold not. intros P Q. intros A B.
destruct (classic Q) as [Q_holds|NQ_holds].
apply Q_holds.
apply False_ind.
apply A.
apply NQ_holds.
apply B.
Qed.

Answer 2

是的，你需要一些额外的能力(经典逻辑)来做到这一点。放

Require Import Classical.

在您的文件的开头。现在，当你有一个命题Q

destruct (classic Q) as [Q_holds|NQ_holds].

它创建了两个子目标:一个是Q有效，另一个是~Q有效。

再加上定理False_ind (允许您从False证明任何东西)，应该足以得出您的证明结论。