(* Predicate calculus *) 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. Proof. intros H H0 c; apply H; apply H0. Qed. Lemma ex_or : (exists a, P a \/ Q a) -> (exists a, P a) \/ (exists a, Q a). Proof. intros H; elim H; intros a [Hp|Hq]. left; exists a; auto. right; exists a; auto. Qed. Lemma not_ex_all: (exists a, P a) -> ~ forall a, ~(P a). Proof. red; intros H H0. elim H; intros a Ha. elim (H0 a). trivial. Qed. Section classic. Hypothesis excluded_middle : forall P, P \/ ~P. Lemma not_all_ex : ~(forall a:A, ~P a)-> exists a, P a. Proof. intro H. elim (excluded_middle (exists a, P a)). trivial. intro H0. elim H. red; intros a Ha. elim H0; exists a; trivial. Qed. End classic. Lemma all_equal : (exists a:A, forall b, a = b) -> forall x y:A, x = y. Proof. intro H; elim H; intros a Ha x y. rewrite <- (Ha x). apply Ha. Qed. Lemma diff_sym : forall a b:A, a<>b -> b<>a. Proof. red;intros a b H H0. elim H. rewrite H0; reflexivity. Qed. End A_fixed. 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. unfold PEIRCE; intros H P Q H0. case (H P). trivial. intro H1; apply H0; intro H2; absurd P; auto. Qed. Lemma PEIRCE_CLASSIC : PEIRCE->CLASSIC. Proof. unfold CLASSIC; intros H P H0. apply (H P False). intro H1. case H0. assumption. Qed. Lemma CLASSIC_EXCLUDED_MIDDLE: CLASSIC->EXCLUDED_MIDDLE. Proof. unfold EXCLUDED_MIDDLE; intros H P. apply H. unfold not at 1; intro H0. absurd P. intro H1; apply H0; auto. apply H; intro H1; apply H0; auto. Qed. Lemma EXCLUDED_MIDDLE_IMPLIES_TO_OR : EXCLUDED_MIDDLE -> IMPLIES_TO_OR. Proof. unfold IMPLIES_TO_OR; intros H P Q H0. case (H P); intro H1. right; auto. left; trivial. Qed. Lemma IMPLIES_TO_OR_EXCLUDED_MIDDLE : IMPLIES_TO_OR -> EXCLUDED_MIDDLE. Proof. unfold EXCLUDED_MIDDLE; intros H P. case (H P P); auto. Qed. Lemma CLASSIC_DE_MORGAN_NOT_AND : CLASSIC -> DE_MORGAN_NOT_AND. Proof. unfold DE_MORGAN_NOT_AND; intros H P Q H0. apply H. intro H1. apply H0. split;intro;apply H1; auto. Qed. Lemma DE_MORGAN_NOT_AND_EXCLUDED_MIDDLE : DE_MORGAN_NOT_AND -> EXCLUDED_MIDDLE. Proof. unfold EXCLUDED_MIDDLE; intros H P. apply H; intro H1; elim H1; auto. Qed.