refactor(Semantics/Composition): extensional operators via DependsOn

Linglib.lean

@@ -829,7 +829,6 @@ import Linglib.Semantics.Mereology
 import Linglib.Semantics.Modality.BranchingTime
 import Linglib.Semantics.Modality.Directive
 import Linglib.Logic.Modal.Epistemic
-import Linglib.Logic.Modal.Extensional
 import Linglib.Semantics.Modality.EventRelativity
 import Linglib.Semantics.Modality.HistoricalAlternatives
 import Linglib.Semantics.Modality.Kernel

Linglib/Logic/Modal/Basic.lean

@@ -6,22 +6,40 @@ public import Mathlib.Data.Fintype.Basic
 public import Mathlib.Order.Lattice
 
 /-!
-# Modal logic over accessibility relations
-
-This file proves the order theory of `□` and `◇` beyond their Galois connection
-(`diamond_box_gc`): antitonicity in the relation (conversational backgrounds
-strengthen necessity by shrinking accessibility), necessity along the transitive closure as the
-infinite conjunction of iterated necessity, and the modal square of opposition. It also defines
-the bundled frame classes `IsS5Frame`, `IsKD45Frame`, `IsK45Frame`, `IsKTBFrame`, and the
-indicial operators, with Montague's S5 `□`/`◇` as the universal-accessibility case
-`R = .univ`. On propositions as sets necessity along the transitive closure is mathlib's
+# Accessibility and the strength of modals
+
+Necessity grows stronger as accessibility shrinks:
+[necessity is antitone in the accessibility relation](##box_restrict) and possibility is
+monotone, so a conversational background that rules out more worlds yields a stronger necessity
+modal. Necessity along the transitive closure of a relation
+[is the infinite conjunction](##box_transGen_iff) $\Box p \land \Box \Box p \land \cdots$, which
+is the shape of common knowledge. Along a serial relation $\Box p$, $\Box \neg p$, $\Diamond p$
+and $\neg \Box p$ [form a square of opposition](##modalSquare_relations).
+
+The standard modal systems are named by the axioms their frames validate. An S5 frame is
+reflexive and Euclidean, a K45 frame transitive and Euclidean, a KD45 frame, the frame of belief,
+serial, transitive and Euclidean, and a KTB frame reflexive and symmetric. An operator on
+propositions is *indicial* when it is necessity along some accessibility relation. Montague's
+necessity, true of a proposition true at every world, is the indicial operator of the universal
+relation. Not every operator is indicial: Gallin's example is Scott's present progressive.
+
+## Main definitions
+
+* `ModalLogic.modalSquare`: the modal square of opposition along a relation.
+* `ModalLogic.IsS5Frame`, `ModalLogic.IsKD45Frame`, `ModalLogic.IsK45Frame`,
+  `ModalLogic.IsKTBFrame`: the frames of the standard systems.
+* `ModalLogic.IsIndicial`: necessity along some relation.
+
+## Implementation notes
+
+On propositions as sets, necessity along the transitive closure is mathlib's
 `SetRel.core_transGen`.
 
 ## References
 
 * [kratzer-1981] — necessity strengthened by restricting accessibility
 * [carnielli-pizzi-2008] — the modal square of opposition
-* [gallin-1975] — the indicial operator hierarchy
+* [gallin-1975] — indicial operators
 * [dowty-wall-peters-1981] — Montague's S5 operators
 -/
 
@@ -45,7 +63,8 @@ theorem compl_box_compl (R : SetRel W W) (p : W → Prop) : (□[R] pᶜ)ᶜ = 
   funext w
   simp [not_box]
 
-/-- The **modal square of opposition** over `R`: `A = □p`, `E = □¬p`, `I = ◇p`, `O = ¬□p`. -/
+/-- The modal square of opposition along `R`, with corners $\Box p$, $\Box \neg p$, $\Diamond p$
+and $\neg \Box p$. -/
 def modalSquare (R : SetRel W W) (p : W → Prop) : Aristotelian.Square (W → Prop) where
   A := □[R] p
   E := □[R] pᶜ
@@ -94,31 +113,26 @@ theorem box_transGen_iff {p : W → Prop} {w : W} :
 
 /-! ### Bundled frame classes -/
 
-/-- `R` is an **S5 frame** if it is reflexive and Euclidean. -/
+/-- `R` is an *S5 frame* when it is reflexive and Euclidean. -/
 class IsS5Frame : Prop extends R.IsRefl, IsEuclidean R
 
-/-- `R` is a **KD45 frame**, the doxastic frame, if it is serial, transitive, and Euclidean. -/
+/-- `R` is a *KD45 frame*, the frame of belief, when it is serial, transitive and Euclidean. -/
 class IsKD45Frame : Prop extends IsSerial R, R.IsTrans, IsEuclidean R
 
-/-- `R` is a **K45 frame** if it is transitive and Euclidean. -/
+/-- `R` is a *K45 frame* when it is transitive and Euclidean. -/
 class IsK45Frame : Prop extends R.IsTrans, IsEuclidean R
 
-/-- `R` is a **KTB frame** if it is reflexive and symmetric. -/
+/-- `R` is a *KTB frame* when it is reflexive and symmetric. -/
 class IsKTBFrame : Prop extends R.IsRefl, R.IsSymm
 
 theorem diamond_box_iff [IsKD45Frame R] {p : W → Prop} {w : W} :
     ◇[R] (□[R] p) w ↔ □[R] p w :=
   ⟨box_of_diamond_box, diamond_box_of_box⟩
 
-/-! ### The Gallin hierarchy
-
-Operators `(W → Prop) → W → Prop` form a three-level hierarchy ([gallin-1975]): arbitrary
-operators, the **indicial** (Kripke-definable) ones, `□[R]` for some accessibility relation,
-and S5, the indicial case `R = .univ`. Tense and other non-Kripke operators live outside
-`IsIndicial`. -/
+/-! ### Indicial operators -/
 
-/-- An operator on world-propositions is **indicial** (Kripke-definable) if it is `□[R]` for
-some accessibility relation `R`. -/
+/-- An operator on propositions is *indicial* when it is necessity along some accessibility
+relation [gallin-1975]. -/
 def IsIndicial (N : (W → Prop) → W → Prop) : Prop := ∃ R : SetRel W W, N = □[R]
 
 theorem box_isIndicial : IsIndicial □[R] := ⟨R, rfl⟩

Linglib/Logic/Modal/Defs.lean

@@ -2,37 +2,47 @@ module
 
 public import Linglib.Core.Relation.SetRel
 public import Mathlib.Order.GaloisConnection.Basic
+public import Mathlib.Logic.Function.DependsOn
 
 /-!
-# Modal operators and frame conditions
-
-This file defines the necessity and possibility operators of Kripke semantics along an
-accessibility relation `R : SetRel W' W`, as operators on propositions `W → Prop`: `□[R] p w`
-holds when `p` holds at every `R`-successor of `w`, and `◇[R] p w` when it holds at some. It proves
-the axioms K, T, D, B, 4, 5 and Alt₁ over their frames, and that each axiom defines its frame
-condition.
+# Necessity and possibility in Kripke frames
+
+In Kripke semantics a proposition is *necessary* at a world when it is true at every world
+accessible from it, and *possible* when it is true at some. The accessibility relation fixes the
+kind of modality: for knowledge it relates a world to the worlds compatible with what is known
+there, for obligation to the worlds where the obligations are met. Necessity distributes over
+implication along every relation, which is axiom K, and the other axioms hold along relations with
+a matching property: T, $\Box p \to p$, along reflexive relations; D, $\Box p \to \Diamond p$,
+along serial ones; B, $p \to \Box \Diamond p$, along symmetric ones; 4,
+$\Box p \to \Box \Box p$, along transitive ones; and 5, $\Diamond p \to \Box \Diamond p$, along
+Euclidean ones. Each axiom holds along a relation
+[exactly when the relation has its property](##box_T_iff).
+
+Possibility along a relation is
+[left adjoint to necessity along the converse relation](##diamond_box_gc), which gives the
+monotonicity and distribution laws, and necessity along a composite relation is
+[nested necessity](##box_comp). Necessity at a world depends on its argument
+[at exactly the worlds the world accesses](##dependsOn_box_iff). Some laws hold at a world exactly when the world has few
+successors. Excluded middle for necessity, $\Box p \lor \Box \neg p$ for every $p$, holds at a
+world [exactly when it accesses at most one world](##box_or_box_not_at_iff), and Negation Swap,
+$\Box \neg p \leftrightarrow \neg \Box p$, holds everywhere
+[exactly when the relation is the graph of a function](##box_compl_eq_iff), along which necessity
+is [precomposition](##box_graph).
 
 ## Main definitions
 
-* `ModalLogic.Box`, `ModalLogic.Diamond`, with notation `□[R]` and `◇[R]`.
+* `ModalLogic.Box`, `ModalLogic.Diamond`: necessity and possibility along a relation, with
+  notation `□[R]` and `◇[R]`.
 * `ModalLogic.IsSerial`, `ModalLogic.IsEuclidean`: the frame conditions of D and 5.
 
-## Main statements
-
-* `ModalLogic.diamond_box_gc`: `◇` along `R` is left adjoint to `□` along its converse, which
-  gives monotonicity and the normality laws for a relation between any two types.
-* `ModalLogic.box_T_iff` and siblings: each axiom defines its frame condition.
-* `ModalLogic.box_comp`: necessity along a composite relation is nested necessity.
-* `ModalLogic.box_not_iff_not_box_at_iff`, `ModalLogic.box_compl_eq_iff`, `ModalLogic.box_graph`:
-  Negation Swap, `□¬p ↔ ¬□p` for every `p`, holds iff the relation is the graph of a function,
-  along which necessity is precomposition.
-
 ## Implementation notes
 
-`□[R]` and `◇[R]` are mathlib's `SetRel.core` and `SetRel.preimage` read on predicates
-(`box_iff_mem_core`, `diamond_iff_mem_preimage`), so propositions stated as sets use mathlib's
-`SetRel.image_core_gc`, `SetRel.core_mono`, `SetRel.core_inter`, `SetRel.core_univ` and
-`SetRel.preimage_union`. Reflexivity, symmetry and transitivity are mathlib's.
+Necessity and possibility are operators on propositions `W → Prop` along a relation
+`R : SetRel W' W`, which may relate two types. They are mathlib's `SetRel.core` and
+`SetRel.preimage` read on predicates (`box_iff_mem_core`, `diamond_iff_mem_preimage`), so
+propositions stated as sets use mathlib's `SetRel.image_core_gc`, `SetRel.core_mono`,
+`SetRel.core_inter`, `SetRel.core_univ` and `SetRel.preimage_union`. Reflexivity, symmetry and
+transitivity are mathlib's.
 
 ## References
 
@@ -52,10 +62,10 @@ section Operators
 
 variable {W W' : Type*} (R : SetRel W' W) (p : W → Prop) (w : W')
 
-/-- Necessity along `R` holds of `p` at `w` when `p` holds at every `R`-successor of `w`. -/
+/-- `p` is necessary at `w` along `R` when it holds at every world `w` accesses. -/
 def Box : Prop := ∀ v, w ~[R] v → p v
 
-/-- Possibility along `R` holds of `p` at `w` when `p` holds at some `R`-successor of `w`. -/
+/-- `p` is possible at `w` along `R` when it holds at some world `w` accesses. -/
 def Diamond : Prop := ∃ v, w ~[R] v ∧ p v
 
 @[inherit_doc] scoped notation:max "□[" R "]" => Box R
@@ -79,8 +89,8 @@ theorem diamond_iff_mem_preimage : ◇[R] p w ↔ w ∈ R.preimage {v | p v} :=
   simp [Box, Diamond, not_and]
 
 variable (R) in
-/-- Necessity distributes over conjunction ([hintikka-1962]'s
-`a believes A and B ↔ a believes A and a believes B`). -/
+/-- Necessity distributes over conjunction. For belief this is [hintikka-1962]'s principle that
+*a* believes *A and B* exactly when *a* believes *A* and *a* believes *B*. -/
 theorem box_and (q : W → Prop) : □[R] (fun v ↦ p v ∧ q v) w ↔ □[R] p w ∧ □[R] q w := by
   simp only [Box, imp_and, forall_and]
 
@@ -92,6 +102,14 @@ theorem box_iUnion {ι : Sort*} (R : ι → SetRel W' W) : □[⋃ i, R i] p w 
 theorem box_congr_left {w'' : W'} (h : ∀ v, w ~[R] v ↔ w'' ~[R] v) : □[R] p w ↔ □[R] p w'' :=
   forall_congr' fun v ↦ imp_congr_left (h v)
 
+/-- Necessity at `w` depends on its argument at a set of worlds exactly when the set contains every
+world `w` accesses. -/
+theorem dependsOn_box_iff {s : Set W} : DependsOn (□[R] · w) s ↔ {v | w ~[R] v} ⊆ s := by
+  refine ⟨fun h v hv ↦ by_contra fun hvs ↦ ?_, fun h p q hpq ↦
+    propext <| forall₂_congr fun v hv ↦ iff_of_eq (hpq v (h hv))⟩
+  have := @h (· ≠ v) (fun _ ↦ True) fun u hu ↦ eq_true (ne_of_mem_of_not_mem hu hvs)
+  exact this.mpr (fun _ _ ↦ trivial) v hv rfl
+
 end Operators
 
 /-! ### The Galois connection and normality -/
@@ -119,8 +137,9 @@ theorem diamond_sup : ◇[R] (p ⊔ q) = ◇[R] p ⊔ ◇[R] q :=
 theorem box_top : □[R] ⊤ = ⊤ := by
   simpa using (diamond_box_gc R.inv).u_top
 
-/-- Over any relation, `p ≤ □_{R⁻¹} ◇_R p`, which is Prior's tense axiom of conversion `A ⊃ G P A`.
-This is the unit of the adjunction. -/
+/-- Along any relation $p$ entails $\Box_{R^{-1}} \Diamond_R p$, the unit of the adjunction. For
+tense this is Prior's axiom of conversion $A \supset GPA$: what is the case will always have been
+the case. -/
 theorem le_box_inv_diamond (p : W → Prop) : p ≤ □[R.inv] (◇[R] p) :=
   (diamond_box_gc R).le_u_l p
 
@@ -137,11 +156,11 @@ theorem diamond_comp (S : SetRel W W) (p : W → Prop) : ◇[R ○ S] p = ◇[R]
 
 /-! ### Frame conditions -/
 
-/-- `R` is *serial* if every world accesses at least one world. -/
+/-- `R` is *serial* when every world accesses some world. -/
 class IsSerial : Prop where
   serial : ∀ w, ∃ v, w ~[R] v
 
-/-- `R` is *Euclidean* if any two `R`-successors of a world access each other. -/
+/-- `R` is *Euclidean* when any two worlds accessed from one world access each other. -/
 class IsEuclidean : Prop where
   eucl : ∀ w v u, w ~[R] v → w ~[R] u → v ~[R] u
 
@@ -181,8 +200,8 @@ theorem box_T [R.IsRefl] (h : □[R] p w) : p w := h w R.rfl
 theorem box_D [IsSerial R] (h : □[R] p w) : ◇[R] p w :=
   let ⟨v, hwv⟩ := IsSerial.serial (R := R) w; ⟨v, hwv, h v hwv⟩
 
-/-- If some `R`-successor of `w` is also an `S`-successor, then `□[R] p` at `w` gives `◇[S] p`
-at `w`; `box_D` is the case `S = R`. -/
+/-- If `w` accesses some world along both `R` and `S`, then necessity along `R` at `w` entails
+possibility along `S`; `box_D` is the case `S = R`. -/
 theorem diamond_of_box {S : SetRel W W} (h : ◇[R] (w ~[S] ·) w) (hp : □[R] p w) : ◇[S] p w :=
   let ⟨v, hR, hS⟩ := h; ⟨v, hS, hp v hR⟩
 

Linglib/Logic/Modal/Epistemic.lean

@@ -4,31 +4,36 @@ public import Linglib.Discourse.CommonGround
 public import Linglib.Logic.Modal.Basic
 
 /-!
-# Multi-agent epistemic logic
-
-The group knowledge operators of [fagin-halpern-moses-vardi-1995] over agent-indexed
-accessibility `Rs : E → SetRel W W` are boxes along lattice combinations of the agents'
-relations: agent `i` knows `p` at `w` when `□[Rs i] p w`, everyone in `G` knows it when
-`□[⋃ i ∈ G, Rs i] p w`, it is distributed knowledge when `□[⋂ i ∈ G, Rs i] p w`, and the
-hierarchy `C_G ≤ E_G ≤ Kᵢ ≤ D_G` is antitonicity in the relation (`ModalLogic.box_restrict`).
-Common knowledge is the box along the transitive closure of the union: `p` holds at every world
-reachable by a chain of members' accessibility ([lederman-2014] Appendix 2.B's construction),
-equivalently the infinite conjunction `E_G p ∧ E_G (E_G p) ∧ ⋯`
-(`commonKnowledge_iff_forall_iterate`). Belief is the same operator over a KD45 frame
-(`ModalLogic.IsKD45Frame`).
+# Group knowledge
+
+In epistemic logic an agent *knows* a proposition at a world when the proposition is true at
+every world the agent cannot tell apart from it. A group of agents gives rise to three further
+notions. A proposition is known by *everyone* in the group when each member knows it; it is
+*distributed knowledge* when it is true at every world that all the members consider possible, so
+that it follows from what they know together; and it is *common knowledge* when everyone knows
+it, everyone knows that everyone knows it, and so on without end. Each is necessity along a
+relation built from the members' relations: their union for everyone's knowledge, their
+intersection for distributed knowledge, and the transitive closure of their union for common
+knowledge, which [is the infinite conjunction of iterated knowledge by
+everyone](##commonKnowledge_iff_forall_iterate). Since necessity is antitone in the relation, common knowledge entails everyone's knowledge,
+which entails each member's knowledge, which entails distributed knowledge. Belief is the same
+operator along a KD45 frame.
+
+A common ground is *grounded in* common knowledge when the worlds it leaves open are exactly
+those at which every proposition it accepts is common knowledge.
 
 ## Main definitions
 
-* `ModalLogic.CommonKnowledge`: `C_G`.
-* `Filter.GroundedIn`: a common ground whose context set is exactly what is common
-  knowledge ([stalnaker-2002]).
+* `ModalLogic.CommonKnowledge`: common knowledge in a group.
+* `Filter.GroundedIn`: a common ground grounded in common knowledge.
 
 ## References
 
 * [fagin-halpern-moses-vardi-1995] — group knowledge and its reachability semantics
 * [halpern-2003] — the same operators in the uncertainty setting
 * [fagin-halpern-1994] — the probabilistic extension, `Studies/FaginHalpern1994.lean`
-* [hintikka-1962] — knowledge as `□`
+* [hintikka-1962] — knowledge as necessity
+* [lederman-2014] — common knowledge as reachability (UNVERIFIED: Appendix 2.B)
 * [stalnaker-2002] — common ground as common knowledge
 -/
 
@@ -41,8 +46,8 @@ open SetRel
 variable {W E : Type*} {Rs : E → SetRel W W} {i : E} {G : Set E} {p : W → Prop} {w : W}
 
 variable (Rs G) in
-/-- Common knowledge among `G`: `p` holds at every world reachable from `w` by a chain of
-members' accessibility. -/
+/-- `p` is common knowledge among `G` at `w` when it holds at every world reachable from `w`
+by a chain of worlds each accessible to some member from the one before. -/
 def CommonKnowledge (p : W → Prop) (w : W) : Prop := □[transGen (⋃ i ∈ G, Rs i)] p w
 
 theorem box_of_commonKnowledge (hi : i ∈ G) (h : CommonKnowledge Rs G p w) : □[Rs i] p w :=
@@ -61,9 +66,9 @@ namespace Filter
 
 variable {W E : Type*}
 
-/-- A common ground `cg : Filter W` is grounded in common knowledge when its context set
-`cg.ker` is exactly the set of worlds where each accepted proposition is common knowledge
-among `G` ([stalnaker-2002]). -/
+/-- A common ground `cg` is grounded in common knowledge among `G` when its context set
+`cg.ker` is exactly the set of worlds at which every proposition it accepts is common knowledge
+[stalnaker-2002]. -/
 def GroundedIn (cg : Filter W) (Rs : E → SetRel W W) (G : Set E) : Prop :=
   ∀ w, w ∈ cg.ker ↔ ∀ p ∈ cg, ModalLogic.CommonKnowledge Rs G (· ∈ p) w