def
definition
Necessary
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Modal.Possibility on GitHub at line 315.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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⟩
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