System C4

[Hughes and Cresswell, 1968]

[Anderson and Belnap, 1962]

[Ulrich, 1981]

Notes

There are at least 6, and no more than 8 two axiom bases for C4 [EFHW, 2002, pg. 170]

Based on

Originally from [Anderson and Belnap, 1962, p31-32]

Based on

C1: p => p
C2: (p=>(q=>r)) => ((p=>q)=>(p=>r))
C4: a => (p=>a) [Where a is strict (I.E. of the form X => y)]

[Hughes and Cresswell, 1968, p295]

Based on

Note that this is the shortest possible two axiom basis for C4

p=>(q=>q)
(p=>(q=>r)) => ( (p=>q) => (s => (p => r)))

[EFHW, 2002, pg. 170]

Based on

Note that this is the shortest possible single axiom basis for C4 [EFHW, 2002, pg. 171]

(p=>((q=>(r=>r)))=>(p=>s)) => ((s=>t)=>(u=>(p=>t)))

[EFHW, 2002, pg. 171]

Basis for

Go to ...

Notes

My thanks to Dolph Ulrich [Ulrich, email, 2005] for straightening me out and documenting that the two C4's that used to be on this page were the same system.