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=gt;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
These can be diagrammed as:
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]
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=>~Mq) [Lewis and Langford, 1932, p500 + axioms on page 493] [Hughes and Cresswell 1968, p233, p233fn]
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:
S3 = S3* + p => Mp [Sobociński, 1962, p53]
[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
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]
© Copyright 2007, by John Halleck, All Rights Reserved.
This page is http://www.cc.utah.edu/~nahaj/logic/structures/systems/s3.html
This page was last modified on August 5th, 2007