計算機科學家邏輯/模態邏輯/公理化

公理化

最簡單的模態邏輯稱為 $K$，由以下公理給出

• 所有經典重言式（及其替換）
• 模態公理：所有形式為 $\square (X\to Y)\to (\square X\to \square Y)$ 的公式

以及推理規則

• 肯定前件規則：從 $X$ 和 $X\to Y$ 推匯出 $Y$
• 必然性規則：從 $X$ 推匯出 $\square X$

從公式集 $S$ 推匯出 $X$ 的 $K$ 推導是一個公式序列，以 $X$ 結束，其中每個公式都是 $K$ 的公理、$S$ 的成員，或者透過應用推理規則從前面的項推匯出來。\defined{$K$ 證明} $X$ 是一個從 $\emptyset$ 推匯出 $X$ 的 $K$ 推導。

舉個例子，考慮 $K$ 對 $(\square P\land \square Q)\to \square (P\land Q)$ 的證明

${\begin{matrix}&{\mbox{Tautology: }}&P\to (Q\to (P\land Q))\\&{\mbox{Necessitation: }}&\square (P\to (Q\to (P\land Q)))\\&{\mbox{Modal axiom:}}&\square (P\to (Q\to (P\land Q)))\to (\square P\to \square (Q\to (P\land Q)))\\&{\mbox{Modus ponens: }}&\square P\to \square (Q\to (P\land Q))\\&{\mbox{Modal axiom:}}&\square (Q\to (P\land Q))\to (\square Q\to \square (P\land Q))\\&{\mbox{Classical arg: }}&\square P\to (\square Q\to \square (P\land Q))\\&{\mbox{Classical arg: }}&(\square P\land \square Q)\to \square (P\land Q)\\\end{matrix}}$

這個蘊含的逆命題也有類似的證明；因此在 $K$ 中我們有

$\square (P\land Q)\leftrightarrow (\square P\land \square Q)$

注意，對析取的分配律不成立！（為什麼？）

K 的擴充套件

從模態邏輯 $K$ 開始，我們可以新增額外的公理，從而得到不同的邏輯。我們列出以下基本公理
$K$ : $\square (X\to Y)\to (\square X\to \square Y)$

$T$ : $\square A\to A$

$D$ : $\square A\to \diamond A$

$4$ : $\square A\to \square \square A$

$5$ : $\diamond A\to \square \diamond A$

$B$ : $A\to \square \diamond A$

傳統上，如果在邏輯 $K$ 中新增公理 $A_{1},\cdots ,A_{n}$，我們稱得到的邏輯為 $KA_{1}\cdots A_{n}$。然而，有時這個邏輯非常有名，以至於被另一個名字稱呼；例如 $KT4$ 被稱為 $S4$。

這些邏輯也可以用某些框架類來刻畫，因為已知特定的公理對應於可達性關係 $R$ 上的特定限制。如果 $\langle W,R\rangle$ 是一個框架，那麼某個公理在 $\langle W,R\rangle$ 上有效，當且僅當 $R$ 滿足某個限制。一些限制可以透過一階邏輯公式來表達，其中二元謂詞 $R(x,y)$ 表示可達性關係

${\begin{matrix}T:&{\mbox{Reflexive}}&\forall w{\text{:}}R(w,w)\\D:&{\mbox{Serial}}&\forall w\exists w':R(w,w')\\4:&{\mbox{Transitive}}&\forall s,t,u:(R(s,t)\land R(t,u))\to R(s,u)\\5:&{\mbox{Euclidean}}&\forall s,t,u:(R(s,t)\land R(s,u))\to R(t,u)\\B:&{\mbox{Symmetric}}&\forall w,w':R(w,w')\to R(w',w)\end{matrix}}$