偶然看到这个问题:为什么互为逆否的命题同真假? - 知乎,尝试证明如下:
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.
|