# /home/nahaj/public_html/logic/systems/pc.txt
# Transformation rules.
fitch
PC Fitch system
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 (NOT p) (IMP p q))
Axiom-Fitch-1
(EQV p (NOT (NOT p)))
Axiom Fitch 2
(EQV (NOT (OR p q)) (AND (NOT p) (NOT q)))
Axiom Fitch 3
(EQV (NOT (AND p q)) (OR (NOT p) (NOT q)))
Axiom Fitch 4