- [Åqvist, 1964]
- [Anderson, 1956]
- [Cresswell, 1967]]
- [Halldén, 1950]
**[Feys, 1965]**- [Hughes and Cresswell, 1968]
- [Hughes and Cresswell, 1996]
**[Lewis and Langford, 1932]**(Original Source)- [Pledger, 1972]
- [Simons, 1953]
- [Zeman, 1973]

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

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=>~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- Definitions. These are not explictly given, although they are used (for
example the defininition of => is used in lines 1 and 2 of the proof
of theorem 1. They are the standard definitions of Lewis' system
S (Also known as S3) and
(though strange to modern eyes) were in common use.
- p=>q =def ~M(p&~q)
- Lp =def ~M~p

- Rules
- Uniform Substitution [Actually, Simons presented his system in terms of axiom schemata instead of axioms, and therefore didn't need a substitution rule. -jh]
- Modus ponens for >

- Axioms

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

S3 is S3^{0} plus Axiom
M6 p=>Mp
[Zeman, 1973, p281]

Or in other words, S3 is:

- Definitions
- ?

- Rules
- Axioms

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

- Operators
- "|" is the Sheffer Stroke
- "||" is a DIFFERENT operator usually interpreted as ~M(P&Q)

- Definitions
- P=>Q =def P || (P|Q)
- P>Q =def P | (P|Q)
- ~P =def P | P
- P+Q =def (P|P) | (Q|Q)
- P&Q =def (P|Q) | (P|Q)
- Mp =def (P||P) | (Q||Q)

- Rules
- MP for =>
- Adjunction: if |- P and |- Q infer P&Q

- Axioms
- p||(q|r) => ((s|q)=>(p|s))
- p => p
- p||(q|r) => ( (s||q) => (p||s) )
- (p||q) => (p|q)
- (p||p) => (p||q)
- (((p|q)|(p|q)) || ((p|q)|(p|q))) => (p||q)

[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 December 15th, 2009