System S1 (Lewis)


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.

Based on (Lewis)

The system S1 (S for strict) is:

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

[Feys, 1965, p43]

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

OR (Halldé)

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)

OR (Lemmon)

[Lemmon, 1957, p177]

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


S1 is S10 plus the axiom M6 p=>Mp [Zeman, 1973, p281]

Therefore the system S1 is:

[Zeman, 1973, p281]


[Zeman, 1968, p459]

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

Basis for

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]

Go to ...

© Copyright 2006, by John Halleck, All Rights Reserved.
This page is
This page was last modified on July 29th, 2008