`modal_duality`

proved

show as: view math explainer →

module: IndisputableMonolith.Modal.Possibility
domain: Modal
line: 331 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Modal.Possibility on GitHub at line 331.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 328notation:50 "◇" p => Possible p
 329
 330/-- Duality: □p ⟺ ¬◇¬p -/
 331theorem modal_duality (p : ConfigProp) (c : Config) :
 332    (□p) c ↔ ¬(◇(fun x => ¬p x)) c := by
 333  constructor
 334  · intro h ⟨y, hy, hny⟩
 335    exact hny (h y hy)
 336  · intro h y hy
 337    by_contra hc
 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)

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.