System S4 (Lewis)

References:

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

Notes

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
LMMLp => LLMLp,  MMLMp => MLLMp

[Pledger, 1972, p275]

OR

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

OR

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

OR

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
- H1: a => (a & a)
- H2: (a & b) => b
- H3: ((c&a)&~(b&c)) => (a&~b)
- H4: ~Ma => ~a
- H5: a => Ma
- H6: (a => b) => (~Mb => ~Ma))
- H7: MMp => Mp

[Simons, 1953, p314]

OR

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

Or, in other words, S4 is:

Definitions
- [todo]
Rules
- Uniform substitution (US)
- Strict detachment (MP=>)
- substitution of strict equivalents. (EQS)
- Adjunction (given |- p and |- q, infer |- a&b) (AD)
Axioms
- M1: (p&q)=>(q&p)
- M2: (p&q)=>p
- M3: ((p&q)&r)=>(p&(q&r))
- M4: p=>(p&p)
- M5: ((p=>q)&(q=>r))=>(p=>r)
- M6: p=>Mp
- M9: MMp=>Mp

[Zeman, 1973, p281]

OR (Feys)

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)