modal_K

formal source

 338    exact h ⟨y, hy, hc⟩
 339
 340/-- Distribution: □(p → q) → (□p → □q) -/
 341theorem modal_K (p q : ConfigProp) (c : Config) :
 342    (□(fun x => p x → q x)) c → (□p) c → (□q) c := by
 343  intro hpq hp y hy
 344  exact hpq y hy (hp y hy)
 345
 346/-- Reflexivity: □p → p (T axiom) fails in general because c ∉ Possibility(c)
 347    (time must advance). But we have the weaker:
 348
 349    If p holds at all possible futures, and c evolves, then p holds after evolution. -/
 350theorem modal_T_weak (p : ConfigProp) (c : Config) :
 351    (□p) c → p (Actualize c) := by
 352  intro h
 353  apply h
 354  exact identity_always_possible c
 355
 356/-! ## Counterfactuals -/
 357
 358/-- A **counterfactual** is an alternative possible future that wasn't actualized.
 359
 360    y is counterfactual from c if:
 361    1. y ∈ P(c) (y was possible)
 362    2. y ≠ Actualize(c) (y wasn't chosen)
 363    3. J(y) > J(Actualize c) (y costs more, which is why it wasn't chosen) -/
 364def Counterfactual (c : Config) : Set Config :=
 365  {y : Config | y ∈ Possibility c ∧ y ≠ Actualize c ∧ J y.value > J (Actualize c).value}
 366
 367/-! ## Possibility Space -/
 368
 369/-- **POSSIBILITY SPACE**: The set of all reachable configurations from a given config.
 370
 371    This is the transitive closure of the Possibility relation. -/