Section A_fixed. Variable A:Set. Variables P Q S: A->Prop. Variable R : A->A->Prop. Lemma imp_all_dist : (forall a, P a -> Q a) -> (forall b, P b) -> forall c, Q c. Admitted. Lemma ex_or : (exists a, P a \/ Q a) -> (exists a, P a) \/ (exists a, Q a). Admitted. Lemma not_ex_all: (exists a, P a) -> ~ forall a, ~(P a). Admitted. Section classic. Hypothesis excluded_middle : forall P, P \/ ~P. Lemma not_all_ex : ~(forall a:A, ~P a)-> exists a, P a. intro H. elim (excluded_middle (exists a, P a)). Admitted. End classic. Lemma all_equal : (exists a:A, forall b, a = b) -> forall x y:A, x = y. intro H; elim H; intros a Ha x y. transitivity a. Admitted. Lemma diff_sym : forall a b:A, a<>b -> b<>a. Admitted. End A_fixed. (* prove the equivalence of the foloowing five characterisations of classical logic. You may use the tactic "unfold " to replace the constant with its definition in the current goal. The variant "unfold const in H" operates the same way in the hypothesis H *) Definition PEIRCE := forall P Q:Prop, ((P->Q)->P)->P. Definition CLASSIC := forall P:Prop, ~~P -> P. Definition EXCLUDED_MIDDLE := forall P:Prop, P\/~P. Definition DE_MORGAN_NOT_AND := forall P Q:Prop, ~(~P/\~Q)->P\/Q. Definition IMPLIES_TO_OR := forall P Q:Prop, (P->Q)->(~P\/Q). Lemma EXCLUDED_MIDDLE_PEIRCE : EXCLUDED_MIDDLE -> PEIRCE. Proof. Admitted. Lemma PEIRCE_CLASSIC : PEIRCE -> CLASSIC. Proof. Admitted. Lemma CLASSIC_EXCLUDED_MIDDLE: CLASSIC -> EXCLUDED_MIDDLE. Proof. Admitted. Lemma EXCLUDED_MIDDLE_IMPLIES_TO_OR : EXCLUDED_MIDDLE -> IMPLIES_TO_OR. Proof. Admitted. Lemma IMPLIES_TO_OR_EXCLUDED_MIDDLE : IMPLIES_TO_OR -> EXCLUDED_MIDDLE. Proof. Admitted. Lemma CLASSIC_DE_MORGAN_NOT_AND : CLASSIC -> DE_MORGAN_NOT_AND. Proof. Admitted. Lemma DE_MORGAN_NOT_AND_EXCLUDED_MIDDLE : DE_MORGAN_NOT_AND -> EXCLUDED_MIDDLE. Proof. Admitted.