System S3*

• [Sobociński, 1962]

Notes

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]

Go to ...

• Systems Page
• Structures Page
• Logic Page
• John Halleck's home page

© Copyright 2006, by John Halleck, All Rights Reserved.
This page is http://www.cc.utah.edu/~nahaj/logic/structures/systems/s3star.html
This page was last modified on August 4th, 2006