0%

「逆否命题⟶原命题」(也)等价于排中律

偶然看到这个问题:为什么互为逆否的命题同真假? - 知乎,尝试证明如下:

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.