System S5 (Lewis)



If you univerally quantify each axiom of S5 [for example, if you convert Lp>p to forall(p,Lp>p) ] you DO NOT have S5, you have a DIFFERENT system (S5-UC)

Also known as system KTE

Also known as KT5 [Chellas, 1980, p139].

Also known as Kρσ [Priest, 2001, p39]

Becker's "Ten Modality Calculus" = S5 [Parry, 1953, p150]

Parry's S4.5 [Parry, 1953, p150] = S5 [Hughes and Cresswell, 1968, p264] [Zeman, 1973, p230]

S5* = S5 [Hughes and Cresswell, 1996, p344 (bottom)]

S5 is characterized by equivalence frames (reflexive, transitive, and symmetrical) [Hughes and Cresswell, 1996, p61]

In the same sense that IPC and S4 are related, Standard PC and S5 are related. [Zeman, 1973, 181] (Quoting [McKinsey and Tarski, 1948, p13] for the S4 part)

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

S5 = 2r (Pledger), and has distinct affirmative modalities as follows:

p   implied by Lp  it implies Mp

Lp                 it implies p, Mp
Mp                 implied by p, Lp

[Pledger, 1972, p270]

Diderik Batens and Joke Meheus present a non-standard (but acceptable) Semantic for S5 in their paper "The adaptive logic of compatibility." Studia Logica, volume 66 (2000), pages 327-348. [Each of their models corresponds to a standard worlds model, but not the other way around.]

Based on

The system S5 is the system S3 plus any of the [Pledger, 1972, p270]

LMLp  => LLp,  MMp => MLMp

LMMLp => {p, Lp, LLp},  {p, Mp, MMp} => MLLMp

{ MLLp, MLp, MLMMLp, MMLp } => { p, Lp, LLp }
{ p, Mp, MMp } => { LMMp, LMp, LMLLMp, LLMp }


The system S5 is the result of System T and the axiom 5 (Mp > LMp) [Hughes and Cresswell, 1996]

In other words, S5 is:


The system S5 is the standard rules plus the axioms:

[Hughes and Cresswell, 1996, p361 B]


The system S5 is the result of S3 and the axiom Mp=>~M~Mp [Simons, 1953] [Parry, 1939, p151]


The system S5 is the result of S3 + (MMp => ~M~MMp) [Or equivalently (MMp => LMMp) -jh] [Parry, 1939, p152]


The system S5 is the result of S3 and the axiom (~M~p=>Mp)=>(p=>~M~Mp) [Anderson, 1956]

OR (Feys)

The system S5 = System S1 plus the axiom M10: Mp => LMp [Feys, 1965, p115] [Hughes and Cresswell 1968, 237]

OR (Sobociński)

S5 = System S4 plus the axiom p => LMp [Feys, 1965, p119] (Quoting [Sobociński, 1962, ?])


The system S5 is the result of S10 plus the Axiom M10 Mp => LMp [Zeman, 1973, p281]

Or in other words, S5 is:


S5 is K sub L plus the definition: DN2: La == a&Ga&Ha [Rescher and Urquhart, 1971, p133]


[Anderson, 1956, p255]

Basis for

S5 + LMp>MLp = collapses to The trivial system [Hughes and Cresswell, 1996]

Go to ...

© Copyright 2007, by John Halleck, All Rights Reserved.
This page is
This page was last modified on July 8th, 2008