Standard Axiom Schemata

Propositional Logic

Implication Introduction: s => (t => s)
Implication Distribution: (r => (s => t)) => ((r => s) => (r => t))
Conflict Resolution: (~t=>s) => ((~t=>~s)=>t)
                     (t=>s) => ((t=>~s)=>~t)

EQ:     (s<=>t) => (s=>t)
        (s<=>t) => (t=>s)
        (t=>s) => ((s=>t) => (s<=>t))

OQ:     (s<=t) <=> (t=>s)
OQ:     (s|t) <=> (~s=>t)
OQ:     (s&t) <=> ~(~s|~t)

Relational Logic

Implication Introduction: s => (t => s)
Implication Distribution: (r => (s => t)) => ((r => s) => (r => t))
Conflict Resolution: (~t=>s) => ((~t=>~s)=>t)
                     (t=>s) => ((t=>~s)=>~t)

EQ:     (s<=>t) => (s=>t)
        (s<=>t) => (t=>s)
        (t=>s) => ((s=>t) => (s<=>t))

OQ:     (s<=t) <=> (t=>s)
OQ:     (s|t) <=> (~s=>t)
OQ:     (s&t) <=> ~(~s|~t)

UD:     Av.(s => t) => (Av.s => Av.t)

UG:     s => Av. s
        where v is not free in s

UI:     Av. s => s [v <-- v_2]
        where v_2 is free for v in s

ED:     Ev. s <=> ~Av. ~s