References:

- [Chellas, 1980]
- [Feys, 1965]
- [Hughes and Cresswell, 1996]
**[Lewis and Langford, 1932]**(Original Source)- [Pledger, 1972]
- [Simons, 1953]
- [Zeman, 1973]

This system is also von Wright's system M' -JH

Originally named by Lewis in his "Survey of Symbolic Logic"

Characterized by reflexive transitive frames. [Hughes and Cresswell 1996, p59]

This system is Pledger's system 6s [Pledger 1972, p270-271]

This system is also S4* [Hughes and Cresswell 1996, p344 B]

This system is also Kρτ [Priest, 2001, p39]

This system is also νρSc (Porte) [Feys, 1965, p144]

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

Any system containing S4 can have at most 14 distinct modalities. (none), L, M, LM, ML, LML, MLM, and their negations. [Chellas, 1980, P149]

In S4 itself they are related as:

p implied by Lp it implies Mp Lp it implies p, LMLp Mp implied by p, MLMp LMp implied by LMLp it implies MLMp MLp it implies MLMp implied by LMLp LMLp implied by Lp it implies LMp, MLp MLMp it implies Mp implied by MLp, LMp

[Pledger, 1972, p270-271] [Chellas, 1980, P149] (Note that this is a proper subset of those in S3)

The system S4 has structural similarity to Intuitionist PC, in that there are validity preserving transformations between them. [Hughes and Cresswell, 1996, p225] (Quoting [McKinsey and Tarski, 1948, p13] which showed that there was a mapping from Heyting Propositional Calculus H to S4.) Note that Ian Hacking [Hacking, 1963] proved that the Heyting Propositional Calculus H could also be mapped onto S3

[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 exists clausal tableau system for S4 that has space requirements on the order of N log N. [Nguyen, 1999]

McKinsey [McKinsey, 1941, p126] gives a decision procedure for S4.

Leonard, von Wright, and Anderson have produced decision procedures for S4 [Feys, 1965, p109]

The system S4 is S3 and any one of the following (Arranged as axiom, dual):

Lp => LLp, MMp => Mp Lp => LLMp, MMLp => Mp Lp => LLMLp, MMLMp => Mp LMp => LLMp, MMLp => MLp LMMp => LLMp, MMLp => LMMp LMLp => LLMp, MMLp => MLMp LMLp => LLMLp, MMLMp => MLMp LMMLp => LLMp, MMLp => MLLMp LMMLp => LLMLp, MMLMp => MLLMp

The system S4 result of T and the Axiom S4: Lp>LLp [Hughes and Cresswell, 1996, p53]

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

The system S4 is the result of S3 + Axiom H7 [MMp=>Mp]

(Specifically Simons built S4 on top of his basis for S3)

- Definitions
- Lp ==def ~M~p
- p+q ==def ~(~p+~q)

- Rules:
- Uniform substitution (US) [Actually, Simons presented the system in terms of axiom schemata instead of substitution -JH]
- Material Detachment From |- p and |- p>q infer |- q

- Axioms

The system S4 is the result of S4^{0} + Axiom
M6[ p=>Mp ]
[Zeman, 1973, p281]

Or, in other words, S4 is:

- Definitions
- [todo]

- Rules
- Axioms

The system S4 is:

- System PC
- Uniform substitution (US)
- Modus Ponens for > (From |- p and |- p> q infer |- q)

- Definitions
- p=>q =def L(p>q)

- Rules
- (None other than the ones inherited from PC.)

- Axioms
- 63.111: (p=>q) > (p>q)
- 63.112: p > (q > (p&q))
- 63.113: (p=>q) => (~q => ~p)
- 63.114: ((p=>q)&(r=>s)) => ((p&r) => (q&s))
- 63.115: (p=>q) => (Mp => Mq)

S5 = S4 + Axiom B [p > LMp] Hughes and Cresswell, 1996]

S4.2 = S4 + Axiom G1 [MLp > LMp] [Hughes and Cresswell, 1996]

S4.3 = S4 + D1 [L(Lp>q)+L(Lq>p)] [Hughes and Cresswell, 1996]

S4F = S4 + F [(LMp & LMq) > M(p&q)] [Hughes and Cresswell, 1996, p131]

S4M = S4 + MS [LMp>MLp] [Hughes and Cresswell, 1996, p131]

S4.1 = S4 + N1 [L(L(p>Lp)>p)>(MLp>p)] [Hughes and Cresswell, 1996, p362]

S4.3.2 = S4 + the axiom M17 [(Lp=>q)+(MLq>p)] [Zeman, 1973, p253]

S4.4 = S4 + the axiom M16 [p=>(MLp>Lp)] [Zeman, 1973, p249]

S4.4 = S4 + the axiom + the axiom HCR1 [MLp>(p>Lp)] [Hughes and Cresswell, 1996, p362]

S4.03 = the system S4 + the axiom L(Lp > q) + (LMLq > p) [Georgacarakos, 1977, p480]

S4.03 = the system S4 + the axiom (LMLp & q) > L(p + Mq) [Georgacarakos, 1977, p483]

S4.01 = S4 + the axiom MLp > (LMp > LMLp) [Goldblatt, 1973a, p567]

S4.01 = S4 + the axiom MLp > L(LMp > MLp) [Goldblatt, 1973a, p567]

S4.01 = S4 + the axiom ML(p>Lp) > L(LMp > MLp) [Goldblatt, 1973a, p567]

S4.01 = S4 + the axiom (LMp>MLp) > L(LMp>MLp) [Goldblatt, 1973a, p567]

© Copyright 2000, by John Halleck, All Rights Reserved.

This page is http://www.cc.utah.edu/~nahaj/logic/structures/systems/s4.html

This page was last modified on December 25th, 2006