`ConfigProp`

definition

show as: view math explainer →

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

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

 305/-! ## Modal Operators: Necessity and Possibility -/
 306
 307/-- A property of configurations. -/
 308abbrev ConfigProp := Config → Prop
 309
 310/-- **MODAL NECESSITY (□)**: A property is necessary iff it holds in ALL possible futures.
 311
 312    □p at c ⟺ ∀ y ∈ P(c), p(y)
 313
 314    In RS, necessity means "forced by cost minimization." -/
 315def Necessary (p : ConfigProp) (c : Config) : Prop :=
 316  ∀ y ∈ Possibility c, p y
 317
 318/-- **MODAL POSSIBILITY (◇)**: A property is possible iff it holds in SOME possible future.
 319
 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⟩

papers checked against this theorem

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