# /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
#
# -------------------------------------------------------------------