System S3 (Lewis)


This system is the original Lewis system from his "Survey of Symbolic Logic", 1918. (In that form it has it's own page at S, based on [Lewis, 1918] ). HOWEVER, the 1918 version had the axiom (p => q) <=> (~Mq => ~Mp) which, in the end destroys the modal nature of the system. This was corrected in his 1920 "Strict Implication, An Emendation.". The corrected form was (p => q) => (~Mq => ~Mp) [Zeman, 1973, p161]+[Lewis and Langford, 1932, appendix II, p492]

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. [Simons, 1953, p310]. He 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 from Wajsberg's original paper.

There is a validity preserving transformation of the Heyting Propositional Calculus H into S3. [Hacking, 1963, p52] (Primary source)

[Hughes and Cresswell, 1996, p207] say that S3 is the intersection of S4 and S7 (In the sense that a theorem is a theorem of S3 if, and only if, it is a theorem of both S4 and S7.)

There is an article that lists all of the possible modality reductions of systems that contain S3. S3 is also that paper's system 20p. [Pledger, 1972]

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

The distinct affirmative modalities in S3 are:

p       implied by Lp            it implies Mp

Lp      implied by LLp           it implies p, LMLp
Mp      it implies MMp           implied by p, MLMp

LLp                              it implies Lp, LLMLp
MMp                              implied by Mp, MMLMp

LMp     implied by LMLp, LMLLMp  it implies LMMp, MLMp
MLp     it implies MLMp, MLMMLp  implied by MLLp, LMLp

LLMp    implied by LLMLp         it implies LMLLMp
MMLp    it implies MMLMp         implied by MLMMLp

LMLp    implied by Lp, LMLLp     it implies LMp, MLp, LMMLp
MLMp    it implies Mp, MLMMp     implied by MLp, LMp, MLLMp

LMMp    implied by LMp, LMMLp    it implies MLMMp
MLLp    it implies MLp, MLLMp    implied by LMLLp

LLMLp   implied by LLp           it implies LLMp, LMLLp
MMLMp   it implies MMp           implied by MMLp, MLMMp

LMLLp   implied by LLMLp         it implies LMLp, MLLp, LMLLMp
MLMMp   it implies MMLMp         implied by MLMp, LMMp, MLMMLp

LMMLp   implied by LMLp          it implies LMMp, MLMMLp
MLLMp   it implies MLMp          implied by MLLp, LMLLMp

LMLLMp  implied by LLMp, LMLLp   it implies LMp, MLLMp
MLMMLp  it implies MMLp, MLMMp   implied by MLp, LMMLp

[Pledger, 1972, p270-271]

These can be diagrammed as:Diagram of the relationships listed above

The diagram above is being used by permission of Dr. Ken Pledger, and is taken from his article "Modalities of systems containing S3" [Pledger, 1972, p268]

Based on

The actual original form as given by Lewis is at S. (Note that the Lewis' original from used an impossibility operator, and not a possibility operator. Gödel first recast it into the possibility operator, which most later authors still use. - JH)

The system S3 is:

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

Note that Lewis and Langford called this THE system of Strict implication, They didn't rename is S3 until later. [See notes for S


[Simons, 1953, p309]

Note, that in [Feys, 1964, p89] Axiom H1 is missquoted as "p => (p+p)" instead of "p => (p&p)"


S3 is S30 plus Axiom M6 p=>Mp [Zeman, 1973, p281]

Or in other words, S3 is:

[Zeman, 1973, p281]

or (Sobociński)

S3 = S3* + p => Mp [Sobociński, 1962, p53]

or (Ishimoto)

[Feys, 1965, p90] (Quoting [Ishimoto, 1956] "A note on the paper 'A set of axioms of the modal propositional calculus equivalent to S3'", The Science of Thought (Tokyo) 2 by Arata Ishimoto, 1956)

Actually Feys has both "||" and "//" for the modal operator (the first binding losely and the second binding tightly), and both "|" and "/" for the regular stroke operator (the first binding losely and the second binding tightly). This was to avoid having to use prentheses. I find the using the prentheses to be less confusing so I've transcribed it that way... -JH

Basis for

S3 + H7 (MMp=>Mp) = S4 [Simons, 1953]

S3 + H8 [Mp=>~M~Mp] = S5 [Simons, 1953] [Parry, 1939, p151]

S3 + (MMp => ~M~MMp) [Or equivalently (MMp => LMMp) -jh] = S5 [Parry, 1939, p152]

S3 + (~M~p=>Mp)=>(p=>~M~Mp) = S5 [Anderson, 1956]

S3 + S (MMp) [Axiom S] = S7 [Halldén, 1950, p230] [Hughes and Cresswell, 1996, p364]

S3 + SP [LMMp] = S8 [Hughes and Cresswell, 1996, p364]

S3 + ~M~MMp = S8 [Halldén, 1950, p230]

S3 + Axiom 5[Mp>LMp] + Axiom S [MMp] = S9 [Åqvist, 1964, p79] (Åqvist calls this S7.5)

S3 + Axiom 5 [Mp>LMp] = S3.5 [Hughes and Cresswell, 1996, p364]

S3 + Axiom B [p>LMp] = S3.5 [Hughes and Cresswell, 1996, p208]

S3 + MLMMp = 20sb [Pledger, 1972, p279]

Go to ...

© Copyright 2007, by John Halleck, All Rights Reserved.
This page is
This page was last modified on December 15th, 2009