Modal logic

It plays a major role in philosophy and related fields as a tool for understanding concepts such as knowledge, obligation, and causation.

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 logic D is sound and complete if one requires the accessibility relation to be serial.

The now-standard relational semantics emerged in the mid twentieth century from work by Arthur Prior, Jaakko Hintikka, and Saul Kripke.

The former is conventionally read aloud as "necessarily", and can be used to represent notions such as moral or legal obligation, knowledge, historical inevitability, among others.

The latter is typically read as "possibly" and can be used to represent notions including permission, ability, compatibility with evidence.

For this reason, modal logicians sometimes talk about frames, which are the portion of a relational model excluding the valuation function.

This gives the corresponding modal graph which is total complete (i.e., no more edges (relations) can be added).

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.

Modern treatments of modal logic begin by augmenting the propositional calculus with two unary operations, one denoting "necessity" and the other "possibility".

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.

[citation needed] Analytic tableaux provide the most popular decision method for modal logics.

For this reason, or perhaps for their familiarity and simplicity, necessity and possibility are often casually treated as the subject matter of modal logic.

(Of course, this analogy does not apply alethic modality in a truly 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".)

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 say both: (1) "No, it is not possible that Bigfoot exists; I am quite certain of that"; and, (2) "Sure, it's possible that Bigfoots could exist".

Here Jones means that it is epistemically possible that it is true or false, for all he knows (Goldbach's conjecture has not been proven either true or false), but if there is a proof (heretofore undiscovered), 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.

It is worthwhile to observe that Jones is not necessarily correct: It is possible (epistemically) that Goldbach's conjecture is both true and unprovable.

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

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 (P will just mean 'it is presently the case that P').

Considering this thesis led Aristotle to reject the principle of bivalence for assertions concerning the future.

These two examples involve nondeterministic or not-fully-understood computations; there are many other modal logics specialized to different types of program analysis.

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

[25] 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 (see below), and combined elements of modal logic and temporal logic in attempts to solve the notorious Master Argument.

In the 19th century, Hugh MacColl made innovative contributions to modal logic, but did not find much acknowledgment.

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

Kripke semantics is basically simple, but proofs are eased using semantic-tableaux or analytic tableaux, as explained by E. W. Beth.

In 1977, Amir Pnueli proposed using temporal logic to formalise the behaviour of continually operating concurrent programs.

Texts on modal logic typically do little more than mention its connections with the study of Boolean algebras and topology.