Modal logic


Modal logic is a collection of formal systems originally developed and still widely used to represent statements about necessity and possibility. For instance, the modal formula can be read as "if P is necessary, then it is also possible". This formula is widely regarded as valid when necessity and possibility are understood with respect to knowledge, as in epistemic modal logic. Whether it is also valid with legal or moral necessity is a question debated since Sophocles' play Antigone.
The first modal axiomatic systems were developed by C. I. Lewis in 1910, building on an informal tradition stretching back to Aristotle. The relational semantics for modal logic was developed by Arthur Prior, Jaakko Hintikka, and Saul Kripke in the mid twentieth century. In this semantics, formulas are assigned truth values relative to a possible world. A formula's truth value at one possible world can depend on the truth values of other formulas at other accessible possible worlds. In particular, possibility amounts to truth at some accessible possible world while necessity amounts to truth at every accessible possible world.
Modal logic is often referred to as "the logic of necessity and possibility", and such applications continue to play a major role in philosophy of language, epistemology, metaphysics, and formal semantics. However, the mathematical apparatus of modal logic has proved useful in numerous other fields including game theory, program verification, web design, multiverse-based set theory, and social epistemology. One prominent textbook on the model theory of modal logic suggests that it can be seen more generally as the study of formal systems which take a local perspective on relational structures.

Overview

A modal—a word that expresses a modality—qualifies a statement. For example, the statement "John is happy" might be qualified by saying that John is usually happy, in which case the term "usually" is functioning as a modal. The traditional alethic modalities, or modalities of truth, include possibility, necessity, and impossibility. Other modalities that have been formalized in modal logic include temporal modalities, or modalities of time, deontic modalities, epistemic modalities, or modalities of knowledge and doxastic modalities, or modalities of belief.
A formal modal logic represents modalities using modal operators. For example, "It might rain today" and "It is possible that rain will fall today" both contain the notion of possibility. In a modal logic this is represented as an operator, "Possibly", attached to the sentence "It will rain today".
The basic unary modal operators are usually written "□" for "Necessarily" and "◇" for "Possibly". Following the example above, if is to represent the statement of "it will rain today", the possibility of rain would be represented by. This reads: It is possible that it will rain today. Similarly reads: It is necessary that it will rain today, expressing certainty regarding the statement.
In a classical modal logic, each can be expressed by the other with negation.
In natural language, this reads: it is possible that it will rain today if and only if it is not necessary that it will not rain today. Similarly, necessity can be expressed in terms of possibility in the following negation:
which states it is necessary that it will rain today if and only if it is not possible that it will not rain today. Alternative symbols used for the modal operators are "L" for "Necessarily" and "M" for "Possibly".

Development of modal logic

In addition to his non-modal syllogistic, Aristotle also developed a modal syllogistic in Book I of his Prior Analytics, which Theophrastus attempted to improve. There are also passages in Aristotle's work, such as the famous sea-battle argument in De Interpretatione §9, that are now seen as anticipations of the connection of modal logic with potentiality and time. In the Hellenistic period, the logicians Diodorus Cronus, Philo the Dialectician and the Stoic Chrysippus each developed a modal system that accounted for the interdefinability of possibility and necessity, accepted axiom T, and combined elements of modal logic and temporal logic in attempts to solve the notorious Master Argument. The earliest formal system of modal logic was developed by Avicenna, who ultimately developed a theory of "temporally modal" syllogistic. Modal logic as a self-aware subject owes much to the writings of the Scholastics, in particular William of Ockham and John Duns Scotus, who reasoned informally in a modal manner, mainly to analyze statements about essence and accident.
C. I. Lewis founded modern modal logic in his 1910 Harvard thesis and in a series of scholarly articles beginning in 1912. This work culminated in his 1932 book Symbolic Logic, which introduced the five systems S1 through S5.
After Lewis, modal logic received little attention for several decades. Nicholas Rescher has argued that this was because Bertrand Russell rejected it. However, Jan Dejnozka has argued against this view, stating that a modal system which Dejnozka calls "MDL" is described in Russell's works, although Russell did believe the concept of modality to "come from confusing propositions with propositional functions," as he wrote in The Analysis of Matter.
Arthur Norman Prior warned Ruth Barcan Marcus to prepare well in the debates concerning quantified modal logic with Willard Van Orman Quine, due to the biases against modal logic.
Ruth C. Barcan developed the first axiomatic systems of quantified modal logic — first and second order extensions of Lewis' S2, S4, and S5.
The contemporary era in modal semantics began in 1959, when Saul Kripke introduced the now-standard Kripke semantics for modal logics. These are commonly referred to as "possible worlds" semantics. Kripke and A. N. Prior had previously corresponded at some length. Kripke semantics is basically simple, but proofs are eased using semantic-tableaux or analytic tableaux, as explained by E. W. Beth.
A. N. Prior created modern temporal logic, closely related to modal logic, in 1957 by adding modal operators and meaning "eventually" and "previously". Vaughan Pratt introduced dynamic logic in 1976. In 1977, Amir Pnueli proposed using temporal logic to formalise the behaviour of continually operating concurrent programs. Flavors of temporal logic include propositional dynamic logic, propositional linear temporal logic, linear temporal logic, computation tree logic, Hennessy–Milner logic, and T.
The mathematical structure of modal logic, namely Boolean algebras augmented with unary operations, began to emerge with J. C. C. McKinsey's 1941 proof that S2 and S4 are decidable, and reached full flower in the work of Alfred Tarski and his student Bjarni Jónsson. This work revealed that S4 and S5 are models of interior algebra, a proper extension of Boolean algebra originally designed to capture the properties of the interior and closure operators of topology. Texts on modal logic typically do little more than mention its connections with the study of Boolean algebras and topology. For a thorough survey of the history of formal modal logic and of the associated mathematics, see Robert Goldblatt.

Semantics

The semantics for modal logic are usually given as follows: First we define a frame, which consists of a non-empty set, G, whose members are generally called possible worlds, and a binary relation, R, that holds between the possible worlds of G. This binary relation is called the accessibility relation. For example, w R u means that the world u is accessible from world w. That is to say, the state of affairs known as u is a live possibility for w. This gives a pair,. Some formulations of modal logic also include a constant term in G, conventionally called "the actual world", which is often symbolized as.
Next, the frame is extended to a model by specifying the truth-values of all propositions at each of the worlds in G. We do so by defining a relation v between possible worlds and positive literals. If there is a world w such that, then P is true at w. A model is thus an ordered triple,.
Then we recursively define the truth of a formula at a world in a model:
According to these semantics, a truth is necessary with respect to a possible world w if it is true at every world that is accessible to w, and possible if it is true at some world that is accessible to w. Possibility thereby depends upon the accessibility relation R, which allows us to express the relative nature of possibility. For example, we might say that given our laws of physics it is not possible for humans to travel faster than the speed of light, but that given other circumstances it could have been possible to do so. Using the accessibility relation we can translate this scenario as follows: At all of the worlds accessible to our own world, it is not the case that humans can travel faster than the speed of light, but at one of these accessible worlds there is another world accessible from those worlds but not accessible from our own at which humans can travel faster than the speed of light.
It should also be noted that the definition of □ makes vacuously true certain sentences, since when it speaks of "every world that is accessible to w" it takes for granted the usual mathematical interpretation of the word "every". Hence, if a world w doesn't have any accessible worlds, any sentence beginning with □ is true.
The different systems of modal logic are distinguished by the properties of their corresponding accessibility relations. There are several systems that have been espoused. An accessibility relation is called:
The logics that stem from these frame conditions are:
The Euclidean property along with reflexivity yields symmetry and transitivity. Hence if the accessibility relation R is reflexive and Euclidean, R is provably symmetric and transitive as well. Hence for models of S5, R is an equivalence relation, because R is reflexive, symmetric and transitive.
We can prove that these frames produce the same set of valid sentences as do the frames where all worlds can see all other worlds of W. This gives the corresponding modal graph which is total complete. For example, in any modal logic based on frame conditions:
If we consider frames based on the total relation we can just say that
We can drop the accessibility clause from the latter stipulation because in such total frames it is trivially true of all w and u that w R u. But note that this does not have to be the case in all S5 frames, which can still consist of multiple parts that are fully connected among themselves but still disconnected from each other.
All of these logical systems can also be defined axiomatically, as is shown in the next section. For example, in S5, the axioms, and hold, whereas at least one of these axioms does not hold in each of the other, weaker logics.

Axiomatic systems

The first formalizations of modal logic were axiomatic. Numerous variations with very different properties have been proposed since C. I. Lewis began working in the area in 1910. Hughes and Cresswell, for example, describe 42 normal and 25 non-normal modal logics. Zeman describes some systems Hughes and Cresswell omit.
Modern treatments of modal logic begin by augmenting the propositional calculus with two unary operations, one denoting "necessity" and the other "possibility". The notation of C. I. Lewis, much employed since, denotes "necessarily p" by a prefixed "box" whose scope is established by parentheses. Likewise, a prefixed "diamond" denotes "possibly p". Regardless of notation, each of these operators is definable in terms of the other in classical modal logic:
Hence □ and ◇ form a dual pair of operators.
In many modal logics, the necessity and possibility operators satisfy the following analogues of de Morgan's laws from Boolean algebra:
Precisely what axioms and rules must be added to the propositional calculus to create a usable system of modal logic is a matter of philosophical opinion, often driven by the theorems one wishes to prove; or, in computer science, it is a matter of what sort of computational or deductive system one wishes to model. Many modal logics, known collectively as normal modal logics, include the following rule and axiom:
The weakest normal modal logic, named "K" in honor of Saul Kripke, is simply the propositional calculus augmented by □, the rule N, and the axiom K. K is weak in that it fails to determine whether a proposition can be necessary but only contingently necessary. That is, it is not a theorem of K that if □p is true then □□p is true, i.e., that necessary truths are "necessarily necessary". If such perplexities are deemed forced and artificial, this defect of K is not a great one. In any case, different answers to such questions yield different systems of modal logic.
Adding axioms to K gives rise to other well-known modal systems. One cannot prove in K that if "p is necessary" then p is true. The axiom T remedies this defect:
T holds in most but not all modal logics. Zeman describes a few exceptions, such as S10.
Other well-known elementary axioms are:
These yield the systems :
K through S5 form a nested hierarchy of systems, making up the core of normal modal logic. But specific rules or sets of rules may be appropriate for specific systems. For example, in deontic logic, seems appropriate, but we should probably not include that. In fact, to do so is to commit the naturalistic fallacy.
The commonly employed system S5 simply makes all modal truths necessary. For example, if p is possible, then it is "necessary" that p is possible. Also, if p is necessary, then it is necessary that p is necessary. Other systems of modal logic have been formulated, in part because S5 does not describe every kind of modality of interest.

Structural proof theory

and systems of natural deduction have been developed for several modal logics, but it has proven hard to combine generality with other features expected of good structural proof theories, such as purity and analyticity. More complex calculi have been applied to modal logic to achieve generality.

Decision methods

provide the most popular decision method for modal logics.

Modal logics in philosophy

Alethic logic

Modalities of necessity and possibility are called alethic modalities. They are also sometimes called special modalities, from the Latin species. Modal logic was first developed to deal with these concepts, and only afterward was extended to others. For this reason, or perhaps for their familiarity and simplicity, necessity and possibility are often casually treated as the subject matter of modal logic. Moreover, it is easier to make sense of relativizing necessity, e.g. to legal, physical, nomological, epistemic, and so on, than it is to make sense of relativizing other notions.
In classical modal logic, a proposition is said to be
In classical modal logic, therefore, the notion of either possibility or necessity may be taken to be basic, where these other notions are defined in terms of it in the manner of De Morgan duality. Intuitionistic modal logic treats possibility and necessity as not perfectly symmetric.
For example, suppose that while walking to the convenience store we pass Friedrich's house, and observe that the lights are off. On the way back, we observe that they have been turned on.
For those with difficulty with the concept of something being possible but not true, the meaning of these terms may be made more comprehensible by thinking of multiple "possible worlds" or "alternate universes"; something "necessary" is true in all possible worlds, something "possible" is true in at least one possible world. These "possible world semantics" are formalized with Kripke semantics.

Physical possibility

Something is physically, or nomically, possible if it is permitted by the laws of physics. For example, current theory is thought to allow for there to be an atom with an atomic number of 126, even if there are no such atoms in existence. In contrast, while it is logically possible to accelerate beyond the speed of light, modern science stipulates that it is not physically possible for material particles or information.

Metaphysical possibility

debate if objects have properties independent of those dictated by scientific laws. For example, it might be metaphysically necessary, as some who advocate physicalism have thought, that all thinking beings have bodies and can experience the passage of time. Saul Kripke has argued that every person necessarily has the parents they do have: anyone with different parents would not be the same person.
Metaphysical possibility has been thought to be more restricting than bare logical possibility. However, its exact relation to logical possibility or to physical possibility is a matter of dispute. Philosophers also disagree over whether metaphysical truths are necessary merely "by definition", or whether they reflect some underlying deep facts about the world, or something else entirely.

Epistemic logic

Epistemic modalities, deal with the certainty of sentences. The □ operator is translated as "x knows that…", and the ◇ operator is translated as "For all x knows, it may be true that…" In ordinary speech both metaphysical and epistemic modalities are often expressed in similar words; the following contrasts may help:
A person, Jones, might reasonably say both: "No, it is not possible that Bigfoot exists; I am quite certain of that"; and, "Sure, it's possible that Bigfoots could exist". What Jones means by is that, given all the available information, there is no question remaining as to whether Bigfoot exists. This is an epistemic claim. By he makes the metaphysical claim that it is possible for Bigfoot to exist, even though he does not: there is no physical or biological reason that large, featherless, bipedal creatures with thick hair could not exist in the forests of North America. Similarly, "it is possible for the person reading this sentence to be fourteen feet tall and named Chad" is metaphysically true, but not alethically true unless you match that description, and not epistemically true if it's known that fourteen-foot-tall human beings have never existed.
From the other direction, Jones might say, "It is possible that Goldbach's conjecture is true; but also possible that it is false", and also "if it is true, then it is necessarily true, and not possibly false". Here Jones means that it is epistemically possible that it is true or false, for all he knows, but if there is a proof, then it would show that it is not logically possible for Goldbach's conjecture to be false—there could be no set of numbers that violated it. Logical possibility is a form of alethic possibility; makes a claim about whether it is possible that a mathematical truth to have been false, but only makes a claim about whether it is possible, for all Jones knows, that the mathematical claim is specifically either true or false, and so again Jones does not contradict himself. It is worthwhile to observe that Jones is not necessarily correct: It is possible that Goldbach's conjecture is both true and unprovable.
Epistemic possibilities also bear on the actual world in a way that metaphysical possibilities do not. Metaphysical possibilities bear on ways the world might have been, but epistemic possibilities bear on the way the world may be. Suppose, for example, that I want to know whether or not to take an umbrella before I leave. If you tell me "it is possible that it is raining outside" – in the sense of epistemic possibility – then that would weigh on whether or not I take the umbrella. But if you just tell me that "it is possible for it to rain outside" – in the sense of metaphysical possibility – then I am no better off for this bit of modal enlightenment.
Some features of epistemic modal logic are in debate. For example, if x knows that p, does x know that it knows that p? That is to say, should □P → □□P be an axiom in these systems? While the answer to this question is unclear, there is at least one axiom that is generally included in epistemic modal logic, because it is minimally true of all normal modal logics :
It has been questioned whether the epistemic and alethic modalities should be considered distinct from each other. The criticism states that there is no real difference between "the truth in the world" and "the truth in an individual's mind". An investigation has not found a single language in which alethic and epistemic modalities are formally distinguished, as by the means of a grammatical mood.

Temporal logic

Temporal logic is an approach to the semantics of expressions with tense, that is, expressions with qualifications of when. Some expressions, such as '2 + 2 = 4', are true at all times, while tensed expressions such as 'John is happy' are only true sometimes.
In temporal logic, tense constructions are treated in terms of modalities, where a standard method for formalizing talk of time is to use two pairs of operators, one for the past and one for the future. For example:
There are then at least three modal logics that we can develop. For example, we can stipulate that,
Or we can trade these operators to deal only with the future. For example,
or,
The operators F and G may seem initially foreign, but they create normal modal systems. Note that FP is the same as ¬G¬P. We can combine the above operators to form complex statements. For example, PP → □PP says, Everything that is past and true is necessary.
It seems reasonable to say that possibly it will rain tomorrow, and possibly it won't; on the other hand, since we can't change the past, if it is true that it rained yesterday, it probably isn't true that it may not have rained yesterday. It seems the past is "fixed", or necessary, in a way the future is not. This is sometimes referred to as accidental necessity. But if the past is "fixed", and everything that is in the future will eventually be in the past, then it seems plausible to say that future events are necessary too.
Similarly, the problem of future contingents considers the semantics of assertions about the future: is either of the propositions 'There will be a sea battle tomorrow', or 'There will not be a sea battle tomorrow' now true? Considering this thesis led Aristotle to reject the principle of bivalence for assertions concerning the future.
Additional binary operators are also relevant to temporal logics, q.v. Linear Temporal Logic.
Versions of temporal logic can be used in computer science to model computer operations and prove theorems about them. In one version, ◇P means "at a future time in the computation it is possible that the computer state will be such that P is true"; □P means "at all future times in the computation P will be true". In another version, ◇P means "at the immediate next state of the computation, P might be true"; □P means "at the immediate next state of the computation, P will be true". These differ in the choice of Accessibility relation. These two examples involve nondeterministic or not-fully-understood computations; there are many other modal logics specialized to different types of program analysis. Each one naturally leads to slightly different axioms.

Deontic logic

Likewise talk of morality, or of obligation and norms generally, seems to have a modal structure. The difference between "You must do this" and "You may do this" looks a lot like the difference between "This is necessary" and "This is possible". Such logics are called deontic, from the Greek for "duty".
Deontic logics commonly lack the axiom T semantically corresponding to the reflexivity of the accessibility relation in Kripke semantics: in symbols,. Interpreting □ as "it is obligatory that", T informally says that every obligation is true. For example, if it is obligatory not to kill others, then T implies that people actually do not kill others. The consequent is obviously false.
Instead, using Kripke semantics, we say that though our own world does not realize all obligations, the worlds accessible to it do. These worlds are called idealized worlds. P is obligatory with respect to our own world if at all idealized worlds accessible to our world, P holds. Though this was one of the first interpretations of the formal semantics, it has recently come under criticism.
One other principle that is often accepted as a deontic principle is D,, which corresponds to the seriality of the accessibility relation. It is an embodiment of the Kantian idea that "ought implies can".

Intuitive problems with deontic logic

When we try to formalize ethics with standard modal logic, we run into some problems. Suppose that we have a proposition K: you have stolen some money, and another, Q: you have stolen a small amount of money. Now suppose we want to express the thought that "if you have stolen some money, it ought to be a small amount of money". There are two likely candidates,
But and K together entail □Q, which says that it ought to be the case that you have stolen a small amount of money. This surely isn't right, because you ought not to have stolen anything at all. And doesn't work either: If the right representation of "if you have stolen some money it ought to be a small amount" is, then the right representation of "if you have stolen some money then it ought to be a large amount" is. Now suppose that you ought not to steal anything, or. But then we can deduce via and ; so sentence follows from our hypothesis. But that can't be right, and is not right when we use natural language. Telling someone they should not steal certainly does not imply that they should steal large amounts of money if they do engage in theft.

Doxastic logic

Doxastic logic concerns the logic of belief. The term doxastic is derived from the ancient Greek doxa which means "belief". Typically, a doxastic logic uses □, often written "B", to mean "It is believed that", or when relativized to a particular agent s, "It is believed by s that".

Metaphysical questions

In the most common interpretation of modal logic, one considers "logically possible worlds". If a statement is true in all possible worlds, then it is a necessary truth. If a statement happens to be true in our world, but is not true in all possible worlds, then it is a contingent truth. A statement that is true in some possible world is called a possible truth.
Under this "possible worlds idiom," to maintain that Bigfoot's existence is possible but not actual, one says, "There is some possible world in which Bigfoot exists; but in the actual world, Bigfoot does not exist". However, it is unclear what this claim commits us to. Are we really alleging the existence of possible worlds, every bit as real as our actual world, just not actual? Saul Kripke believes that 'possible world' is something of a misnomer – that the term 'possible world' is just a useful way of visualizing the concept of possibility. For him, the sentences "you could have rolled a 4 instead of a 6" and "there is a possible world where you rolled a 4, but you rolled a 6 in the actual world" are not significantly different statements, and neither commit us to the existence of a possible world. David Lewis, on the other hand, made himself notorious by biting the bullet, asserting that all merely possible worlds are as real as our own, and that what distinguishes our world as actual is simply that it is indeed our world – this world. That position is a major tenet of "modal realism". Some philosophers decline to endorse any version of modal realism, considering it ontologically extravagant, and prefer to seek various ways to paraphrase away these ontological commitments. Robert Adams holds that 'possible worlds' are better thought of as 'world-stories', or consistent sets of propositions. Thus, it is possible that you rolled a 4 if such a state of affairs can be described coherently.
Computer scientists will generally pick a highly specific interpretation of the modal operators specialized to the particular sort of computation being analysed. In place of "all worlds", you may have "all possible next states of the computer", or "all possible future states of the computer".

Further applications

Modal logics have begun to be used in areas of the humanities such as literature, poetry, art and history.