# 在Coq中证明经典逻辑命题的等价性

Published:

## 一、概述

Exercise: 5 stars, standard, optional (classical_axioms)
For those who like a challenge, here is an exercise taken from the Coq'Art book by Bertot and Casteran (p. 123). Each of the following four statements, together with excluded_middle, can be considered as characterizing classical logic. We can't prove any of them in Coq, but we can consistently add any one of them as an axiom if we wish to work in classical logic.


Definition excluded_middle := forall P : Prop,
P \/ ~ P.

Definition peirce := forall P Q: Prop,
((P->Q)->P)->P.

Definition double_negation_elimination := forall P:Prop,
~~P -> P.

Definition de_morgan_not_and_not := forall P Q:Prop,
~(~P /\ ~Q) -> P\/Q.

Definition implies_to_or := forall P Q:Prop,
(P->Q) -> (~P\/Q).


classical_axioms_1: excluded_middle -> double_negation_elimination
classical_axioms_2: double_negation_elimination -> excluded_middle
classical_axioms_3: excluded_middle -> de_morgan_not_and_not
classical_axioms_4: de_morgan_not_and_not -> excluded_middle
classical_axioms_5: excluded_middle -> implies_to_or
classical_axioms_6: implies_to_or -> excluded_middle
classical_axioms_7: double_negation_elimination -> peirce
classical_axioms_8: peirce -> double_negation_elimination ## 二、证明

excluded_middle <-> double_negation_elimination

Theorem classical_axioms_1 (* 很简单 *)
: excluded_middle -> double_negation_elimination.
Proof.
unfold double_negation_elimination.
unfold excluded_middle. unfold not.
intros H P H0. destruct (H P) as [H1|H2].
- apply H1.
- apply H0 in H2. destruct H2.
Qed.

Theorem classical_axioms_2
: double_negation_elimination -> excluded_middle.
Proof.
unfold double_negation_elimination.
unfold excluded_middle. unfold not.
intros H P. apply H.
intro H0. (* H0 : P \/ (P -> False) -> False *)
assert ((P -> False) -> False).
{ intros. apply or_intror with (A:=P) in H1.
apply H0 in H1. (* H1 : False *)
apply H1. }
(* H1 : (P -> False) -> False *)
apply H in H1. (* H1 : P *)
apply or_introl with (B:=P->False) in H1.
apply H0 in H1. (* H1 : False *)
apply H1.
Qed.


excluded_middle <-> de_morgan_not_and_not

Theorem classical_axioms_3
: excluded_middle -> de_morgan_not_and_not.
Proof.
unfold de_morgan_not_and_not.
unfold excluded_middle.
unfold not. intros.
destruct (H Q).
- right. apply H1.
- destruct (H P).
+ left. apply H2.
+ destruct H0. split. ++ apply H2. ++ apply H1.
Qed.

Theorem classical_axioms_4
: de_morgan_not_and_not -> excluded_middle.
Proof.
unfold de_morgan_not_and_not.
unfold excluded_middle.
unfold not. intros.
apply H. intros [H1 H2]. apply H2. apply H1.
Qed.


excluded_middle<->implies_to_or

Theorem classical_axioms_5
: excluded_middle -> implies_to_or.
Proof.
unfold excluded_middle.
unfold implies_to_or.
unfold not. intros.
destruct (H P).
- right. apply H0 in H1. apply H1.
- left. apply H1.
Qed.

Theorem classical_axioms_6
: implies_to_or -> excluded_middle.
Proof.
unfold excluded_middle.
unfold implies_to_or.
unfold not. intros.
assert((P -> False)\/P ->  P \/ (P -> False)).
{ intros. destruct H0. right. apply H0. left. apply H0. }
apply H0.
apply H.
intros. apply H1.
Qed.


double_negation_elimination<->peirce

Theorem classical_axioms_7
: double_negation_elimination -> peirce.
Proof.
unfold double_negation_elimination.
unfold peirce.
unfold not. intros.
apply H.
intros. apply H1. apply H0. intros.
apply H1 in H2. destruct H2.
Qed.

Theorem classical_axioms_8
: peirce -> double_negation_elimination.
Proof.
unfold peirce.
unfold double_negation_elimination. unfold not.
intros.
apply H with (Q:=False).
intros. apply H0 in H1. destruct H1.
Qed.


Coq好有意思！！！

Tags:

Categories: