# /home/nahaj/public_html/logic/systems/t.txt
# Transformation rules.
T
Modal System T
US
Uniform Substitution
p
MP
Modus Ponens
p
(IMP p q)
q
N
Necessatation
p
(NES p)
# 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
# ==================================================
# Modal system K
(IMP (NES (IMP p q)) (IMP (NES p) (NES q)))
Axiom
# Modal system T
(IMP (NES p) p)
Axiom