Why modal logic

This assigns to each atom either the value 1 true or the value 0 false at a world. The valuation function v is extended to the whole language via the following recursive clauses:. It also validates the Distribution principle or K-principle :. The logic induced by the semantics the set of valid sentences is called K , after Kripke. This is the weakest normal modal logic. Be careful in how you read this rule. If we impose some conditions on R , we obtain stronger normal modal logics.

The normal modal logics obtained in this way contain all the K -theorems, plus some extra ones too. In semantic terms, we get more entailments by putting further conditions on the accessibility relation R.

Table 4. The logic KTB adds the T and B axioms, for example, and so corresponds to to the reflexive and symmetrical frame. Corresponding to the serial and euclidean frame is the logic KD5. And so on. Whether we accept these additional axioms depends on how we understand the involved modalities. The D axiom says that what is necessary is possible, and this seems plausible on most readings of the notions of possibility and necessity.

Thus, D fails. If the relevant necessity is factive, then the T axiom must hold: if A is necessary at a given world w , then it should be true at that p. For without Reflexivity, it could be that A holds at all worlds accessible from w but not at w itself. If the relevant necessity is unrestricted, then the 4 and 5 axioms look very plausible. If A is unrestrictedly necessary or possible in the relevant sense, this fact should not be contingent on anything and so it should be necessary as well.

This may not be so for factive but restricted or relative necessities. Against 4, for instance, it might be physically necessary determined by the laws of physics that bodies do not accelerate through the speed of light; but its necessity may not be determined by the laws of physics. Lewis Lewis and Langford , a founding father of modern modal logic. It says that, if one knows that A , then one knows that one knows that A.

One has perfect introspective access to what one knows. It seems, however, that this has counterexamples. Think of yourself panicking the night before the exam, but doing fine with your essay the day after. The 5 axiom is even more suspect in an epistemic setting. As we shall see in Chapter 5 , it is indeed doubtful that any normal modal logic can provide an adequate formal treatment of epistemic notions like knowledge and belief.

This section expands on Berto and Jago Normal Kripke frames are celebrated for having provided suitable interpretations of different systems of modal logic, including S4 and S5. Kripke also introduced non-normal worlds Kripke , in order to provide world-based semantics for modal logics weaker than the basic normal modal system K. These are non-normal modal logics, including C.

For if A is a logical truth, then it is by definition true at all worlds of all models. Non-normal worlds enter the stage in order to make N fail. R is as before. In a sense, non-normal worlds of this kind are worlds where nothing is necessary and anything is possible. These worlds are deviant only in this respect: their behavior, as far as the extensional connectives are concerned, is quite regular.

A logical system for a language is a set of axioms and rules designed to prove exactly the valid arguments statable in the language. Creating such a logic may be a difficult task. The logician must make sure that the system is sound , i. Furthermore, the system should be complete , meaning that every valid argument has a proof in the system.

Such a demonstration cannot get underway until the concept of validity is defined rigorously. Formal semantics for a logic provides a definition of validity by characterizing the truth behavior of the sentences of the system. In propositional logic, validity can be defined using truth tables. A valid argument is simply one where every truth table row that makes its premises true also makes its conclusion true.

Nevertheless, semantics for modal logics can be defined by introducing possible worlds. Then we will explain how the same strategy may be adapted to other logics in the modal family.

Then the truth values of the complex sentences are calculated with truth tables. A definition of validity is now just around the corner. In deontic logic, temporal logic, and others, the analog of the truth condition 5 is clearly not appropriate; furthermore there are even conceptions of necessity where 5 should be rejected as well. The point is easiest to see in the case of temporal logic. Then the correct clause can be formulated as follows. Validity for this brand of temporal logic can now be defined.

One condition which is only mildly controversial is that there is no last moment of time, i. This condition on frames is called seriality. Density would be false if time were atomic, i. Each of the modal logic axioms we have discussed corresponds to a condition on frames in the same way.

The relationship between conditions on frames and corresponding axioms is one of the central topics in the study of modal logics. This, in turn, allows us to select the right set of axioms for that logic. Under such a reading, it should be clear that the relevant frames should obey seriality, the condition that requires that each possible world have a morally acceptable variant.

For example, I might say that it is necessary for me to pay my bills, even though I know full well that there is a possible world where I fail to pay them. Depending on exactly how the accessibility relation is understood, symmetry and transitivity may also be desired. A list of some of the more commonly discussed conditions on frames and their corresponding axioms along with a map showing the relationship between the various modal logics can be found in the next section.

A list of these and other axioms along with their corresponding frame conditions can be found below the diagram.

In this chart, systems are given by the list of their axioms. In boldface, we have indicated traditional names of some systems. The notion of correspondence between axioms and frame conditions that is at issue here was explained in the previous section. Several stronger notions of correspondence between axioms and frame conditions have emerged in research on modal logic.

The correspondence between axioms and conditions on frames may seem something of a mystery. A beautiful result of Lemmon and Scott goes a long way towards explaining those relationships. Their theorem concerned axioms which have the following form:. In order to do so, we will need a definition. A relation may be composed with itself. We may now state the Scott-Lemmon result. For example, consider 5. So the corresponding condition is. So the corresponding condition on frames is.

The Scott-Lemmon results provides a quick method for establishing results about the relationship between axioms and their corresponding frame conditions. Sahlqvist has discovered important generalizations of the Scott-Lemmon result covering a much wider range of axiom types.

The reader should be warned, however, that the neat correspondence between axioms and conditions on frames is atypical. There are condtions on frames that correspond to no axioms, and there are even conditions on frames for which no system is adequate. For an example see Boolos, , pp.

Two dimensional semantics is a variant of possible world semantics that uses two or more kinds of parameters in truth evaluation, rather than possible worlds alone. However, indexicals bring in a second dimension — so we need to generalize again.

Kaplan defines the character of a sentence B to be a function from the set of linguistic contexts to the content or intension of B, where the content, in turn, is simply the intension of B, that is a function from possible worlds to truth-values. Here, truth evaluation is doubly dependent — on both linguistic contexts and possible worlds. An example is 1. This suggests that the context dimension is apt for tracking analytic knowledge obtained from the mastery of our language.

On the other hand, the possible-worlds dimension keeps track of what is necessary. Holding the context fixed, there there are possible worlds where 1 is false. Therefore, two-dimensional semantics can handle situations where necessity and analyticity come apart. Another example where bringing in two dimension is useful is in the logic for an open future Thomason, ; Belnap, et al. Here one employs a temporal structure where many possible future histories extend from a given time.

Consider 2. If 2 is contingent, then there is a possible history where the battle occurs the day after the time of evaluation, and another one where it does not occur then. So to evaluate 2 you need to know two things: what is the time t of evaluation, and which of the histories h that run through t is the one to be considered.

So we would have the following truth condition:. Then the truth condition Now is revised to 2DNow. To properly evaluate 4 we need to keep track of which world is taken to be the actual or real world as well as which one is taken to the world of evaluation. The idea of distinguishing different possible world dimensions in semantics has had useful applications in philosophy. For example, Chalmers has presented arguments from the conceivability of say zombies to dualist conclusions in the philosophy of mind.

Chalmers has deployed two-dimensional semantics to help identify an a priori aspect of meaning that would support such conclusions.

The idea has also been deployed in the philosophy of language. On the other hand, there is a strong intuition that had the real world been somewhat different from what it is, the odorless liquid that falls from the sky as rain, fills our lakes and rivers, etc. So in some sense it is conceivable that water is not H Two dimensional semantics makes room for these intuitions by providing a separate dimension that tracks a conception of water that lays aside the chemical nature of what water actually is.

Modal logic has been useful in clarifying our understanding of central results concerning provability in the foundations of mathematics Boolos, Using this notation, sentences of provability logic express facts about provability.

Furthermore, the box may be iterated. In provability logic, provability is not to be treated as a brand of necessity. The applications of modal logic to mathematics and computer science have become increasingly important.

Provability logic is only one example of this trend. This tradition has been woven into the history of modal logic right from its beginnings Goldblatt, Research into relationships with topology and algebras represents some of the very first technical work on modal logic. Some examples of the many interesting topics dealt with include results on decidability whether it is possible to compute whether a formula of a given modal logic is a theorem and complexity the costs in time and memory needed to compute such facts about modal logics.

Bisimulation provides a good example of the fruitful interactions that have been developed between modal logic and computer science.

In computer science, labeled transition systems LTSs are commonly used to represent possible computation pathways during execution of a program. So ideas like the correctness and successful termination of programs can be expressed in this language. Models for such a language are like Kripke models save that LTSs are used in place of frames.

Bisimulation is a weaker notion than isomorphism a bisimulation relation need not be , but it is sufficient to guarantee equivalence in processing. In the s, a version of bisimulation had already been developed by modal logicians to help better understand the relationship between modal logic axioms and their corresponding conditions on Kripke frames.

Similar results hold for many other axioms and frame conditions. For example, this is the core idea behind the elegant results of Sahlqvist That result generalizes easily to the poly-modal case Blackburn et. This suggests that poly-modal logic lies at exactly the right level of abstraction to describe, and reason about, computation and other processes. After all, what really matters there is the preservation of truth values of formulas in models rather than the finer details of the frame structures.

Furthermore the implicit translation of those logics into well-understood fragments of predicate logic provides a wealth of information of interest to computer scientists. As a result, a fruitful area of research in computer science has developed with bisimulation as its core idea Ponse et al. The interaction between the theory of games and modal logic is a flourishing new area of research van der Hoek and Pauly, ; van Benthem, , Ch.

This work has interesting applications to understanding cooperation and competition among agents as information available to them evolves. Imagine two players that choose to either cooperate or cheat. If both cooperate, they both achieve a reward of 3 points, if they both cheat, they both get nothing, and if one cooperates and the other cheats, the cheater makes off with 5 points and the cooperator gets nothing. If both players are altruistic and motivated to maximize the sum of their rewards, they will both cooperate, as this is the best they can do together.

However, they are both tempted to cheat to increase their own reward from 3 to 5. On the other hand, if they are rational, they may recognize that if they cheat their opponent threatens to cheat and leave them with nothing. So cooperation is the best one can do given this threat. For a more comprehensive treatment, see chapter 5 of Blackburn, de Rijke, and Venema See also Goldblatt In the early s the recognition of the semantical nature of the notion of logical truth led Rudolf Carnap to an informal explication of this notion in terms of Leibnizian possible worlds.

At the same time, he recognized that the many syntactical advances in modal logic from on were still not accompanied by adequate semantic considerations. Carnap instead thought of necessity as logical truth or analyticity. The idea of quantified modal systems occurred to Ruth Barcan too. Though some specific semantic points about quantified modal logic will be considered, this entry is not focused on the development of quantified modal logic, but rather on the emergence of the model theoretic formal semantics for modal logic, propositional or quantified.

For a more extensive treatment of quantified modal logic, consult the SEP entry on modal logic. That is to say, the modal concept of the logical necessity of a proposition and the semantical concept of the logical truth or analyticity of a sentence correspond to each other. Carnap introduces the apparatus of state-descriptions to define the formal semantic notion of L -truth. This formal notion is then to be used to provide a formal semantics for S5.

An atomic sentence holds in a state-description R if and only if it belongs to R. The range of a sentence is the class of state-descriptions in which it holds. In later work Carnap adopts models in place of state-descriptions. Models are assignments of values to the primitive non-logical constants of the language. It is important to notice that the definition of L -truth does not employ the notion of truth, but rather only that of holding-in-a-state-description.

Truth is introduced later as what holds in the real state description. To be an adequate formal representation of analyticity, L -truth must respect the basic idea behind analyticity: truth in virtue of meaning alone. In fact, the L -truths of a system S are such that the semantic rules of S suffice to establish their truth. Informally, state-descriptions represent something like Leibnizian possible worlds or Wittgensteinian possible states of affairs and the range of state-descriptions for a certain language is supposed to exhaust the range of alternative possibilities describable in that language.

Let S be a system:. Carnap assumes a fixed domain of quantification for his quantified system, the functional calculus with identity FC , and consequently for the modal functional calculus with identity MFC , a quantified form of S5.

The language of FC contains denumerably many individual constants, the universe of discourse contains denumerably many individuals, each constant is assigned an individual of the domain, and no two constants are assigned the same individual. This result is guaranteed by the assumption of a fixed domain of quantification.

Carnap instead adopts one unique denumerable domain of quantification. A consequence of the definitions of state-descriptions for a language and L -truth is that each atomic sentence and its negation turn out to be true at some, but not all, state-descriptions.

The proof however effectively employs a schematic notion of validity. Given that the non-valid first-order sentences are not recursively enumerable, neither are the validities for the modal system MFC.

But the class of theorems of MFC is recursively enumerable. Cocchiarella b attributes the result to Richard Montague and Donald Kalish. Yet some crucial ingredients are still missing. First, the maximal notion of validity must be replaced by a new universal notion. Second, state-descriptions must make space for possible worlds understood as indices or points of evaluation.

Last, a relation of accessibility between worlds needs to be introduced. Kanger , Montague , but originally presented in , Hintikka , and Prior were all thinking of a relation between worlds, and Hintikka like Kripke a adopted a new notion of validity that required truth in all arbitrary sets of worlds. But Kripke was the only one to characterize the worlds as simple points of evaluation in a.

Other logicians were still thinking of the worlds fundamentally as models of first-order logic, though perhaps Prior in his development of temporal logic was also moving towards a more abstract characterization of instants of time. Kripke saw very clearly this connection between the algebra and the semantics, and this made it possible for him to obtain model theoretic completeness and decidability results for various modal systems in a systematic way.

Goldblatt section 4. Such a generalization opens the door to different future developments of the model theory and makes it possible to provide model theories for intensional logics in general. For a more comprehensive treatment of the initial development of PWS, including the late fifties work on S5 of the French logician Bayart, the reader is referred to Goldblatt The most important thing to be noticed in the model theory is the definition of validity.

Kripke says:. In trying to construct a definition of universal logical validity, it seems plausible to assume not only that the universe of discourse may contain an arbitrary number of elements and that predicates may be assigned any given interpretations in the actual world, but also that any combination of possible worlds may be associated with the real world with respect to some group of predicates.

This assumption leads directly to our definition of universal validity. So far the only significant divergence from Carnap is that different Kripke models can have domains of different cardinality.

This by itself is sufficient to reintroduce completeness for the non-modal part of the system. But the most significant development, and the one that makes it possible to prove completeness for the modal system, is the definition of validity not as truth in all worlds of a maximal structure of worlds, but as truth across all the subsets of the maximal structure. While necessities are relative to a model, hence to a set of worlds, validities must hold across all such sets.

This permits the reintroduction of the rule of Uniform Substitution. If we only consider this complete truth table, we are only considering maximal models that contain two worlds it makes no difference which world is actual. If instead we define validity as Kripke does, we have to consider also the non-maximal models that contain only one world, that is, incomplete truth-tables that cancel some rows. Notice that the crucial innovation is the definition of validity as truth across all subsets of worlds, not just the maximal subset.

The additional fact that validity in a model is defined as truth at the actual world of the model—as opposed to truth at all worlds of the model—though revealing of the fact that Kripke did not link the notion of necessity to the notion of validity, is irrelevant to this technical result.

A main tableau and its auxiliary tableaux form a set of tableaux. So we have to consider alternative sets of tableaux.

A semantic tableau is closed if and only if all its alternative sets are closed. This last result is achieved by showing how to build models from semantic tableaux. It is in this paper that the two additional crucial generalizations of the model theory are introduced.

Hence, while in the model theory. Let it be emphasized once again that the idea of a relation between worlds is not new to Kripke. For example, it is already present as an alternativeness relation in Montague , Hintikka , and Prior , where the idea is attributed to Peter Geach.

First, he shows that every satisfiable formula has a connected model, i. Hence, only connected models need to be considered. The decidability of these systems, including the more complex case of S4 , is also proved. For a more detailed treatment of frames, consult the SEP entry on modal logic.

Though these systems are considered somewhat unnatural, their model theory is deemed elegant. This is required as the systems under consideration do not have a full rule of necessitation. The great success of the Kripkean model theory notwithstanding, it is worth emphasizing that not all modal logics are complete. For incompleteness results see Makinson , for a system weaker than S4 ; and Fine , S. Thomason , Goldblatt , and van Benthem , for systems between S4 and S5.

Some modal formulas impose conditions on frames that cannot be expressed in a first-order language, thus even propositional modal logic is fundamentally second-order in nature. Insofar as the notion of validity on a frame abstracts from the interpretation function, it implicitly involves a higher-order quantification over propositions. As a result all worlds in one model had the same cardinality.

Given the variability of domains across worlds, Kripke can now construct counter-examples both to the Barcan Formula. The Barcan formula can be falsified in structures with growing domains. To disprove the converse of the Barcan formula we need models with decreasing domains. Kripke points out that from a model theoretical point of view this is just a technical choice. Kripke reconstructs a proof of the converse Barcan formula in quantified T and shows that the proof goes through only by allowing the necessitation of a sentence containing a free variable.

But if free variables are instead to be considered as universally bound, this step is illicit. Necessitating directly an open formula, without first closing it, amounts to assuming what is to be proved.