Section Minimal_Propositional_Logic. Variables P Q R S : Prop. Theorem imp_perm : (P->Q->R)->(Q->P->R). Admitted. Theorem imp_dist : (P->Q->R)->(P->Q)->P->R. Admitted. Theorem P3_Q : (((P->Q)->Q)->Q) -> P->Q. Admitted. Theorem weak_peirce : ((((P->Q)->P)->P)->Q)->Q. Admitted. (* Notice that Peirce : ((P->Q)->P)->P is valid but non provable in Mimimal propositional intuitionist logic *) End Minimal_Propositional_Logic.