# System S3*

## Based on

The system S3* is:

• Definitions
• + : a+b =def ~(~a & ~b)
• => : a=>b =def ~M(a & ~b)
• > : a >b =def ~ (a & ~b)
• <=> : a <=> b =def ( (a => b) & (b => a)) [Strict equivalence]
• La : L a =def ~M~a
• Rules
• Uniform substitution (US)
• Strict detachment (MP=>)
• Axioms
• Z1: p => (p&p)
• Z2: ((p&q)=>q)
• Z3: ((r&p)&~(q&r)) => (p&~q)
• Z4: (p=>q)=>(~Mq=>~Mp)
• Z5: ~Mp > ~p

[Sobociński, 1962, p53]

## OR

Note that Sobociński presents both this basis, and (parenthetically) the basis above. -JH

• Definitions
• + : a+b =def ~(~a & ~b)
• => : a=>b =def ~M(a & ~b)
• > : a >b =def ~ (a & ~b)
• <=> : a <=> b =def ( (a => b) & (b => a)) [Strict equivalence]
• La : L a =def ~M~a
• Rules
• Uniform substitution (US)
• Strict detachment (MP=>)
• Axioms
• Z1: ~M(p & ~(p&p))
• Z2: ~M((p&q)&~q)
• Z3: ~M(((r&p)&~(q&r))&~(p&~q))
• Z4: ~(~M(p&~q)&~~M(~Mq&~~Mp))
• Z5: ~(~Mp&~~p)

[Sobociński, 1962, p53] *** note: *** Sobociński has a typo in Z2, on first occurance, but it is correct in the second occurance. (NMKpqNq vs. NMKKpqNq) (And note that the original is in Polish notation, and I've converted it to infix, as usual.) -JH

## Basis for

S3 = S3* + p => Mp [Sobociński, 1962, p53]