Section Propositional_Logic. Variables P Q R S: Prop. Theorem P_or_False : P \/ False -> P. Admitted. Theorem and_idempotent_1 : P -> P /\ P. Admitted. Theorem and_idempotent_2 : P/\P -> P. Admitted. Theorem and_or_dist : (P\/Q)/\R -> (P/\R)\/(Q/\R). Admitted. Theorem absurd : P -> ~P -> Q. Admitted. Theorem demorgan1 : P /\ Q -> ~(~P \/ ~Q). Admitted. Theorem demorgan2 : ~(P \/ Q) -> ~P /\~Q. Admitted. Theorem demorgan3 : P \/ Q -> ~(~P /\ ~Q). Admitted. End Propositional_Logic.