`Possible`

definition

show as: view math explainer →

module: IndisputableMonolith.Modal.Possibility
domain: Modal
line: 323 · 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 323.

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

used by

formal source

 320    ◇p at c ⟺ ∃ y ∈ P(c), p(y)
 321
 322    In RS, possibility means "reachable at finite cost." -/
 323def Possible (p : ConfigProp) (c : Config) : Prop :=
 324  ∃ y ∈ Possibility c, p y
 325
 326/-- Modal notation -/
 327notation:50 "□" p => Necessary p
 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

papers checked against this theorem

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