References:

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

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

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

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:

- 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

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]

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

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

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

Or in other words, S5 is:

- Definitions
- Lp def ~M~p

- Rules
- 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

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

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

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

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

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

This page was last modified on July 8th, 2008