様相論理を学ぶと体系が沢山現れることが気になると思う。

$\mathsf{K}, \mathsf{S4}, \mathsf{S5}, \mathsf{K4.3}, \mathsf{S4.3}, \cdots$

それじゃあ一体いくらあるんだ？

という疑問に対してこう答えられる。

S4を含む様相論理だけで非可算無限個ある。

つまりアホほど存在するのである。

Kit Fine, "An ascending chain of S4 logics", Theoria, vol. 40, issue 2, pp.110-116にある証明をある程度ラフに説明する。

証明にはJankov-fine論理式というもの(原論文ではframe-formula)とbounded morphismというものを使う。以下記号は読みやすさを考慮し、適宜原論文とは異なるものを用いている。

フレーム $\mathcal{F}$ を $\{v\in W : wRv\}$ に制限したものを $\mathcal{F}^{w}$ と書く。

bounded morphismの定義

Given two frames $F=(W, R)$ and $F'=(W', R')$ , a bounded morphism $f: W\to W'$ between $F$ and $F'$ is a map such that

$f$ is a surjective,

$wRv$ implies $f(w)R'f(v)$ ,

$f(w)R'v'$ implies that there is a $v\in W$ such that $wRv$ and [f(v)=v'].

bounded morphismとはフレーム版の双模倣性のようなものである。

Jankov-Fine論理式 $\phi_{\mathcal{F}}$ は次のようにして作る。フレーム $\mathcal{F}$ が与えられた時、 $\mathcal{F}$ の状態を $w_0,\cdots, w_n$ と列挙する(nは自然数)。各状態 $w_i$ に対して命題変数 $p_i$ を対応させる。始点を $w_0$ とする。以下の論理式の連言を $\phi_{\mathcal{F}}$ とする。

(i) $p_{0}$

(ii) $\square(p_0\lor\dots\lor p_n)$

(iii) $(p_i\to\lnot p_j)\land\square(p_i\to\lnot p_j)$ for each $i, j$ with $i\neq j\le n$

(iv) $(p_i\to\lnot p_j)\land\square(p_i\to\diamond p_j)$ for each $i, j$ with $w_i R w_j$

(v) $(p_i\to\lnot\diamond p_j)\land\square(p_i\to\lnot \diamond p_j)$ for each $i, j$ with $\lnot(w_i R w_j)$

これは証明で用いられる次の梯子型のフレームを見ると理解しやすい。

f:id:Incognito0:20200720160025p:plain — Fine(1974)p.113の図を使用

ここで0が始点である。(i)から(iii)により各点には同じ自然数の論理式が一対一で対応しており、(iv), (v)はフレームの到達性関係を論理式の形で記述している。

Jankov-Fine論理式は以下の補題が成り立つようにできている。

補題フレーム $\mathcal{G}$ がJankov-Fine論理式 $\phi_{\mathcal{F}}$ を充足する iff ある $w_0\in V$ に対してbounded morphism $f:\mathcal{G}^{w_0}\to \mathcal{F}$ が存在する。

S4に特定の論理式を足していくことでS4を含む論理がどんどん増えていく。しかしこのようにして作られていく論理の列がどこかで証明能力に関して飽和し、同じものになってしまうかもしれない。このようなことが起きないような追加する論理式を選ばないといけないし、証明で確かめることが必要である。そのために都合の良くうまく選んだ論理式がJankov-Fine論理式(の否定)なのである。

$M\subseteq \omega$ に対して $LM=S4 + \{\lnot\phi_{\mathcal{F}_{m}}: m\in M\}$ とする. ここで $\mathcal{F}_{n}=\{ 5+2n, R| 5+2n \}$ . ¹