S5 (modal logic)
   HOME

TheInfoList



OR:

In
logic Logic is the study of correct reasoning. It includes both formal and informal logic. Formal logic is the science of deductively valid inferences or of logical truths. It is a formal science investigating how conclusions follow from premises ...
and
philosophy Philosophy (from , ) is the systematized study of general and fundamental questions, such as those about existence, reason, knowledge, values, mind, and language. Such questions are often posed as problems to be studied or resolved. Some ...
, S5 is one of five systems of
modal logic Modal logic is a collection of formal systems developed to represent statements about necessity and possibility. It plays a major role in philosophy of language, epistemology, metaphysics, and natural language semantics. Modal logics extend other ...
proposed by
Clarence Irving Lewis Clarence Irving Lewis (April 12, 1883 – February 3, 1964), usually cited as C. I. Lewis, was an American academic philosopher. He is considered the progenitor of modern modal logic and the founder of conceptual pragmatism. First a noted logic ...
and
Cooper Harold Langford Cooper Harold Langford (25 August 1895, Dublin, Logan County, Arkansas – 28 August 1964) was an American analytic philosopher and mathematical logician who co-authored the book ''Symbolic Logic'' (1932) with Clarence Irving Lewis, C. I. Lewis. H ...
in their 1932 book ''Symbolic Logic''. It is a
normal modal logic In logic, a normal modal logic is a set ''L'' of modal formulas such that ''L'' contains: * All propositional tautologies; * All instances of the Kripke schema: \Box(A\to B)\to(\Box A\to\Box B) and it is closed under: * Detachment rule (''modus po ...
, and one of the oldest systems of modal logic of any kind. It is formed with
propositional calculus Propositional calculus is a branch of logic. It is also called propositional logic, statement logic, sentential calculus, sentential logic, or sometimes zeroth-order logic. It deals with propositions (which can be true or false) and relations b ...
formulas and tautologies, and inference apparatus with
substitution Substitution may refer to: Arts and media *Chord substitution, in music, swapping one chord for a related one within a chord progression * Substitution (poetry), a variation in poetic scansion * "Substitution" (song), a 2009 song by Silversun Pi ...
and
modus ponens In propositional logic, ''modus ponens'' (; MP), also known as ''modus ponendo ponens'' (Latin for "method of putting by placing") or implication elimination or affirming the antecedent, is a deductive argument form and rule of inference. ...
, but extending the syntax with the
modal operator A modal connective (or modal operator) is a logical connective for modal logic. It is an operator which forms propositions from propositions. In general, a modal operator has the "formal" property of being non-truth-functional in the following sen ...
''necessarily'' \Box and its dual ''possibly'' \Diamond.


The axioms of S5

The following makes use of the modal operators \Box ("necessarily") and \Diamond ("possibly"). S5 is characterized by the axioms: *K: \Box(A\to B)\to(\Box A\to\Box B); *T: \Box A \to A, and either: * 5: \Diamond A\to \Box\Diamond A; * or both of the following: :* 4: \Box A\to\Box\Box A, and :* B: A\to\Box\Diamond A. The (5) axiom restricts the
accessibility relation An accessibility relation is a relation which plays a key role in assigning truth values to sentences in the relational semantics for modal logic. In relational semantics, a modal formula's truth value at a ''possible world'' w can depend on w ...
R of the
Kripke frame Kripke semantics (also known as relational semantics or frame semantics, and often confused with possible world semantics) is a formal semantics for non-classical logic systems created in the late 1950s and early 1960s by Saul Kripke and André Jo ...
to be Euclidean, i.e. (wRv \land wRu) \implies vRu .


Kripke semantics

In terms of
Kripke semantics Kripke semantics (also known as relational semantics or frame semantics, and often confused with possible world semantics) is a formal semantics for non-classical logic systems created in the late 1950s and early 1960s by Saul Kripke and André Jo ...
, S5 is characterized by models where the accessibility relation is an
equivalence relation In mathematics, an equivalence relation is a binary relation that is reflexive, symmetric and transitive. The equipollence relation between line segments in geometry is a common example of an equivalence relation. Each equivalence relation ...
: it is reflexive, transitive, and
symmetric Symmetry (from grc, συμμετρία "agreement in dimensions, due proportion, arrangement") in everyday language refers to a sense of harmonious and beautiful proportion and balance. In mathematics, "symmetry" has a more precise definiti ...
. Determining the satisfiability of an S5 formula is an
NP-complete In computational complexity theory, a problem is NP-complete when: # it is a problem for which the correctness of each solution can be verified quickly (namely, in polynomial time) and a brute-force search algorithm can find a solution by tryi ...
problem. The hardness proof is trivial, as S5 includes the
propositional logic Propositional calculus is a branch of logic. It is also called propositional logic, statement logic, sentential calculus, sentential logic, or sometimes zeroth-order logic. It deals with propositions (which can be true or false) and relations b ...
. Membership is proved by showing that any satisfiable formula has a Kripke model where the number of worlds is at most linear in the size of the formula.


Applications

S5 is useful because it avoids superfluous iteration of qualifiers of different kinds. For example, under S5, if ''X'' is necessarily, possibly, necessarily, possibly true, then ''X'' is possibly true. Unbolded qualifiers before the final "possibly" are pruned in S5. While this is useful for keeping propositions reasonably short, it also might appear counter-intuitive in that, under S5, if something is possibly necessary, then it is necessary.
Alvin Plantinga Alvin Carl Plantinga (born November 15, 1932) is an American analytic philosopher who works primarily in the fields of philosophy of religion, epistemology (particularly on issues involving epistemic justification), and logic. From 1963 to 1982, ...
has argued that this feature of S5 is not, in fact, counter-intuitive. To justify, he reasons that if ''X'' is ''possibly necessary'', it is necessary in at least one
possible world A possible world is a complete and consistent way the world is or could have been. Possible worlds are widely used as a formal device in logic, philosophy, and linguistics in order to provide a semantics for intensional logic, intensional and mod ...
; hence it is necessary in ''all'' possible worlds and thus is true in all possible worlds. Such reasoning underpins 'modal' formulations of the
ontological argument An ontological argument is a philosophical argument, made from an ontological basis, that is advanced in support of the existence of God. Such arguments tend to refer to the state of being or existing. More specifically, ontological arguments ...
. S5 is equivalent to the adjunction \Diamond\dashv\Box.
Leibniz Gottfried Wilhelm (von) Leibniz . ( – 14 November 1716) was a German polymath active as a mathematician, philosopher, scientist and diplomat. He is one of the most prominent figures in both the history of philosophy and the history of mathema ...
proposed an
ontological argument An ontological argument is a philosophical argument, made from an ontological basis, that is advanced in support of the existence of God. Such arguments tend to refer to the state of being or existing. More specifically, ontological arguments ...
for the existence of God using this axiom. In his words, "If a necessary being is possible, it follows that it exists actually". S5 is also the modal system for the metaphysics of saint
Thomas Aquinas Thomas Aquinas, OP (; it, Tommaso d'Aquino, lit=Thomas of Aquino; 1225 – 7 March 1274) was an Italian Dominican friar and priest who was an influential philosopher, theologian and jurist in the tradition of scholasticism; he is known wi ...
and in particular for the Five Ways.


See also

*
Modal logic Modal logic is a collection of formal systems developed to represent statements about necessity and possibility. It plays a major role in philosophy of language, epistemology, metaphysics, and natural language semantics. Modal logics extend other ...
*
Normal modal logic In logic, a normal modal logic is a set ''L'' of modal formulas such that ''L'' contains: * All propositional tautologies; * All instances of the Kripke schema: \Box(A\to B)\to(\Box A\to\Box B) and it is closed under: * Detachment rule (''modus po ...
*
Kripke semantics Kripke semantics (also known as relational semantics or frame semantics, and often confused with possible world semantics) is a formal semantics for non-classical logic systems created in the late 1950s and early 1960s by Saul Kripke and André Jo ...


References

{{Reflist


External links

* http://home.utah.edu/~nahaj/logic/structures/systems/s5.html
Modal Logic
at the Stanford Encyclopedia of Philosophy Modal logic