様相論理（ようそうろんり、英: modal logic）は、いわゆる古典論理の対象でない、様相（modal）と呼ばれる「?は必然的に真」や「?は可能である」といった必然性や可能性などを扱う論理である（様相論理は、部分の真理値からは全体の真理値が決定されない内包論理の一種と見ることができる）。

その歴史は古くアリストテレスまで遡ることができる[1]:138が、形式的な扱いは数理論理学以降、非古典論理としてである。

様相論理では一般に、標準的な論理体系に「?は必然的である」ことを意味する必然性演算子 ◻ {\displaystyle \Box } と、「?は可能である」ことを意味する可能性演算子 ◊ {\displaystyle \Diamond } のふたつの演算子が追加される。
真理論的様相と認識論的様相

様相論理は真理論的（形而上学的、論理的）様相の文脈で語られることが最も多い。この様相においては「?は必然的である」、「?は可能である」といった言明が扱われるが、これは認識論的様相と混同されやすい。

例えば「雪男は存在しているはずがない」という主張と、「雪男が存在することは可能である」という主張は、矛盾無く行うことが可能である。この場合、前者は認識論的様相であり、「（これまでの情報からして）雪男が実際に存在するとは考えられない」という主張とみなしうる。一方、後者は真理論的様相であり「（実際には存在しないのだが）雪男が存在することは可能である」という主張であると解釈することができる。

あるいは、「ゴールドバッハ予想は正しいかもしれないし、正しくないかもしれない」という言明も認識論的である。これは現時点の知識では正しいかどうか分からないということであり、仮にゴールドバッハ予想の証明が存在し、その方法に気付いていないだけだとすれば、真理論的には「正しくないかもしれない」という主張は誤りであることになる。

これ以外の様相としては、時間的なものがある。例えば、「明日雨が降るかどうかは決まっていない」のに対し、「昨日雨が降ったかどうかは決まっている」と考えられる。このように素朴な時間観には同意しない哲学者も多いが、その構造は様相論理によって把握することができる。

さらに「?べきではない」「?してもよい」といった義務に関わる命題も様相論理によって扱うことができる。直感的にも、「?べきではない」と「?してもよい」の関係は「?は必然的である」と「?は可能である」の関係と極めて類似している。義務表現を扱う様相論理は義務論理と呼ばれる。
様相論理の公理系

様相論理には様々な公理系が考えられており、どのような公理系が妥当なのかはそれ自体が論争の的である。二つの様相演算子のあいだにド・モルガンの法則的な関係が成立することは、どの公理系でも共通している。 ◻ {\displaystyle \Box } は必然性演算子、 ◊ {\displaystyle \Diamond } は可能性演算子である。

◻ p ↔ ¬ ◊ ¬ p {\displaystyle \Box p\leftrightarrow \neg \Diamond \neg p}

◊ p ↔ ¬ ◻ ¬ p {\displaystyle \Diamond p\leftrightarrow \neg \Box \neg p}

即ち、「必然的に真」は「偽である可能性がない」と同等であり、「真である可能性がある」は「必然的に偽であるわけではない」と同等である。様相論理としての最低限の定義 ◊ p = ¬ ◻ ¬ p {\displaystyle \Diamond p=\neg \Box \neg p} のみを満たす最小の公理系としては、E という公理系が知られている。これは古典命題論理に以下の推論規則を加えたものである。

推論規則 : φ ↔ ψ {\displaystyle \varphi \leftrightarrow \psi } が成り立つならば、 ◻ φ ↔ ◻ ψ {\displaystyle \Box \varphi \leftrightarrow \Box \psi } も成り立つ。

この公理系 E より「強い」すべての公理系は、Classical な公理系と呼ばれる。

しかしながら、真と認めるべきかどうか直感的に明らかでない論理式も多く作ることができる。例えば「必然的に真ならば必然的に「必然的に真」である」と言えるのかどうか、即ち ◻ p → ◻ ◻ p {\displaystyle \Box p\rightarrow \Box \Box p} が成り立つのかどうかははっきりしない。こういった定理を認めるか否かによって、様々な公理系が生まれる。

必然化規則を満たす公理系（Normal な公理系）の中で、最も「小さな」公理系として知られているのは、クリプキによる K という公理系である。K の公理系に更に公理を付け加えることにより、様々な様相論理が得られる[2]。
K の公理系

K の公理系は古典命題論理の公理系に公理図式K（太字になっていることに注意）と必然化規則（necessitation）を付け加えたものである。

公理K : ◻ ( A → B ) → ( ◻ A → ◻ B ) {\displaystyle \Box (A\rightarrow B)\rightarrow (\Box A\rightarrow \Box B)}

必然化規則 : A {\displaystyle A} が無仮定で証明可能ならば、 ◻ A {\displaystyle \Box A} もまた無仮定で成立する。

ここで可能性演算子は定義 ◊ p = ¬ ◻ ¬ p {\displaystyle \Diamond p=\neg \Box \neg p} によって導入される。
T の公理系

K の公理系に以下の公理図式T「必然的に真ならば、真である」を加えた体系は T と呼ばれる。

公理T : ◻ A → A {\displaystyle \Box A\rightarrow A}

T においては、K では証明可能でなかった p → ◊ p {\displaystyle p\rightarrow \Diamond p} などが証明可能となる。
S4, S5の公理系

公理系K,Tにおいては以下の1?4の同値性を証明できないために多重の様相（ ◊ ◊ {\displaystyle \Diamond \Diamond } , ◻ ◻ {\displaystyle \Box \Box } , ◊ ◻ {\displaystyle \Diamond \Box } , ◻ ◊ {\displaystyle \Box \Diamond } , ◻ ◻ ◻ {\displaystyle \Box \Box \Box } , ...）を減らすことができない。従って無限に多くの様相が区別されることになる。
◊ P ↔ ◻ ◊ P {\displaystyle \Diamond P\leftrightarrow \Box \Diamond P}

◻ P ↔ ◊ ◻ P {\displaystyle \Box P\leftrightarrow \Diamond \Box P}

◊ P ↔ ◊ ◊ P {\displaystyle \Diamond P\leftrightarrow \Diamond \Diamond P}

◻ P ↔ ◻ ◻ P {\displaystyle \Box P\leftrightarrow \Box \Box P}

これらは還元法則と呼ばれるが、右辺→左辺はTで証明可能なので、1?4の左辺→右辺の内、どれを公理系T に付け加えるかで S4, S5 の違いが生まれる。

公理4 : ◻ A → ◻ ◻ A {\displaystyle \Box A\rightarrow \Box \Box A} （還元法則の4に対応）をTに付け加えたのがS4である。

公理5 : ◊ A → ◻ ◊ A {\displaystyle \Diamond A\rightarrow \Box \Diamond A} （還元法則の1に対応）をTに付け加えたのがS5である。

実は、還元法則の1を仮定すれば、Tの下で2?4は証明可能となる。一方3を仮定すれば4がTで証明可能だが、2は証明可能でない。従ってS5はS4より真に強い（証明力の強い）公理系である。還元法則の導入により本質的に区別される様相はS4で7種類、S5で3種類と実際に減少する。

クリプキはこの S5 に非常に単純な意味論が当てはまることを示した（下の#様相論理の意味論参照）。しかし実際には、議論の目的によって適切な公理系は異なる。例えば、真理論的様相に関しては S5 が最も適当だが、認識論的様相では S4 という公理系が適切であると考えられている。
様相論理の意味論

様相論理の意味論としてはソール・クリプキによって与えられたクリプキ意味論と呼ばれる体系があり、それと関係するよく知られたアイディアとして可能世界論がある。上で見た公理系のバリエーションは、可能世界のあいだの二項関係として定義される到達可能性の概念によって捉えることができる。なお、可能世界という概念をどう解釈すべきかを巡っては、哲学上の議論も盛んである。

命題様相論理の意味論の概要は以下の通りである。

Wを空でない集合とする。これは個々の可能世界全体の集合を表していると考えられる。次にW上の二項関係Rを考える。つまり R ⊆ W 2 {\displaystyle R\subseteq W^{2}} である。また ⟨ w , w ′ ⟩ ∈ R {\displaystyle \langle w,w'\rangle \in R} を w R w ′ {\displaystyle _{w}R_{w'}} と表す。RはW上の到達関係と呼ばれ、様相演算子の付いた論理式の真偽に影響する。またPVを命題変数全体の集合とし、このPVと先に定義したWに対し、関数Vを V : P V → 2 W {\displaystyle V:PV\rightarrow 2^{W}}

として定義する（ 2 W {\displaystyle 2^{W}} はWの冪集合、すなわち部分集合全体の集合である）。これは、ある原子命題について、それが真である可能世界の集合を与える解釈である。すなわち、可能世界wにおいて原子命題pが真であることを w ∈ V ( p ) {\displaystyle w\in V(p)} として表す。このように定義された順序三組〈W, R, V〉を解釈（もしくはクリプキモデル）と呼ぶ。

さて、解釈Vを以下のように論理式全体に再帰的に拡張する。A、Bを任意の論理式、wをWの任意の要素とする。

w ∈ V ( ¬ A ) ⇔ w ∉ V ( A ) {\displaystyle w\in V(\neg A)\Leftrightarrow w\notin V(A)}

w ∈ V ( A ∧ B ) ⇔ w ∈ V ( A ) {\displaystyle w\in V(A\land B)\Leftrightarrow w\in V(A)} かつ w ∈ V ( B ) {\displaystyle w\in V(B)}

w ∈ V ( A ∨ B ) ⇔ w ∈ V ( A ) {\displaystyle w\in V(A\lor B)\Leftrightarrow w\in V(A)} または w ∈ V ( B ) {\displaystyle w\in V(B)}