# /home/nahaj/public_html/logic/systems/pc.txt # Transformation rules. pclt A Default PC basis US Uniform Substitution p MP Modus Ponens p (IMP p q) q # initial axioms. (IMP p (IMP q p)) Axiom A1 (IMP (IMP p (IMP q r)) (IMP (IMP p q) (IMP p r))) Axiom A2 (IMP (AND p q) p) Axiom A3 (IMP (AND p q) q) Axiom A4 (IMP p (IMP q (AND p q))) Axiom A5 (IMP p (OR p q)) Axiom A6 (IMP q (OR p q)) Axiom A7 (IMP (IMP p r) (IMP (IMP q r) (IMP (OR p q) r))) Axiom A8 (IMP (EQV p q) (IMP p q)) Axiom A9 (IMP (EQV p q) (IMP q p)) Axiom A10 (IMP (IMP p q) (IMP (IMP q p) (EQV p q))) Axiom A11 # ---------- (IMP (IMP (NOT p) (NOT q)) (IMP q p)) Axiom A12 # --- Alternate sets that would have given the same system: # # ------------------------------------------------------------------ # # (IMP (NOT (NOT p)) p) # Axiom A12 Law of double negation # # # # (IMP p (IMP (q (NOT q)) (NOT q))) # Axiom A13 Kant's Satz des Widerspruchs) # # ------------------------------------------------------------------ # # (OR p (NOT p)) # Axiom A12 Law of excluded middle # # # # (IMP (NOT p) (IMP p q)) # Axiom A13 Law of the denial of the antecedent # # # # (IMP (IMP p (NOT p)) (NOT p)) # Axiom A14 Special law of reductio # # -------------------------------------------------------------------