System S4 (Lewis)



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

Technical Notes

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]

Based on

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

[Pledger, 1972, p275]


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)

[Simons, 1953, p314]


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

Or, in other words, S4 is:

[Zeman, 1973, p281]

OR (Feys)

The system S4 is:

[Feys, 1965, p97]

Basis for

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]

Go to ...

© Copyright 2000, by John Halleck, All Rights Reserved.
This page is
This page was last modified on December 25th, 2006