S0 (Halldén)

• [Feys, 1965, p139]
• Original source is Halldén's paper [Halldén, 1948] "A question concerning a logcial calculus related to Lewis's system of strict implication, which is of special interest for the study of entailment" in the Journal "Theoria", Volume 14, p265-269)

Notes

This system is known to be weaker than S1⁰ [Feys, 1965, p139]

The following are known to *NOT* be provable in S0:

• p => (p+q)
• (p&~p) => q (I.E. Contradictions don't imply everything)
• ([(p&q)=>r]&[(p&~q)=>r]} => (p => r)

[Feys, 1965, p139] (Quoting Halldén's paper)

S0 can be inbedded in the Relevant Logic Rbox, making it one of the earliest Relevant logics. [Priest, 2007 (email)]

S0 appears to be a paraconsistent logic, pubilshed the same year as Jaśkowski's paper giving system D2, which is normally credited as being the first paraconsistent logic. [Priest, 2007 (email)] (Note that Jaśkowski's paper should probably retain that credit, since it was specificly intending to treat something like paraconsistency. -JH)

Basis

S0 is Lewis' basis for S1 without the definition p => q =def ~M(p&~q) [Feys, 1965, p139] (Quoting Halldén's paper)

Or in other words, it is:

• Definitions
  • +, a+b = ~(~a&~b)
  • =, a=b = (a=>b)&(b=>a)
  • L, La = ~M~a
• Rules
  • Uniform substitution (US)
  • Modus Ponens for => (From |- p, and |- p=>q, infer |- q)
  • Adjunction (if |- a and |- b, infer |- a&b)
  • substitution of strict equivalents. (EQS)
• Axioms
  • AS1.1 [Also known as M1]: (p&q) => (q&p)
  • AS1.2 [Also known as M2]: (p&q) => p
  • AS1.3 [Also known as M4]: p => (p&p)
  • AS1.4 [Also known as M3]: ((p&q)&r) => (p&(q&r))
  • AS1.5 [Also known as M5]: ((p=>q)&(q=>r))=>(p=>r)
  • AS1.6: (p&(p=>q)) => q

Basis for

© Copyright 2007 by John Halleck, All Rights Reserved.
This page is http://www.cc.utah.edu/~nahaj/logic/structures/systems/s1.html
This page was last modified on January 9th, 2007.