- [Feys, 1965, p139]
- Original source is
Halldén's paper [Halldén, 1948] "
*A question concerning a logical 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)

This system is known to be weaker than S1^{0}
[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 R[] (R box), making it one of the earliest Relevant logics. [Priest, 2007 (email)]

In a later email, Dr. Priest Clairified: "... if one maps the strict conditional of S0 to the arrow a relevant logic, the result is a subsystem of R[].

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)]

Jaskowski's paper is alleged to be: [But I've not seen it personally -JH]
S. Jaśkowski. "Propositional calculus for contradictory deductive
systems"
(in Polish). Studia Societatis Scientiarum Torunensis, section
A-I:57-77, 1948.
Translated into English:
Studia Logica, 24:143-157, 1967.
(Note that Jaśkowski's paper should probably retain that credit,
since it was specificly *intending* to treat something like
paraconsistency. -JH)

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

System S1 = S0 + definition p => q =def ~M(p&~q)

© Copyright 2016-2013 by John Halleck, All Rights Reserved. This page is http://www.cc.utah.edu/~nahaj/logic/structures/systems/s0.html This page was last modified on Saturday, September 14th, 2013.