modal_T_weak

formal source

 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. -/
 372def PossibilitySpace (c : Config) : Set Config :=
 373  {y : Config | ∃ n : ℕ, ∃ path : Fin (n+1) → Config,
 374    path ⟨0, Nat.zero_lt_succ n⟩ = c ∧
 375    path ⟨n, Nat.lt_succ_self n⟩ = y ∧
 376    ∀ i : Fin n, path ⟨i.val + 1, Nat.succ_lt_succ i.isLt⟩ ∈
 377                 Possibility (path ⟨i.val, Nat.lt_of_lt_of_le i.isLt (Nat.le_succ n)⟩)}
 378
 379/-- The identity is in every possibility space. -/
 380theorem identity_in_all_possibility_spaces (c : Config) :