System S5 (Lewis)

References:

[Anderson 1956]
[Hughes and Cresswell, 1996]
[Lewis and Langford, 1932] (Original source)
[Simons, 1953]
[Zeman, 1973]

Notes

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 }

OR

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

In other words, S5 is:

PC Including:
- Rule: Modus Ponens
- Rule: Uniform substitution
Including
- Definition: Mp == ~L~p
- Necessitation: From |- p infer |- Lp
- Axiom K: L(p>q) > (Lp>Lq)
- Axiom T: Lp > p
Axioms
- Axiom 5: Mp > LMp

OR

The system S5 is the standard rules plus the axioms:

K: L(p>q)>(Lp>Lq)
T: Lp>p
B: p>LMp
4: Lp>LLp

[Hughes and Cresswell, 1996, p361 B]

OR

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

OR

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

OR

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, ?])

OR

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

Or in other words, S5 is:

Definitions
- Lp def ~M~p
Rules
- Uniform substitution (US)
- Strict detachment (MP=>)
- Adjunction (given a, b, return a&b) (AD)
- substitution of strict equivalents. (EQS)
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)
- M10: Mp=>LMp

OR

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

OR

Definitions
- Standard definitions for operators not in axioms.
Rules
- Uniform Substitution (Actually, Anderson presented axiom schemata instead of axioms, and therefore didn't need uniform substitution)
- Material Detachment: From |- p and |- p > q infer |- q
Axioms
- HA1: p => (p&p)
- HA2: (p&q) => p
- HA3: ((r&p)&~(q&r)) => (p&~q)
- HA4: ~Mp => ~p
- HA5: p => Mp
- HA6: (p=>q) => (~Mq=>~Mp)
- S: (~M~a => Ma) => (a => ~M~Ma)

[Anderson, 1956, p255]

Basis for

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