Section Minimal_Propositional_Logic. Variables P Q R S : Prop. Theorem imp_perm : (P->Q->R)->(Q->P->R). Proof. intros H q p; apply H; assumption. Qed. Theorem imp_dist : (P->Q->R)->(P->Q)->P->R. Proof. intros H H0 p; apply H. assumption. apply H0; assumption. Qed. Theorem P3_Q : (((P->Q)->Q)->Q) -> P->Q. Proof. intros H p; apply H. intro H0; apply H0; assumption. Qed. Theorem weak_peirce : ((((P->Q)->P)->P)->Q)->Q. Proof. intro H; apply H. intro H0; apply H0. intro p; apply H. intro H1; assumption. Qed. (* Notice that Peirce : ((P->Q)->P)->P is valid but non provable in Mimimal propositional intuitionist logic *) End Minimal_Propositional_Logic.