Modal logic is a kind oflogic used to represent statements aboutnecessity and possibility. Inphilosophy and related fieldsit is used as a tool for understanding concepts such asknowledge,obligation, andcausation. For instance, inepistemic modal logic, theformula can be used to represent the statement that is known. Indeontic modal logic, that same formula can represent that is a moral obligation. Modal logic considers the inferences that modal statements give rise to. For instance, most epistemic modal logics treat the formula as atautology, representing the principle that only true statements can count as knowledge. However, this formula is not a tautology in deontic modal logic, since what ought to be true can be false.
Modal logics areformal systems that includeunary operators such as and, representing possibility and necessity respectively. For instance the modal formula can be read as "possibly" while can be read as "necessarily". In the standardrelational semantics for modal logic, formulas are assigned truth values relative to apossible world. A formula's truth value at one possible world can depend on the truth values of other formulas at otheraccessiblepossible worlds. In particular, is true at a world if is true atsome accessible possible world, while is true at a world if is true atevery accessible possible world. A variety of proof systems exist which are sound and complete with respect to the semantics one gets by restricting the accessibility relation. For instance, the deontic modal logicD is sound and complete if one requires the accessibility relation to beserial.
While the intuition behind modal logic dates back to antiquity, the first modalaxiomatic systems were developed byC. I. Lewis in 1912. The now-standard relational semantics emerged in the mid twentieth century from work byArthur Prior,Jaakko Hintikka, andSaul Kripke. Recent developments include alternativetopological semantics such asneighborhood semantics as well as applications of the relational semantics beyond its original philosophical motivation.[1] Such applications includegame theory,[2]moral andlegal theory,[2]web design,[2]multiverse-based set theory,[3] andsocial epistemology.[4]
Modal logic differs from other kinds of logic in that it uses modaloperators such as and. The former is conventionally read aloud as "necessarily", and can be used to represent notions such as moral or legalobligation,knowledge,historical inevitability, among others. The latter is typically read as "possibly" and can be used to represent notions includingpermission,ability, compatibility withevidence. Whilewell-formed formulas of modal logic include non-modal formulas such as, it also contains modal ones such as,,, and so on.
Thus, thelanguage of basicpropositional logic can bedefined recursively as follows.
Modal operators can be added to other kinds of logic by introducing rules analogous to #4 and #5 above. Modalpredicate logic is one widely used variant which includes formulas such as. In systems of modal logic where and areduals, can be taken as an abbreviation for, thus eliminating the need for a separate syntactic rule to introduce it. However, separate syntactic rules are necessary in systems where the two operators are not interdefinable.
Common notational variants include symbols such as and in systems of modal logic used to represent knowledge and and in those used to represent belief. These notations are particularly common in systems which use multiple modal operators simultaneously (multi-modal logic). For instance, a combined epistemic-deontic logic could use the formula read as "I know P is permitted". Systems of modal logic can include infinitely many modal operators distinguished by indices, i.e.,,, and so on.
The standard semantics for modal logic is called therelational semantics. In this approach, the truth of a formula is determined relative to a point which is often called apossible world. For a formula that contains a modal operator, its truth value can depend on what is true at otheraccessible worlds. Thus, the relational semantics interprets formulas of modal logic usingmodels defined as follows.[5]
The set is often called theuniverse. The binary relation is called anaccessibility relation, and it controls which worlds can "see" each other for the sake of determining what is true. For example, means that the world is accessible from world. That is to say, thestate of affairs known as is a live possibility for. Finally, the function is known as avaluation function. It determines whichatomic formulas are true at which worlds.
Then we recursively define the truth of a formula at a world in a model:
According to this semantics, a formula isnecessary with respect to a world if it holds at every world that is accessible from. It ispossible if it holds at some world that is accessible from. Possibility thereby depends upon the accessibility relation, 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 cantranslate 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 isanother world accessible fromthose worlds but not accessible from our own at which humans can travel faster than the speed of light.
The choice of accessibility relation alone can sometimes be sufficient to guarantee the truth or falsity of a formula. For instance, consider a model whose accessibility relation isreflexive. Because the relation is reflexive, we will have that for any regardless of which valuation function is used. For this reason, modal logicians sometimes talk aboutframes, which are the portion of a relational model excluding the valuation function.
The different systems of modal logic are defined usingframe conditions. A frame is called:
The logics that system from these frame conditions are:
The Euclidean property along with reflexivity yields symmetry and transitivity. (The Euclidean property can be obtained, as well, from symmetry and transitivity.) Hence if the accessibility relationR is reflexive and Euclidean,R is provablysymmetric andtransitive as well. Hence for models of S5,R is anequivalence relation, becauseR 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 ofW (i.e., whereR is a "total" relation). This gives the correspondingmodal graph which is total complete (i.e., no more edges (relations) can be added). 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 allw andu thatw R u. But 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 (corresponding tosymmetry,transitivity andreflexivity, respectively) hold, whereas at least one of these axioms does not hold in each of the other, weaker logics.
Modal logic has also been interpreted using topological structures. For instance, theInterior Semantics interprets formulas of modal logic as follows.
Atopological model is a tuple where is atopological space and is a valuation function which maps each atomic formula to some subset of. The basic interior semantics interprets formulas of modal logic as follows:
Topological approaches subsume relational ones, allowingnon-normal modal logics. The extra structure they provide also allows a transparent way of modeling certain concepts such as the evidence or justification one has for one's beliefs. Topological semantics is widely used in recent work in formal epistemology and has antecedents in earlier work such asDavid Lewis andAngelika Kratzer's logics forcounterfactuals.

The first formalizations of modal logic wereaxiomatic. Numerous variations with very different properties have been proposed sinceC. I. Lewis began working in the area in 1912.Hughes andCresswell (1996), for example, describe 42normal and 25 non-normal modal logics. Zeman (1973) describes some systems Hughes and Cresswell omit.
Modern treatments of modal logic begin by augmenting thepropositional calculus with two unary operations, one denoting "necessity" and the other "possibility". The notation ofC. I. Lewis, much employed since, denotes "necessarilyp" by a prefixed "box" (□p) whosescope is established by parentheses. Likewise, a prefixed "diamond" (◇p) denotes "possiblyp". Similar to thequantifiers infirst-order logic, "necessarilyp" (□p) does not assume therange of quantification (the set of accessible possible worlds inKripke semantics) to be non-empty, whereas "possiblyp" (◇p) often implicitly assumes (viz. the set of accessible possible worlds is non-empty). Regardless of notation, each of these operators is definable in terms of the other in classical modal logic:
Hence □ and ◇ form adual pair of operators.
In many modal logics, the necessity and possibility operators satisfy the following analogues ofde Morgan's laws fromBoolean algebra:
Precisely what axioms and rules must be added to thepropositional 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 asnormal modal logics, include the following rule and axiom:
The weakestnormal modal logic, named "K" in honor ofSaul Kripke, is simply thepropositional calculus augmented by □, the ruleN, and the axiomK.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 ofK 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 ofK is not a great one. In any case, different answers to such questions yield different systems of modal logic.
Adding axioms toK gives rise to other well-known modal systems. One cannot prove inK that if "p is necessary" thenp is true. The axiomT remedies this defect:
T holds in most but not all modal logics. Zeman (1973) describes a few exceptions, such asS10.
Other well-known elementary axioms are:
These yield the systems (axioms in bold, systems in italics):
K throughS5 form a nested hierarchy of systems, making up the core ofnormal modal logic. But specific rules or sets of rules may be appropriate for specific systems. For example, indeontic logic, (If it ought to be thatp, then it is permitted thatp) seems appropriate, but we should probably not include that. In fact, to do so is to commit thenaturalistic fallacy (i.e. to state that what is natural is also good, by saying that ifp is the case,p ought to be permitted).
The commonly employed systemS5 simply makes all modal truths necessary. For example, ifp is possible, then it is "necessary" thatp is possible. Also, ifp is necessary, then it is necessary thatp is necessary. Other systems of modal logic have been formulated, in part becauseS5 does not describe every kind of modality of interest.
Sequent calculi 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 goodstructural proof theories, such as purity (the proof theory does not introduce extra-logical notions such as labels) and analyticity (the logical rules support a clean notion ofanalytic proof). More complex calculi have been applied to modal logic to achieve generality.[citation needed]
Analytic tableaux provide the most popular decision method for modal logics.[6]
Modalities of necessity and possibility are calledalethic modalities. They are also sometimes calledspecial modalities, from theLatinspecies. 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 asthe 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.
Inclassical 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 ofDe 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.
(Of course, this analogy does not apply alethic modality in atruly rigorous fashion; for it to do so, it would have to axiomatically make such statements as "human beings cannot rise from the dead", "Socrates was a human being and not an immortal vampire", and "we did not take hallucinogenic drugs which caused us to falsely believe the lights were on",ad infinitum. Absolute certainty of truth or falsehood exists only in the sense of logically constructed abstract concepts such as "it is impossible to draw a triangle with four sides" and "all bachelors are unmarried".)
For those having 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" (in the sense ofLeibniz) or "alternate universes"; something "necessary" is true in all possible worlds, something "possible" is true in at least one possible world.
Something is physically, or nomically, possible if it is permitted by thelaws of physics.[citation needed] For example, current theory is thought to allow for there to be anatom with anatomic number of 126,[7] even if there are no such atoms in existence. In contrast, while it is logically possible to accelerate beyond thespeed of light,[8] modern science stipulates that it is not physically possible for material particles or information.[9]
Philosophers[who?] debate if objects have properties independent of those dictated by scientific laws. For example, it might be metaphysically necessary, as some who advocatephysicalism have thought, that all thinking beings have bodies[10] and can experience the passage oftime.Saul Kripke has argued that every person necessarily has the parents they do have: anyone with different parents would not be the same person.[11]
Metaphysical possibility has been thought to be more restricting than bare logical possibility[12] (i.e., fewer things are metaphysically possible than are logically possible). However, its exact relation (if any) to logical possibility or to physical possibility is a matter of dispute. Philosophers[who?] 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 modalities (from the Greekepisteme, knowledge), deal with thecertainty of sentences. The □ operator is translated as "x is certain 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 sayboth: (1) "No, it isnot possible thatBigfoot exists; I am quite certain of that";and, (2) "Sure, it'spossible that Bigfoots could exist". What Jones means by (1) is that, given all the available information, there is no question remaining as to whether Bigfoot exists. This is an epistemic claim. By (2) he makes themetaphysical claim that it ispossible 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 (regardless of whether or not they do). Similarly, "it is possible for the person reading this sentence to be fourteen feet tall and named Chad" ismetaphysically true (such a person would not somehow be prevented from doing so on account of their height and name), but notalethically true unless you match that description, and notepistemically true if it is known that fourteen-foot-tall human beings have never existed.[citation needed]
From the other direction, Jones might say, (3) "It ispossible thatGoldbach's conjecture is true; but alsopossible that it is false", andalso (4) "if itis true, then it is necessarily true, and not possibly false". Here Jones means that it isepistemically possible that it is true or false, for all he knows (Goldbach's conjecture has not been proven either true or false), but if thereis a proof (heretofore undiscovered), then it would show that it is notlogically possible for Goldbach's conjecture to be false—there could be no set of numbers that violated it. Logical possibility is a form ofalethic possibility; (4) makes a claim about whether it is possible (i.e., logically speaking) that a mathematical truth to have been false, but (3) only makes a claim about whether it is possible, for all Jones knows, (i.e., speaking of certitude) 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 (epistemically) thatGoldbach'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 worldmight have been, but epistemic possibilities bear on the way the worldmay be (for all we know). Suppose, for example, that I want to know whether or not to take an umbrella before I leave. If you tell me "it ispossible 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 ispossible for it to rain outside" – in the sense ofmetaphysical possibility – then I am no better off for this bit of modal enlightenment.
Some features of epistemic modal logic are in debate. For example, ifx knows thatp, doesx know that it knows thatp? That is to say, should □P → □□P be an axiom in these systems? While the answer to this question is unclear,[13] there is at least one axiom that is generally included in epistemic modal logic, because it is minimally true of all normal modal logics (seethe section on axiomatic systems):
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" (alethic) and "the truth in an individual's mind" (epistemic).[14] An investigation has not found a single language in which alethic and epistemic modalities are formally distinguished, as by the means of agrammatical mood.[15]
Temporal logic is an approach to the semantics of expressions withtense, 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 usetwo pairs of operators, one for the past and one for the future (P will just mean 'it is presently the case that P'). 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 (or past). For example,
or,
The operatorsF andG may seem initially foreign, but they createnormal modal systems.FP is the same as ¬G¬P. We can combine the above operators to form complex statements. For example,PP → □PP says (effectively),Everything that is past and true is necessary.
It seems reasonable to say that possibly it will rain tomorrow, and possibly it will not; on the other hand, since we cannot change the past, if it is true that it rained yesterday, it cannot be 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 asaccidental 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, theproblem 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 ledAristotle to reject theprinciple of bivalence for assertions concerning the future.
Additional binary operators are also relevant to temporal logics (seeLinear temporal logic).
Versions of temporal logic can be used incomputer 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 thatP 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 ofAccessibility relation. (P always means "P is true at the current computer state".) 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.
Likewise talk of morality, or ofobligation andnorms 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 calleddeontic, from the Greek for "duty".
Deontic logics commonly lack the axiomT semantically corresponding to the reflexivity of the accessibility relation inKripke 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 (i.e. killing is morally forbidden), thenT implies that people actually do not kill others. The consequent is obviously false.
Instead, usingKripke semantics, we say that though our own world does not realize all obligations, the worlds accessible to it do (i.e.,T holds at these worlds). These worlds are calledidealized 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.[16]
One other principle that is often (at least traditionally) accepted as a deontic principle isD,, which corresponds to the seriality (or extendability or unboundedness) of the accessibility relation. It is an embodiment of the Kantian idea that "ought implies can". (Clearly the "can" can be interpreted in various senses, e.g. in a moral or alethic sense.)
When we try to formalize ethics with standard modal logic, we run into some problems. Suppose that we have a propositionK: 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 (1) andK together entail □Q, which says that it ought to be the case that you have stolen a small amount of money. This surely is not right, because you ought not to have stolen anything at all. And (2) does not work either: If the right representation of "if you have stolen some money it ought to be a small amount" is (2), then the right representation of (3) "if you have stolen some money then it ought to be a large amount" is. Now suppose (as seems reasonable) that you ought not to steal anything, or. But then we can deduce via and (thecontrapositive of); so sentence (3) follows from our hypothesis (of course the same logic shows sentence (2)). But that cannot 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.[17]
Doxastic logic concerns the logic of belief (of some set of agents). The term doxastic is derived from theancient Greekdoxa 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".
Modal logics may be extended tofuzzy form with calculi in the class of fuzzy Kripke models.[18]
Modal logics may also be enhanced viabase-extension semantics for the classical propositional systems. In this case, the validity of a formula can be shown by an inductive definition generated by provability in a ‘base’ of atomic rules.[19]
Intuitionistic modal logics are used in different areas of application, and they have often risen from different sources. The areas include the foundations of mathematics, computer science and philosophy. In these approaches, often modalities are added to intuitionistic logic to create new intuitionistic connectives and to simulate the monadic elements of intuitionisticfirst order logic.[20]
In the most common interpretation of modal logic, one considers "logically possible worlds". If a statement is true in allpossible 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 (not necessarily our own) 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.[21] 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.[22]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 asactual is simply that it is indeed our world –this world.[23] 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.[24]
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".
Modal logics have begun to be used in areas of the humanities such as literature, poetry, art and history.[25][26] In thephilosophy of religion, modal logics are commonly used in arguments for theexistence of God.[27]
The basic ideas of modal logic date back to antiquity.Aristotle developed a modal syllogistic in Book I of hisPrior Analytics (ch. 8–22), whichTheophrastus attempted to improve.[28] There are also passages in Aristotle's work, such as the famoussea-battle argument inDe Interpretatione §9, that are now seen as anticipations of the connection of modal logic withpotentiality and time. In the Hellenistic period, the logiciansDiodorus Cronus,Philo the Dialectician and the StoicChrysippus each developed a modal system that accounted for the interdefinability of possibility and necessity, acceptedaxiomT (see§ Axiomatic systems), and combined elements of modal logic andtemporal logic in attempts to solve the notoriousMaster Argument.[29] The earliest formal system of modal logic was developed byAvicenna, who ultimately developed a theory of "temporally modal" syllogistic.[30] Modal logic as a self-aware subject owes much to the writings of theScholastics, in particularWilliam of Ockham andJohn Duns Scotus, who reasoned informally in a modal manner, mainly to analyze statements aboutessence andaccident.
In the 19th century,Hugh MacColl made innovative contributions to modal logic, but did not find much acknowledgment.[31]C. I. Lewis founded modern modal logic in a series of scholarly articles beginning in 1912 with "Implication and the Algebra of Logic".[32][33] Lewis was led to invent modal logic, and specificallystrict implication, on the grounds that classical logic grantsparadoxes of material implication such as the principle thata falsehood implies any proposition.[34] This work culminated in his 1932 bookSymbolic Logic (withC. H. Langford),[35] which introduced the five systemsS1 throughS5.
After Lewis, modal logic received little attention for several decades.Nicholas Rescher has argued that this was becauseBertrand Russell rejected it.[36] 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 withpropositional functions", as he wrote inThe Analysis of Matter.[37]
Ruth C. Barcan (laterRuth Barcan Marcus) developed the first axiomatic systems of quantified modal logic — first and second order extensions of Lewis'S2,S4, andS5.[38][39][40]Arthur Norman Prior warned her to prepare well in the debates concerning quantified modal logic withWillard Van Orman Quine, because of bias against modal logic.[41]
The contemporary era in modal semantics began in 1959, whenSaul Kripke (then only a 18-year-oldHarvard University undergraduate) introduced the now-standardKripke semantics for modal logics. These are commonly referred to as "possible worlds" semantics. Kripke andA. N. Prior had previously corresponded at some length. Kripke semantics is basically simple, but proofs are eased using semantic-tableaux oranalytic tableaux, as explained byE. W. Beth.
A. N. Prior created moderntemporal logic, closely related to modal logic, in 1957 by adding modal operators [F] and [P] meaning "eventually" and "previously".Vaughan Pratt introduceddynamic logic in 1976. In 1977,Amir Pnueli proposed using temporal logic to formalise the behaviour of continually operatingconcurrent programs. Flavors of temporal logic includepropositional dynamic logic (PDL), (propositional)linear temporal logic (LTL),computation tree logic (CTL),Hennessy–Milner logic, andT.[clarification needed]
The mathematical structure of modal logic, namelyBoolean algebras augmented withunary operations (often calledmodal algebras), began to emerge withJ. C. C. McKinsey's 1941 proof thatS2 andS4 are decidable,[42] and reached full flower in the work ofAlfred Tarski and his studentBjarni Jónsson (Jónsson and Tarski 1951–52). This work revealed thatS4 andS5 are models ofinterior algebra, a proper extension of Boolean algebra originally designed to capture the properties of theinterior andclosure operators oftopology. Texts on modal logic typically do little more than mention its connections with the study ofBoolean algebras andtopology. For a thorough survey of the history of formal modal logic and of the associated mathematics, seeRobert Goldblatt (2006).[43]