Editing Modal logic (section)

==Axiomatic systems==
[[File:Diagram_of_Normal_Modal_Logics.png|thumb|300px|Diagram of common modal logics; '''K4W''' stands for [[Provability logic]], and '''B''' on the top corner stands for [[L. E. J. Brouwer|Brouwer]]'s system of '''KTB''']]
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 1912. [[George Edward Hughes|Hughes]] and [[Max John Cresswell|Cresswell]] (1996), for example, describe 42 [[normal modal logic|normal]] and 25 non-normal modal logics. Zeman (1973) 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 [[Clarence Irving Lewis|C. I. Lewis]], much employed since, denotes "necessarily ''p''" by a prefixed "box" (□''p'') whose [[Scope (logic)|scope]] is established by parentheses. Likewise, a prefixed "diamond" (◇''p'') denotes "possibly ''p''". Similar to the [[Quantifier (logic)|quantifiers]] in [[first-order logic]], "necessarily ''p''" (□''p'') does not assume the [[Quantifier (logic)#Range of quantification|range of quantification]] (the set of accessible possible worlds in [[Kripke semantics]]) to be non-empty, whereas "possibly ''p''" (◇''p'') often implicitly assumes <math>\Diamond\top</math> (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:
* □''p'' (necessarily ''p'') is equivalent to {{math|¬◇¬''p''}} ("not possible that not-''p''")
* ◇''p'' (possibly ''p'') is equivalent to {{math|¬□¬''p''}} ("not necessarily not-''p''")
Hence □ and ◇ form a [[duality (mathematics)#Duality in logic and set theory|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 (logic)|Boolean algebra]]:

:"It is '''not necessary that''' ''X''" is [[Logical equivalence|logically equivalent]] to "It is '''possible that not''' ''X''".
:"It is '''not possible that''' ''X''" is logically equivalent to "It is '''necessary that not''' ''X''".

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 logic]]s, include the following rule and axiom:
* '''N''', '''Necessitation Rule''': If ''p'' is a [[theorem]]/[[Tautology (logic)|tautology]] (of any system/model invoking '''N'''), then □''p'' is likewise a theorem (i.e. <math> (\models p) \implies (\models \Box p)  </math>).
* '''K''', '''Distribution Axiom''': {{math|□(''p'' → ''q'') → (□''p'' → □''q'').}}

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''', '''Reflexivity Axiom''': {{math|□''p'' → ''p''}} (If ''p'' is necessary, then ''p'' is the case.) 
'''T''' holds in most but not all modal logics. Zeman (1973) describes a few exceptions, such as ''S1<sup>0</sup>''.

Other well-known elementary axioms are:
*'''4''': <math> \Box p \to \Box \Box p</math>
*'''B''': <math> p \to \Box \Diamond p</math>
*'''D''': <math> \Box p \to \Diamond p</math>
*'''5''': <math> \Diamond p \to \Box \Diamond p </math>

These yield the systems (axioms in bold, systems in italics):
*''K'' := '''K''' + '''N'''
*''T'' := ''K'' + '''T'''
*''S4'' := ''T'' + '''4'''
*''S5'' := ''T'' + '''5'''
*''D'' := ''K'' + '''D'''.
''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]], <math> \Box p \to \Diamond p</math> (If it ought to be that ''p'', then it is permitted that ''p'') seems appropriate, but we should probably not include that <math> p \to \Box \Diamond p</math>. In fact, to do so is to commit the [[naturalistic fallacy]] (i.e. to state that what is natural is also good, by saying that if ''p'' is the case, ''p'' ought to be permitted).

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===
[[sequent calculus|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 good [[structural 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 of [[analytic proof]]). More complex calculi have been applied to modal logic to achieve generality.{{Citation needed|date=September 2024}}

===Decision methods===
[[Analytic tableaux]] provide the most popular decision method for modal logics.{{sfn|Girle|2014}}