偶然看到这个问题：为什么互为逆否的命题同真假？ - 知乎，尝试证明如下：
1
2
3
4
5
6
7
| Definition excluded_middle_statement := forall (P : Prop), P \/ ~P.
Definition double_negation_statement := forall (P : Prop), ~~P -> P.
Definition contraposition_2 := forall P Q, (~Q -> ~P) -> (P -> Q).
Theorem excluded_middle_iff_contraposition_2 :
excluded_middle_statement <-> contraposition_2.
Proof with try tauto. unfold excluded_middle_statement, contraposition_2. split; intros. destruct (H Q)... assert double_negation_statement. { intros Q. specialize (H True Q)... } apply H0... Qed.
|