James Dugundji [Dugundji, 1940, p150-151] proved that there is no finite Characteristic Matrix for S1.

M. Wajsberg showed ("*Ein erweiterter Klassenkalkül*" in
Monatshefte für Mathematik und Physik, vol 40 (1933), p 118f) that
if a>b is a (PC) tautology, then a=>b is a
theorem in S3 (not S1).
[Simons,
1953, p310].
**But** Simons goes on to say that Parry extended this to S1.
[Parry,
1939, p143, last paragraph,
and the footnote.] (The paragraph says that his proof is only valid for
S3 and above, but the footnote says how to prove it
for S1 and above from Wajsberg's original paper.

The system S1 (S for strict) is:

- Definitions
- +, a+b = ~(~a&~b)
- =>, a=>b = ~M(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

Note that the original also had: ~ ~ p => p, but that was shown
redundant by J. C. C. Mckinsey, "*A reduction in the number of postulates
for C. I. Lewis' system of strict implication*" in the "*Bulletin of
the American Mathematical Society"*,
Vol. 40 (1934) pgs 110-112

[Lewis and Langford, 1932, p500] Systems S1 through S5 are defined in the last few pages of the last appendex of the book (p500-502). And not directly by a list of axioms of each systems, but by prose that says things like "System S1 is axioms B1-B7". The common axiom list is on page 493. Adjunction, Modus Ponens (Called the "rule of inference"), and "substitution of equivalents" are on pg. 494. Uniform substitution is implicitly included, as introduced on page 125. The definitions above are introduced in Chapter 11, P123-124 (As syntatic equalities, but the '=' sign was stated (p123) to mean logical equivalences.)

[Hughes and Cresswell, 1996, pg 198] (Who also point out that many of the definitions were equivalence axioms in the original)

S1 = S0 + the definition "p => q ==def ~M(p&~q) [Feys, 1965, p139 (Since, in fact, Halldén formed S0 by taken the Lewis basis for S1, and removing the definition. -JH)

- PC
- rule Uniform Substitution US
- rule Modus Ponens

- Definitions
- =>, a=>b = L(a>b)

- Rules
- Axioms

[Hughes and Cresswell, 1996, pg 199-200]

S1 is S1^{0} plus the axiom
M6 p=>Mp
[Zeman, 1973, p281]

Therefore the system S1 is:

- Definitions
- +, a+b = ~(~a&~b)
- =>, a=>b = ~M(a&~b)
- =, a=b = (a=>b)&(b=>a)
- L, La = ~M~a

- Rules
- Axioms
- M1: (p&q)=>(q&p)
- M2: (p&q)=>p
- M3: ((p&q)&r)=>(p&(q&r))
- M4: p=>(p&p)
- M5: : ((p=>q)&(q=>r))=>(p=>r)
- M6: p=>Mp

- System PC as a base
- Rules
- Ga': If φ is a PC theorem, or an axiom, then generate Lφ
- Gb': If you have L(φ > ψ) and you have L(ψ > φ) then generate L(Lφ > Lψ)

- Axioms
- G2: Lp > p
- G3: (L(p>q) & L(q>r)) > L(p>r)

Note that the article also builds S1^{0},
and the ONLY difference between S1^{0} and S1 is that S1 has the
AXIOM (Lp > p), and S1^{0}
has the RULE "if |- Lp infer |- p".

The system T = S1 plus any axiom of the form LLα where LLα is a T theorem [Such as LL(p&p) or LL(any PC thesis) -JH] [Hughes and Cresswell, 1968, p227fn (and see 223-227)]

System S2 = S1 + M(p&q)=>(Mp&Mq) [Hughes and Cresswell, 1996, p200]

System S2 = S1 + M(p&q) => Mp [Hughes and Cresswell 1968, p230]

System S3 = S1 + S3 (p=>q)=>(~Mp=>~Mq) [Lewis and Langford, 1932, p500 + axioms on page 493] [Hughes and Cresswell 1968, p233, p233fn]

System S4 = S1 + Lp=>LLp [Hughes and Cresswell 1968, p236]

System S5 = S1 + Mp=>LMp [Feys, 1965, p115] [Hughes and Cresswell 1968, 237]

© Copyright 2006, 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 July 29th, 2008