1 に答える
ボックスをフォアオールに簡単に交換でき、ダイアモンドが存在します（または単にデュアルに書き直します）。しかし、クリプキモデルの解釈のポイントは、数式が純粋にローカルレベルで評価されるということです。Kripkeモデルを、頂点にラベルが付いた有向グラフ（ラベルは命題に対応）として想像すると、数式は常に*状態で評価されます。クリプキの可能な世界哲学によれば、これはしばしば世界と呼ばれます。
さて、あなたはそれをどのように評価しますか？さて、単に、ボックスphiが（ワールド/状態/頂点で）trueと評価されるのは、到達可能なすべてのワールド（現在の頂点の外向きの近傍）phiがtrueである場合に限ります。これを一階述語論理と比較してください。ここで、すべてのオブジェクトに対してphiが真である場合にのみ（グローバルに！）、forallphiが真になります。
これで、ダイアモンドはボックスではなくデュアルに置き換えられますが、必要に応じて、到達可能なワールドが存在する場合にのみ、ダイアモンドファイが（ワールド/状態/頂点で）trueと評価されます（頂点に出力ネイバーがあります）ファイは真です。繰り返しますが、これを一階述語論理と比較してください。ファイが真であるオブジェクトが（グローバルに）存在する場合、ファイは真です。
追伸 数式を評価する頂点には、状態、ワールド、ノードなど、さまざまな名前があります。それはあなたが働いている論理のどの分野に依存します、例えばコンピュータサイエンス（CTL、CTL *、ATL、LTLなど）では、認識論理のように、システムの内部状態を表すかもしれないので、私たちは頂点状態と呼びます、義務論理、認識論理、またはあなたが持っているもの、私たちはそれらを（可能）世界と呼ぶかもしれません。
編集し、明確にしようとしています：
FOLでは、式は構造/モデルでグローバルに評価されます。forall phiは、phiがドメインのすべてのメンバーに対して保持されることを意味します。クリプキセマンティクスでは、式はドメイン wのメンバーで評価され、ボックスphiは、 wのすべての近傍について、phiが当てはまることを意味します。ダイアモンドファイは、ファイが保持するwの隣人が存在する場合に当てはまります。