diff --git a/Linglib.lean b/Linglib.lean
index bb5bcded5c..e083ca850a 100644
--- a/Linglib.lean
+++ b/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
diff --git a/Linglib/Logic/Modal/Basic.lean b/Linglib/Logic/Modal/Basic.lean
index 4bd36642e7..004250f4e7 100644
--- a/Linglib/Logic/Modal/Basic.lean
+++ b/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⟩
diff --git a/Linglib/Logic/Modal/Defs.lean b/Linglib/Logic/Modal/Defs.lean
index e0d4ffdb6e..fcb28133a2 100644
--- a/Linglib/Logic/Modal/Defs.lean
+++ b/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⟩
 
diff --git a/Linglib/Logic/Modal/Epistemic.lean b/Linglib/Logic/Modal/Epistemic.lean
index 7884aee2b5..c62e18a5ec 100644
--- a/Linglib/Logic/Modal/Epistemic.lean
+++ b/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
 
diff --git a/Linglib/Logic/Modal/Extensional.lean b/Linglib/Logic/Modal/Extensional.lean
deleted file mode 100644
index 8e42088edd..0000000000
--- a/Linglib/Logic/Modal/Extensional.lean
+++ /dev/null
@@ -1,115 +0,0 @@
-module
-
-public import Mathlib.Logic.Function.Basic
-public import Linglib.Logic.Modal.Defs
-
-/-!
-# Extensional operators
-
-An operator `O` on intensions `W → α` is *extensional at* `w` when its value at `w` depends on
-its argument only through the argument's extension at `w`, i.e. `O · w` factors through
-evaluation at `w`. Equivalently, `O` cannot tell an argument whose index it binds from the same
-argument with the index fixed at `w`, which is why a situation pronoun bound under an extensional
-operator reads as if it were free. The pointwise connectives are extensional, and extensionality
-is closed under them and under composition; the Kripke box `ModalLogic.Box R` is extensional at
-`w` only when `w` reaches no index but itself.
-
-## Main definitions
-
-* `IsExtensionalAt O w`, `IsExtensional O`: local truth-functionality of an operator.
-
-## Main results
-
-* `isExtensionalAt_iff_forall_diag`: extensionality as the failure to distinguish a bound index
-  from a fixed one.
-* `isExtensionalAt_box_iff`: when the box is extensional.
-* `IsExtensionalAt.and`, `IsExtensionalAt.or`, `IsExtensionalAt.not`,
-  `IsExtensionalAt.comp`: closure of extensional operators.
--/
-
-@[expose] public section
-
-namespace ModalLogic
-
-variable {W α β : Type*}
-
-/-- `O` is extensional at `w` when its value at `w` depends on the argument intension only
-through the argument's extension at `w`, that is, when `O · w` factors through evaluation at
-`w`. -/
-def IsExtensionalAt (O : (W → α) → W → β) (w : W) : Prop :=
-  ∀ p q : W → α, p w = q w → O p w = O q w
-
-/-- `O` is extensional at every index. -/
-def IsExtensional (O : (W → α) → W → β) : Prop :=
-  ∀ w, IsExtensionalAt O w
-
-theorem isExtensionalAt_iff_factorsThrough (O : (W → α) → W → β) (w : W) :
-    IsExtensionalAt O w ↔ Function.FactorsThrough (O · w) (· w) :=
-  ⟨fun h _ _ hpq => h _ _ hpq, fun h _ _ hpq => h hpq⟩
-
-theorem not_isExtensionalAt_iff_exists_witness {O : (W → α) → W → β} {w : W} :
-    ¬ IsExtensionalAt O w ↔ ∃ p q, p w = q w ∧ O p w ≠ O q w := by
-  simp only [IsExtensionalAt, not_forall, exists_prop]
-
-/-- An operator is extensional at `w` exactly when it cannot tell an argument whose index it
-binds, `fun v ↦ g v v`, from the same argument with the index fixed at `w`, `g w`. -/
-theorem isExtensionalAt_iff_forall_diag {O : (W → α) → W → β} {w : W} :
-    IsExtensionalAt O w ↔ ∀ g : W → W → α, O (fun v ↦ g v v) w = O (g w) w := by
-  classical
-  refine ⟨fun h g ↦ h _ _ rfl, fun h p q hpq ↦ ?_⟩
-  have h' := h fun u v ↦ if u = w then q v else p v
-  have e₁ : (fun v ↦ if v = w then q v else p v) = p := by
-    funext v
-    by_cases hv : v = w
-    · subst hv; simp [hpq]
-    · simp [hv]
-  have e₂ : (fun v ↦ if w = w then q v else p v) = q := by simp
-  rwa [e₁, e₂] at h'
-
-open SetRel in
-/-- The box along `R` is extensional at `w` exactly when `w` reaches no index but itself. -/
-theorem isExtensionalAt_box_iff {R : SetRel W W} {w : W} :
-    IsExtensionalAt (Box R) w ↔ ∀ v, w ~[R] v → v = w := by
-  refine ⟨fun h v hv ↦ ?_, fun h p q hpq ↦ propext ⟨fun hp v hv ↦ ?_, fun hq v hv ↦ ?_⟩⟩
-  · have := h (fun _ ↦ True) (· = w) (eq_true rfl).symm
-    exact (this ▸ fun _ _ ↦ trivial : Box R (· = w) w) v hv
-  · obtain rfl := h v hv
-    exact hpq ▸ hp v hv
-  · obtain rfl := h v hv
-    exact hpq ▸ hq v hv
-
-namespace IsExtensionalAt
-
-variable {w : W}
-
-theorem eval : IsExtensionalAt (fun (p : W → α) w' => p w') w :=
-  fun _ _ hpq => hpq
-
-theorem const (P : W → Prop) : IsExtensionalAt (fun (_ : W → α) w' => P w') w :=
-  fun _ _ _ => rfl
-
-/-- Pointwise negation is extensional, since negation is not an intensional operator. -/
-theorem neg : IsExtensionalAt (fun p (w' : W) => ¬ p w') w :=
-  fun _ _ hpq => congrArg Not hpq
-
-theorem and {O₁ O₂ : (W → α) → W → Prop} (h₁ : IsExtensionalAt O₁ w)
-    (h₂ : IsExtensionalAt O₂ w) : IsExtensionalAt (fun p w' => O₁ p w' ∧ O₂ p w') w :=
-  fun p q hpq => congrArg₂ And (h₁ p q hpq) (h₂ p q hpq)
-
-theorem or {O₁ O₂ : (W → α) → W → Prop} (h₁ : IsExtensionalAt O₁ w)
-    (h₂ : IsExtensionalAt O₂ w) : IsExtensionalAt (fun p w' => O₁ p w' ∨ O₂ p w') w :=
-  fun p q hpq => congrArg₂ Or (h₁ p q hpq) (h₂ p q hpq)
-
-theorem not {O : (W → α) → W → Prop} (h : IsExtensionalAt O w) :
-    IsExtensionalAt (fun p w' => ¬ O p w') w :=
-  fun p q hpq => congrArg Not (h p q hpq)
-
-/-- Extensional operators compose, so scope-inertness lifts through a stack of them. -/
-theorem comp {O₁ : (W → α) → W → β} {O₂ : (W → β) → W → Prop}
-    (h₂ : IsExtensionalAt O₂ w) (h₁ : IsExtensionalAt O₁ w) :
-    IsExtensionalAt (fun p w' => O₂ (fun s => O₁ p s) w') w :=
-  fun p q hpq => h₂ _ _ (h₁ p q hpq)
-
-end IsExtensionalAt
-
-end ModalLogic
diff --git a/Linglib/Logic/Modal/FirstOrder/Correspondence.lean b/Linglib/Logic/Modal/FirstOrder/Correspondence.lean
index 2b004a6330..8a615f71aa 100644
--- a/Linglib/Logic/Modal/FirstOrder/Correspondence.lean
+++ b/Linglib/Logic/Modal/FirstOrder/Correspondence.lean
@@ -4,29 +4,33 @@ public import Linglib.Core.ModelTheory.Binders
 public import Linglib.Logic.Modal.FirstOrder.Semantics
 
 /-!
-# The correspondence language and the standard translation
-
-The standard translation of quantified modal logic into first-order logic,
-for an arbitrary signature: modal formulas over `L` translate into plain
-mathlib first-order formulas over the correspondence language
-`L.correspondence` — every symbol world-relativized to one arity higher,
-plus a binary accessibility relation and an individual-sort predicate —
-interpreted on the two-sorted-as-one carrier `W ⊕ M`. `realize_st` is
-satisfaction preservation.
-
-## Main declarations
-
-* `Language.correspondence` — the correspondence language of `L`;
-  `ModalStructure.correspondence` — the `W ⊕ M` encoding of a modal
-  structure as one mathlib structure.
-* `ModalFormula.st` — the standard translation, total: the current world is
-  the free variable `Sum.inr k`, and `box` introduces the fresh world
-  variable `Sum.inr (k + 1)`.
-* `realize_st` — satisfaction preservation: Kripke satisfaction at `w` is
-  first-order realization over `correspondence` at any sorted valuation
-  pinning `Sum.inr k` to `w`.
-* `stClose` — sort-guarded existential closure of the current-world
-  variable, turning translations into sentence candidates.
+# The standard translation
+
+The *standard translation* rewrites a modal formula as a first-order formula about worlds and
+individuals, so that results about first-order logic apply to modal logic. A formula over a
+signature `L` becomes a formula over the *correspondence language* of `L`, which has, for each
+symbol of `L`, a symbol taking a world as an extra first argument, together with a binary
+accessibility relation and a predicate true of individuals. Necessity becomes universal
+quantification over the accessible worlds, and the quantifiers range over individuals. A Kripke
+model becomes a single first-order structure whose domain contains both its worlds and its
+individuals, and the translation [preserves satisfaction](##realize_st): a modal formula holds at
+a world exactly when its translation holds with the current-world variable assigned that world.
+
+## Main definitions
+
+* `FirstOrder.Language.correspondence`: the correspondence language of a signature.
+* `FirstOrder.Language.ModalStructure.correspondence`: a Kripke model as one first-order
+  structure on its worlds and individuals.
+* `FirstOrder.Language.ModalFormula.st`: the standard translation.
+* `FirstOrder.Language.stClose`: the existential closure of the current-world variable over
+  worlds.
+
+## Implementation notes
+
+World variables are numbered: the current world is the variable `Sum.inr k`, and necessity
+quantifies the fresh variable `Sum.inr (k + 1)`. Worlds and individuals share the carrier
+`W ⊕ M`, sorted by the predicate true of individuals; an atom applied to arguments of the wrong
+sort is false, and a function symbol applied to them takes a default value.
 
 ## References
 
@@ -41,9 +45,9 @@ variable {W M Var : Type*}
 
 /-! ### The correspondence language -/
 
-/-- The correspondence language of `L` has an `(n + 1)`-ary symbol for
-    each `n`-ary `L`-symbol — the new first argument the world — together
-    with an individual-sort predicate and an accessibility relation. -/
+/-- The correspondence language of `L`: an `(n + 1)`-ary symbol for each `n`-ary symbol of `L`,
+whose first argument is a world, together with a predicate true of individuals and an
+accessibility relation. -/
 def correspondence (L : Language) : Language where
   Functions := fun n ↦ match n with
     | 0 => PEmpty
@@ -58,7 +62,7 @@ abbrev corrFunc (f : L.Functions n) : L.correspondence.Functions (n + 1) := f
 
 abbrev corrRel (R : L.Relations n) : L.correspondence.Relations (n + 1) := Sum.inl R
 
-/-- The individual-sort predicate. -/
+/-- The predicate true of individuals. -/
 abbrev corrIndiv : L.correspondence.Relations 1 := Sum.inr PUnit.unit
 
 /-- The accessibility relation symbol. -/
@@ -70,8 +74,8 @@ abbrev corrWorldVar (k : ℕ) : L.correspondence.Term (Var ⊕ ℕ) := Term.var
 
 /-! ### Sorted valuations -/
 
-/-- The sorted valuation of an individual assignment `v` and a world
-    assignment `u`. `realize_st` evaluates translations at these. -/
+/-- The assignment to individual and world variables given by an assignment `v` of
+individuals and an assignment `u` of worlds. -/
 def stVal (v : Var → M) (u : ℕ → W) : Var ⊕ ℕ → W ⊕ M :=
   Sum.elim (Sum.inr ∘ v) (Sum.inl ∘ u)
 
@@ -93,18 +97,17 @@ theorem stVal_update_world [DecidableEq Var] (v : Var → M) (u : ℕ → W) (j
 
 /-! ### The translation -/
 
-/-- `stTerm` translates terms: a variable stays put; a function symbol
-    applies its world-relativized form at the current world variable. -/
+/-- The translation of terms: a variable is unchanged, and a function symbol takes the current
+world as its first argument. -/
 def stTerm (k : ℕ) : L.Term Var → L.correspondence.Term (Var ⊕ ℕ)
   | .var x => corrIndivVar x
   | .func f args =>
       Term.func (corrFunc f) (Fin.cons (corrWorldVar k) fun i ↦ stTerm k (args i))
 
-/-- The standard translation `ST_k` of [blackburn-derijke-venema-2001].
-    The current world is the free variable `Sum.inr k`; atoms
-    world-relativize; `box` relativizes a fresh world variable
-    `Sum.inr (k + 1)` along accessibility; quantifiers relativize to the
-    individual sort. -/
+/-- The standard translation $ST_k$ [blackburn-derijke-venema-2001], with the current world
+the variable `Sum.inr k`. Atoms take the current world as their first argument, necessity
+quantifies the variable `Sum.inr (k + 1)` over the worlds accessible from the current one, and
+the quantifiers range over individuals. -/
 def ModalFormula.st [DecidableEq Var] (k : ℕ) :
     ModalFormula L Var → L.correspondence.Formula (Var ⊕ ℕ)
   | .equal t₁ t₂ => Term.equal (stTerm k t₁) (stTerm k t₂)
@@ -119,10 +122,10 @@ def ModalFormula.st [DecidableEq Var] (k : ℕ) :
 
 /-! ### Sort-guarded sentence closure -/
 
-/-- `stClose` closes the current-world variable `Sum.inr k` under a
-    sort-guarded existential, `∃z(¬IsIndiv(z) ∧ ψ)`. The guard is
-    load-bearing on the mixed carrier — a bare `ex₁` could be witnessed by
-    a junk individual-as-world, which satisfies `□⊥` vacuously. -/
+/-- The existential closure of the current-world variable `Sum.inr k` over worlds,
+$\exists z \, (\neg \mathrm{Indiv}(z) \land \psi)$. Without the restriction to worlds an
+individual could witness the quantifier, and an individual accesses no world, so it satisfies
+$\Box \bot$. -/
 def stClose [DecidableEq Var] (k : ℕ) (ψ : L.correspondence.Formula (Var ⊕ ℕ)) :
     L.correspondence.Formula (Var ⊕ ℕ) :=
   Formula.ex₁ (Sum.inr k)
@@ -140,11 +143,9 @@ theorem realize_stClose [DecidableEq Var] [L.correspondence.Structure (W ⊕ M)]
 
 variable [Inhabited M] (K : ModalStructure L W M)
 
-/-- `K.correspondence` encodes a modal structure as a single mathlib
-    structure on `W ⊕ M` — the structure half of `Language.correspondence`:
-    worlds and individuals share the carrier, sorted by `corrIndiv`;
-    relational guards make all off-sort atoms false, and off-sort function
-    arguments default. -/
+/-- A Kripke model as one structure for the correspondence language on its worlds and
+individuals. An atom applied to arguments of the wrong sort is false, and a function symbol
+applied to them takes a default value. -/
 @[instance_reducible] def ModalStructure.correspondence :
     L.correspondence.Structure (W ⊕ M) where
   funMap := fun {n} f z ↦ match n, f with
@@ -207,10 +208,9 @@ private theorem realize_stTerm {k : ℕ} {v : Var → M} {u : ℕ → W} :
         (fun i ↦ by simpa [Fin.cons_succ] using realize_stTerm (args i))]
     rfl
 
-/-- The standard translation preserves satisfaction. Kripke satisfaction at the world pinned at
-    index `k` is first-order realization over `K.correspondence` at the sorted valuation. Off-sort
-    quantifier instances are discharged by the relational guards, and `box`'s fresh world variable
-    `k + 1` leaves index `k` untouched. -/
+/-- The standard translation preserves satisfaction: a modal formula holds at a world exactly
+when its translation holds in the model's first-order structure with the current-world variable
+assigned that world. -/
 theorem realize_st [DecidableEq Var] {φ : ModalFormula L Var} {k : ℕ}
     {v : Var → M} {u : ℕ → W} :
     φ.Realize K (u k) v ↔
diff --git a/Linglib/Logic/Modal/FirstOrder/Semantics.lean b/Linglib/Logic/Modal/FirstOrder/Semantics.lean
index 1f326548ea..3d3027ff02 100644
--- a/Linglib/Logic/Modal/FirstOrder/Semantics.lean
+++ b/Linglib/Logic/Modal/FirstOrder/Semantics.lean
@@ -6,35 +6,34 @@ public import Linglib.Logic.Modal.FirstOrder.Syntax
 /-!
 # Constant-domain Kripke semantics
 
-`[UPSTREAM]` candidates for `Mathlib/ModelTheory`, which is classical: one
-structure, no accessibility. A `ModalStructure L W M` — the modal analogue
-of `L.Structure` — is a `W`-indexed family of `L`-structures on a constant
-domain `M` together with `Finset`-valued accessibility; `ModalFormula L α` is the quantified modal
-language in `BoundedFormula`'s basis, and `ModalFormula.Realize` is
-Kripke satisfaction `K, w ⊨_v φ`.
+A Kripke model for quantified modal logic has a set of worlds, an accessibility relation between
+them, and at each world a first-order structure. In a *constant-domain* model every world has
+the same domain of individuals, and only the interpretation of the symbols varies from world to
+world. A formula is satisfied at a world under an assignment of individuals to its free
+variables: atomic formulas are evaluated in the world's structure, necessity quantifies over the
+accessible worlds, and the quantifiers range over the common domain. Because the domain does not
+vary, the [Barcan formula](##realize_barcan) $\forall x \, \Box \varphi \to \Box \forall x \,
+\varphi$ and [its converse](##realize_converseBarcan) hold in every model.
 
-## Main declarations
+## Main definitions
 
-* `ModalStructure` — accessibility plus a world-indexed family of
-  first-order structures on a constant domain, so that terms and plain formulas
-  realize at a world by `Term.realizeAt` and `Formula.RealizeAt`.
-* `ModalFormula.Realize` — Kripke satisfaction for the modal language of
-  `Syntax.lean`, with the `realize_*` simp set and the Barcan laws.
+* `FirstOrder.Language.ModalStructure`: a constant-domain Kripke model.
+* `FirstOrder.Language.ModalFormula.Realize`: satisfaction of a modal formula at a world.
 
 ## Implementation notes
 
-* Accessibility is `Finset`-valued (computability-first, matching the
-  team-semantics consumers); generalize to a `Prop`-valued relation when a
-  consumer needs infinite branching.
-* `ModalFormula` quantifiers bind **named** variables with
-  `Function.update` semantics (the `Formula.all₁` / `ex₁` convention of
-  `Core/ModelTheory/Binders.lean`), not de Bruijn indices: the modal
-  layer's consumers carry named variables.
+* `[UPSTREAM]` candidate for mathlib's `ModelTheory`, whose semantics has one structure and no
+  accessibility relation.
+* Accessibility is `Finset`-valued, for computation, as the team-semantics consumers require; it
+  can be generalized to a `Prop`-valued relation when a consumer needs infinite branching.
+* Quantifiers bind named variables and update the assignment with `Function.update`, as
+  `Formula.all₁` and `Formula.ex₁` of `Core/ModelTheory/Binders.lean` do, rather than de Bruijn
+  indices, since the consumers carry named variables.
 
 ## References
 
-* [fitting-mendelsohn-2023] — constant-domain models, world-relative
-  interpretation, the Barcan formulas
+* [fitting-mendelsohn-2023] — constant-domain models, world-relative interpretation, the Barcan
+  formulas
 -/
 
 @[expose] public section
@@ -43,13 +42,12 @@ namespace FirstOrder.Language
 
 variable {L : Language} {W M α : Type*}
 
-/-- A structure for the quantified modal language — the model object of
-    constant-domain Kripke semantics: `Finset`-valued accessibility plus a
-    `W`-indexed family of `L`-structures on the domain `M`. -/
+/-- A constant-domain Kripke model: an accessibility relation on the worlds `W` and, at each
+world, an `L`-structure on the domain `M`. -/
 structure ModalStructure (L : Language) (W M : Type*) where
-  /-- Accessibility relation (per-world set of accessible worlds). -/
+  /-- The worlds accessible from each world. -/
   access : W → Finset W
-  /-- World-indexed interpretation of the signature. -/
+  /-- The structure at each world. -/
   interp : W → L.Structure M
 
 namespace ModalStructure
@@ -95,8 +93,7 @@ namespace ModalFormula
 
 variable [DecidableEq α]
 
-/-- Kripke satisfaction `K, w ⊨_v φ`, under which atoms evaluate at the world's structure,
-    `□` quantifies over accessible worlds, and named quantifiers update the valuation. -/
+/-- Satisfaction of a modal formula at a world under an assignment, $K, w \vDash_v \varphi$. -/
 def Realize (K : ModalStructure L W M) :
     W → ModalFormula L α → (α → M) → Prop
   | w, .equal t₁ t₂, v => t₁.realizeAt K.interp w v = t₂.realizeAt K.interp w v
@@ -167,8 +164,7 @@ variable (K : ModalStructure L W M) (w : W) (v : α → M)
 
 /-! ### The Barcan laws
 
-Constant domains validate the Barcan formula and its converse: `□` and `∀`
-are both world-independent universal quantifiers, so they commute. -/
+In a constant-domain model necessity and universal quantification commute. -/
 
 theorem realize_barcan (x : α) (φ : ModalFormula L α) :
     (all x (box φ)).Realize K w v → (box (all x φ)).Realize K w v :=
diff --git a/Linglib/Logic/Modal/FirstOrder/Syntax.lean b/Linglib/Logic/Modal/FirstOrder/Syntax.lean
index d57ed2adda..bfb5de9ee8 100644
--- a/Linglib/Logic/Modal/FirstOrder/Syntax.lean
+++ b/Linglib/Logic/Modal/FirstOrder/Syntax.lean
@@ -5,11 +5,24 @@ public import Mathlib.ModelTheory.Syntax
 /-!
 # The quantified modal language
 
-`ModalFormula L α`: modal formulas over `L` with named free variables `α`,
-in mathlib's `BoundedFormula` basis — atomic `equal`/`rel`, `falsum`,
-`imp` — plus `□` and named universal quantification, with `∼`, `⊤`, `⊓`,
-`⊔`, `ex`, and `diamond` derived exactly as for `BoundedFormula`.
-`[UPSTREAM]` candidate for `Mathlib/ModelTheory`.
+Quantified modal logic adds a necessity operator to first-order logic. Its formulas over a
+signature `L`, with free variables in `α`, are built as mathlib's first-order formulas are, from
+equations between terms, relation symbols applied to terms, falsity and implication, together
+with necessity and universal quantification over a named variable. Negation, the other
+connectives, existential quantification and possibility are defined from these exactly as for
+first-order formulas.
+
+## Main definitions
+
+* `FirstOrder.Language.ModalFormula L α`: the formulas of quantified modal logic.
+
+## Implementation notes
+
+`[UPSTREAM]` candidate for mathlib's `ModelTheory`.
+
+## References
+
+* [fitting-mendelsohn-2023]
 -/
 
 @[expose] public section
@@ -18,10 +31,7 @@ namespace FirstOrder.Language
 
 variable {L : Language} {α : Type*}
 
-/-- Modal formulas over `L` with named free variables `α`: mathlib's
-    `BoundedFormula` basis — atomic `equal`/`rel`, `falsum`, `imp` — plus
-    `□` and named quantification; `∼`, `⊤`, `⊓`, `⊔`, `ex`, and `diamond` are
-    derived exactly as for `BoundedFormula`. -/
+/-- A formula of quantified modal logic over `L` with free variables in `α`. -/
 inductive ModalFormula (L : Language) (α : Type*) where
   /-- The proposition that two terms are equal. -/
   | equal (t₁ t₂ : L.Term α) : ModalFormula L α
@@ -52,12 +62,12 @@ instance : Min (ModalFormula L α) := ⟨fun φ ψ => (φ.imp ψ.not).not⟩
 
 instance : Max (ModalFormula L α) := ⟨fun φ ψ => φ.not.imp ψ⟩
 
-/-- Existential quantification of a named variable, derived: `∃x := ∼∀x∼`. -/
+/-- Existential quantification of a named variable, defined as $\neg \forall x \neg$. -/
 @[match_pattern]
 protected def ex (x : α) (φ : ModalFormula L α) : ModalFormula L α :=
   (all x φ.not).not
 
-/-- Possibility, derived: `◇φ := ∼□∼φ` — to `box` what `ex` is to `all`. -/
+/-- Possibility, defined as $\neg \Box \neg$. -/
 @[match_pattern]
 def diamond (φ : ModalFormula L α) : ModalFormula L α := (box φ.not).not
 
diff --git a/Linglib/Semantics/Composition/Extensional.lean b/Linglib/Semantics/Composition/Extensional.lean
new file mode 100644
index 0000000000..d9549fea19
--- /dev/null
+++ b/Linglib/Semantics/Composition/Extensional.lean
@@ -0,0 +1,152 @@
+module
+
+public import Mathlib.Logic.Function.DependsOn
+public import Linglib.Logic.Modal.Defs
+
+/-!
+# Extensional operators
+
+An operator on intensions is *extensional* at an index when the value it yields there depends only
+on the extension of its argument at that index. Negation is extensional: whether *it is not
+raining* is true at a world depends only on whether *it is raining* is true there. Necessity is
+not, since whether *it must be raining* is true at a world depends on whether *it is raining* is
+true at the worlds accessible from it. Among adjectives, which map properties to properties,
+*gray* is extensional and *skillful* is not: where the cobblers are exactly the darts players, the
+gray cobblers are the gray darts players, but the skillful cobblers need not be the skillful darts
+players.
+
+An operator is extensional exactly when it is
+[a function on extensions applied index by index](##isExtensional_iff_exists_eq_piMap). At an
+index where it is extensional, an operator
+[gives the same value on an intension and on the constant intension with the same
+extension](##isExtensionalAt_iff_forall_const), and so
+[cannot tell a variable it binds from one fixed at that index](##isExtensionalAt_iff_forall_diag):
+a situation variable bound under negation reads as if it were free. The truth-functional
+connectives are extensional, and so are composites of extensional operators.
+
+In general the value of an operator at an index depends on its argument at some set of indices,
+and the operator is extensional there when that set can be taken to be the index alone. Necessity
+in a Kripke frame depends at a world on
+[exactly the worlds accessible from it](##ModalLogic.dependsOn_box_iff), so it is
+[extensional only at a world that accesses no world but itself](##isExtensionalAt_box_iff).
+
+## Main definitions
+
+* `Montague.IsExtensionalAt O w`: the value of `O` at `w` depends only on the extension of its
+  argument at `w`.
+* `Montague.IsExtensional O`: `O` is extensional at every index.
+
+## Implementation notes
+
+Extensionality at `w` is the statement that `O · w` factors through evaluation at `w`, and that it
+depends, in the sense of mathlib's `DependsOn`, on the coordinate `w` alone. Kamp's condition for
+an extensional adjective takes a single function on extensions for every index; the function here
+may vary with the index, as in his gloss of the condition and as his claim that every predicative
+adjective is extensional requires.
+
+## References
+
+* [kamp-1975]
+* [zimmermann-2026]
+-/
+
+@[expose] public section
+
+namespace Montague
+
+open Function
+
+variable {W α β γ δ : Type*}
+
+/-- `O` is extensional at `w` when its value at `w` depends on its argument only through the
+argument's extension at `w`. -/
+def IsExtensionalAt (O : (W → α) → W → β) (w : W) : Prop :=
+  ∀ ⦃p q : W → α⦄, p w = q w → O p w = O q w
+
+/-- `O` is extensional when it is extensional at every index. -/
+def IsExtensional (O : (W → α) → W → β) : Prop :=
+  ∀ w, IsExtensionalAt O w
+
+variable {O : (W → α) → W → β} {w : W}
+
+theorem isExtensionalAt_iff_factorsThrough :
+    IsExtensionalAt O w ↔ FactorsThrough (O · w) (· w) :=
+  .rfl
+
+theorem isExtensionalAt_iff_dependsOn : IsExtensionalAt O w ↔ DependsOn (O · w) {w} := by
+  simp [IsExtensionalAt, DependsOn]
+
+theorem not_isExtensionalAt_iff : ¬ IsExtensionalAt O w ↔ ∃ p q, p w = q w ∧ O p w ≠ O q w := by
+  simp [IsExtensionalAt]
+
+/-- An operator is extensional at `w` exactly when it does not distinguish its argument from the
+constant intension with the same extension at `w`. -/
+theorem isExtensionalAt_iff_forall_const :
+    IsExtensionalAt O w ↔ ∀ p, O p w = O (fun _ ↦ p w) w :=
+  ⟨fun h _ ↦ h rfl, fun h p q hpq ↦ by rw [h p, h q, hpq]⟩
+
+theorem isExtensionalAt_iff_exists : IsExtensionalAt O w ↔ ∃ f : α → β, ∀ p, O p w = f (p w) :=
+  ⟨fun h ↦ ⟨fun a ↦ O (fun _ ↦ a) w, fun _ ↦ h rfl⟩, fun ⟨f, hf⟩ p q hpq ↦ by rw [hf, hf, hpq]⟩
+
+/-- An operator is extensional exactly when it applies a function on extensions at each index. -/
+theorem isExtensional_iff_exists_eq_piMap : IsExtensional O ↔ ∃ f : W → α → β, O = Pi.map f :=
+  ⟨fun h ↦ ⟨fun w a ↦ O (fun _ ↦ a) w, funext₂ fun _ w ↦ h w rfl⟩,
+    fun ⟨f, hf⟩ w _ _ hpq ↦ hf ▸ congrArg (f w) hpq⟩
+
+theorem isExtensional_piMap (f : W → α → β) : IsExtensional (Pi.map f) :=
+  isExtensional_iff_exists_eq_piMap.2 ⟨f, rfl⟩
+
+/-- An operator is extensional at `w` exactly when it does not distinguish an argument whose index
+it binds, `fun v ↦ g v v`, from the same argument with the index fixed at `w`, `g w`. -/
+theorem isExtensionalAt_iff_forall_diag :
+    IsExtensionalAt O w ↔ ∀ g : W → W → α, O (fun v ↦ g v v) w = O (g w) w :=
+  ⟨fun h _ ↦ h rfl, fun h ↦ isExtensionalAt_iff_forall_const.2 fun p ↦ h fun u _ ↦ p u⟩
+
+/-! ### Necessity -/
+
+open ModalLogic SetRel in
+theorem isExtensionalAt_box_iff {R : SetRel W W} :
+    IsExtensionalAt □[R] w ↔ ∀ v, w ~[R] v → v = w := by
+  rw [isExtensionalAt_iff_dependsOn, dependsOn_box_iff, Set.subset_singleton_iff]
+  rfl
+
+/-! ### Closure -/
+
+theorem isExtensionalAt_id : IsExtensionalAt (id : (W → α) → W → α) w :=
+  fun _ _ ↦ id
+
+theorem isExtensionalAt_const (c : W → β) : IsExtensionalAt (fun _ : W → α ↦ c) w :=
+  fun _ _ _ ↦ rfl
+
+theorem isExtensionalAt_not : IsExtensionalAt (fun (p : W → Prop) v ↦ ¬ p v) w :=
+  fun _ _ ↦ congrArg Not
+
+namespace IsExtensionalAt
+
+theorem comp {O' : (W → β) → W → γ} (h' : IsExtensionalAt O' w) (h : IsExtensionalAt O w) :
+    IsExtensionalAt (O' ∘ O) w :=
+  fun _ _ hpq ↦ h' (h hpq)
+
+theorem comp_left (h : IsExtensionalAt O w) (g : β → γ) :
+    IsExtensionalAt (fun p v ↦ g (O p v)) w :=
+  fun _ _ hpq ↦ congrArg g (h hpq)
+
+theorem comp₂ {O' : (W → α) → W → γ} (h : IsExtensionalAt O w) (h' : IsExtensionalAt O' w)
+    (g : β → γ → δ) : IsExtensionalAt (fun p v ↦ g (O p v) (O' p v)) w :=
+  fun _ _ hpq ↦ congrArg₂ g (h hpq) (h' hpq)
+
+theorem not {O : (W → α) → W → Prop} (h : IsExtensionalAt O w) :
+    IsExtensionalAt (fun p v ↦ ¬ O p v) w :=
+  h.comp_left Not
+
+theorem and {O O' : (W → α) → W → Prop} (h : IsExtensionalAt O w) (h' : IsExtensionalAt O' w) :
+    IsExtensionalAt (fun p v ↦ O p v ∧ O' p v) w :=
+  h.comp₂ h' And
+
+theorem or {O O' : (W → α) → W → Prop} (h : IsExtensionalAt O w) (h' : IsExtensionalAt O' w) :
+    IsExtensionalAt (fun p v ↦ O p v ∨ O' p v) w :=
+  h.comp₂ h' Or
+
+end IsExtensionalAt
+
+end Montague
diff --git a/Linglib/Semantics/Modification/Classification.lean b/Linglib/Semantics/Modification/Classification.lean
index 4969b88f9e..a0847a864c 100644
--- a/Linglib/Semantics/Modification/Classification.lean
+++ b/Linglib/Semantics/Modification/Classification.lean
@@ -5,7 +5,7 @@ public import Linglib.Semantics.Reference.Rigidity
 public import Mathlib.Order.PropInstances
 public import Mathlib.Data.Set.Basic
 public import Mathlib.Tactic.Common
-public import Linglib.Logic.Modal.Extensional
+public import Linglib.Semantics.Composition.Extensional
 
 /-!
 # Modifiers of intensional properties
@@ -62,10 +62,8 @@ theorem isPrivative_iff_forall :
 
 /-- Intersective modifiers are extensional, since the meet with a fixed property reads the noun
 only through its extension at each world. -/
-theorem IsIntersective.isExtensional (h : IsIntersective adj) : ModalLogic.IsExtensional adj := by
-  obtain ⟨Q, hQ⟩ := h
-  intro w N₁ N₂ hN
-  simp only [hQ, Pi.inf_apply, hN]
+theorem IsIntersective.isExtensional (h : IsIntersective adj) : Montague.IsExtensional adj :=
+  h.elim fun Q hQ ↦ Montague.isExtensional_iff_exists_eq_piMap.2 ⟨fun w ↦ (Q w ⊓ ·), funext hQ⟩
 
 /-- A privative modifier that holds of something is not subsective. -/
 theorem IsPrivative.not_isSubsective (hp : IsPrivative adj) (hne : ∃ N w x, adj N w x) :
diff --git a/Linglib/Semantics/Reference/Rigidity.lean b/Linglib/Semantics/Reference/Rigidity.lean
index 696068de35..6e43501d6f 100644
--- a/Linglib/Semantics/Reference/Rigidity.lean
+++ b/Linglib/Semantics/Reference/Rigidity.lean
@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Logic.Function.Basic
 public import Mathlib.Data.Set.Image
+public import Linglib.Semantics.Composition.Extensional
 
 /-!
 # Rigid designation
@@ -21,8 +22,9 @@ of identity.
 An operator `O` governing the predication of `P` of a designator `f` has a large scope reading,
 which evaluates `f` at the index of the whole sentence, and a small scope reading, which
 evaluates it at each index the operator reaches. The large scope reading of `f` is the small
-scope reading of the designator whose reference `f` fixes at that index, so the two readings
-coincide for a rigid designator.
+scope reading of the designator whose reference `f` fixes at that index. The two readings
+coincide when `f` is constant on the indices on which the operator's value depends: under every
+operator when `f` is rigid, and for every designator when the operator is extensional.
 
 ## Main definitions
 
@@ -35,7 +37,11 @@ coincide for a rigid designator.
 * `isRigid_iff_subsingleton_range`: the mathlib face.
 * `IsRigid.eq_of_apply_eq`: the necessity of identity.
 * `largeScope_eq_smallScope_const`: the large scope reading as fixing the reference.
+* `largeScope_eq_smallScope_of_dependsOn`: the scope readings coincide for a designator constant
+  on the indices the operator reads.
 * `largeScope_eq_smallScope`: the scope readings coincide for a rigid designator.
+* `Montague.IsExtensionalAt.largeScope_eq_smallScope`: the scope readings coincide under an
+  extensional operator.
 
 ## References
 
@@ -97,6 +103,20 @@ theorem largeScope_eq_smallScope_const (O : (W → Prop) → W → Prop) (P : τ
     (f : W → τ) (w : W) : largeScope O P f w = smallScope O P (fun _ ↦ f w) w :=
   rfl
 
+/-- The two scope readings of `f` coincide at `w` when `f` is constant on a set of indices on
+which the operator's value at `w` depends. -/
+theorem largeScope_eq_smallScope_of_dependsOn {O : (W → Prop) → W → Prop} {s : Set W} {w : W}
+    (hO : DependsOn (O · w) s) (hf : Set.EqOn f (fun _ ↦ f w) s) (P : τ → W → Prop) :
+    largeScope O P f w = smallScope O P f w :=
+  hO fun v hv ↦ congrArg (P · v) (hf hv).symm
+
 theorem largeScope_eq_smallScope (h : IsRigid f) (O : (W → Prop) → W → Prop)
     (P : τ → W → Prop) : largeScope O P f = smallScope O P f :=
-  funext fun w ↦ (congrArg (smallScope O P · w) (h.eq_const w)).symm
+  funext fun w ↦ largeScope_eq_smallScope_of_dependsOn (dependsOn_univ _) (fun v _ ↦ h v w) P
+
+/-- The two scope readings of every designator coincide under an operator extensional at `w`. -/
+theorem Montague.IsExtensionalAt.largeScope_eq_smallScope {O : (W → Prop) → W → Prop} {w : W}
+    (h : Montague.IsExtensionalAt O w) (P : τ → W → Prop) (f : W → τ) :
+    largeScope O P f w = smallScope O P f w :=
+  largeScope_eq_smallScope_of_dependsOn (Montague.isExtensionalAt_iff_dependsOn.1 h)
+    (Set.eqOn_singleton.2 rfl) P
diff --git a/Studies/Kamp1975.lean b/Studies/Kamp1975.lean
index 63a4f04a81..d08aae1846 100644
--- a/Studies/Kamp1975.lean
+++ b/Studies/Kamp1975.lean
@@ -5,7 +5,7 @@ public import Linglib.Logic.Trivalent.Basic
 public import Mathlib.Data.Set.Basic
 public import Mathlib.Algebra.Order.Ring.Rat
 public import Mathlib.Algebra.Order.BigOperators.Group.Finset
-public import Linglib.Logic.Modal.Extensional
+public import Linglib.Semantics.Composition.Extensional
 
 /-!
 # Kamp (1975): Two theories about adjectives
@@ -28,6 +28,14 @@ two agree. Before this, Kamp argues that no many-valued logic handles borderline
   asymmetric, and the witness shows the incomparability and the forced verdict, not the
   paper's specific outcome.
 
+## Errata
+
+* Definition (7) asks for a single function $F'$ on extensions with $F(P)(w) = F'(P(w))$ at
+  every world, while the gloss after it and the claim that every predicative adjective is
+  extensional need $F'$ to vary with the world. A predicative adjective whose property differs
+  between worlds, such as `grayAdj`, satisfies (4) and the gloss but not (7) as printed. The
+  study reads (7) by its gloss, `Montague.IsExtensional`.
+
 ## References
 
 * [kamp-1975]
@@ -224,35 +232,38 @@ inductive W2 | w₁ | w₂
 /-- Three entities suffice for all witness constructions. -/
 inductive E3 | a | b | c
 
--- UNVERIFIED: Kamp's definition numbers (4)–(6) below; the paper is not available to check.
-
-/-- *gray* is predicative, Kamp's definition (4), since it conjoins a fixed property with the
-noun, so *gray cat* entails both *gray* and *cat*. -/
-def grayAdj : Modifier (W2 → E3 → Prop) := fun N w x ↦
-  (match x with | .a => True | _ => False) ∧ N w x
+/-- *gray* is predicative, Kamp's definition (4) (p. 124), since it conjoins a property with the
+noun, so *gray cat* entails both *gray* and *cat*. Only `a` is gray, and only at `w₁`. -/
+def grayAdj : Modifier (W2 → E3 → Prop) := fun N w x ↦ (w = .w₁ ∧ x = .a) ∧ N w x
 
-/-- Each class has a member, and extensionality is independent of subsectivity. -/
 theorem gray_intersective : IsIntersective grayAdj :=
-  Modifier.isIntersective_iff_exists_forall.mpr
-    ⟨fun _ x ↦ match x with | .a => True | _ => False,
-     fun N w x ↦ by cases x <;> simp [grayAdj]⟩
+  ⟨fun w x ↦ w = .w₁ ∧ x = .a, fun _ ↦ rfl⟩
 
 /-- *gray* is therefore also extensional and subsective. -/
-example : ModalLogic.IsExtensional grayAdj :=
+example : Montague.IsExtensional grayAdj :=
   Modifier.IsIntersective.isExtensional gray_intersective
 example : IsSubsective grayAdj := gray_intersective.isSubsective
 
-/-- *fake* is privative, Kamp's definition (5), so *fake gun* entails *not a gun*. Kamp doubts
-that any English adjective is privative "in all of its possible uses". -/
+/-- No single function on extensions gives *gray*, so the predicative *gray* is not extensional by
+(7) as printed (p. 125). -/
+theorem not_exists_forall_grayAdj_eq :
+    ¬ ∃ F' : (E3 → Prop) → E3 → Prop, ∀ N w, grayAdj N w = F' (N w) := by
+  rintro ⟨F', hF'⟩
+  have h := (congrFun (hF' (fun _ _ ↦ True) .w₁) .a).trans
+    (congrFun (hF' (fun _ _ ↦ True) .w₂) .a).symm
+  simp [grayAdj] at h
+
+/-- *fake* is privative, Kamp's definition (5) (p. 125), so *fake gun* entails *not a gun*. Kamp
+doubts that any English adjective is privative "in all of its possible uses". -/
 def fakeAdj : Modifier (W2 → E3 → Prop) := fun N w x ↦
   (match x with | .b => True | _ => False) ∧ ¬ N w x
 
 theorem fake_privative : IsPrivative fakeAdj :=
   Modifier.isPrivative_iff_forall.mpr fun _ _ _ h ↦ h.2
 
-/-- *skillful* is affirmative, Kamp's definition (6), but not extensional. A skillful surgeon
-is a surgeon, yet skill depends on the noun's intension and not just its current extension, as
-in the case of cobblers and darts players that Kamp credits to Lewis. -/
+/-- *skillful* is affirmative, Kamp's definition (6) (p. 125), but not extensional (7). A
+skillful surgeon is a surgeon, yet skill depends on the noun's intension and not just its current
+extension, as in the case of cobblers and darts players that Kamp credits to Lewis. -/
 def skillfulAdj : Modifier (W2 → E3 → Prop) := fun N w x ↦
   N w x ∧ match x with
     | .a => N .w₁ .a  -- a's skill assessment depends on N's intension
@@ -261,7 +272,7 @@ def skillfulAdj : Modifier (W2 → E3 → Prop) := fun N w x ↦
 theorem skillful_subsective : IsSubsective skillfulAdj :=
   fun _ _ _ h ↦ h.1
 
-theorem skillful_not_extensional : ¬ ModalLogic.IsExtensional skillfulAdj := by
+theorem skillful_not_extensional : ¬ Montague.IsExtensional skillfulAdj := by
   intro hext
   let N₁ : W2 → E3 → Prop := fun _ _ ↦ True
   let N₂ : W2 → E3 → Prop := fun w x ↦ match w, x with
@@ -269,16 +280,16 @@ theorem skillful_not_extensional : ¬ ModalLogic.IsExtensional skillfulAdj := by
     | _, _    => True
   have hagree : N₁ .w₂ = N₂ .w₂ := by
     funext x; cases x <;> simp [N₁, N₂]
-  have h := hext .w₂ N₁ N₂ hagree
+  have h := hext .w₂ hagree
   have hLHS : skillfulAdj N₁ .w₂ .a := ⟨trivial, trivial⟩
   exact (congrFun h .a ▸ hLHS).2
 
-/-- *alleged* satisfies no meaning postulate, Kamp's opening example (1) being that *every
-alleged thief is a thief* is no logical truth. -/
+/-- *alleged* satisfies no meaning postulate, Kamp's opening example (1) (p. 123) being that
+*every alleged thief is a thief* is no logical truth. -/
 def allegedAdj : Modifier (W2 → E3 → Prop) := fun _N _ x ↦
   match x with | .a => True | _ => False
 
-theorem alleged_extensional : ModalLogic.IsExtensional allegedAdj :=
+theorem alleged_extensional : Montague.IsExtensional allegedAdj :=
   fun _ _ _ _ ↦ rfl
 
 /-- *alleged N* does not entail *N*. -/
diff --git a/Studies/Kripke1980.lean b/Studies/Kripke1980.lean
index 219a9ab1cd..5e44ce7e6b 100644
--- a/Studies/Kripke1980.lean
+++ b/Studies/Kripke1980.lean
@@ -80,7 +80,7 @@ theorem forall_largeScope_box_iff_smallScope_box_iff :
     (∀ P, largeScope □[R] P t w ↔ smallScope □[R] P t w) ↔
       Set.EqOn t (fun _ ↦ t w) {v | w ~[R] v} :=
   ⟨fun h v hv ↦ (h fun e _ ↦ e = t w).1 (fun _ _ ↦ rfl) v hv, fun h _ ↦
-    forall₂_congr fun _ hv ↦ by simp only [h hv]⟩
+    iff_of_eq (largeScope_eq_smallScope_of_dependsOn (dependsOn_box_iff.2 subset_rfl) h _)⟩
 
 theorem isRigid_iff_largeScope_eq_smallScope :
     IsRigid t ↔ ∀ P, largeScope □[Set.univ] P t = smallScope □[Set.univ] P t :=
diff --git a/Studies/Zimmermann2026.lean b/Studies/Zimmermann2026.lean
index aaad522d4c..a3f8ce5ebb 100644
--- a/Studies/Zimmermann2026.lean
+++ b/Studies/Zimmermann2026.lean
@@ -2,7 +2,7 @@ module
 
 public import Studies.Owusu2022
 public import Studies.Zimmermann2008
-public import Linglib.Logic.Modal.Extensional
+public import Linglib.Semantics.Reference.Rigidity
 
 /-!
 # Zimmermann (2026): African Lambdas I, The Nominal Domain
@@ -57,13 +57,19 @@ theorem bi_reading_not_narrow {S E : Type*} (f : S → ChoiceFunction E) {s : S}
   have h' := (Owusu2022.negation_narrow_iff f ⟨a, ha⟩).mp h
   hab ((h' a ha).trans (h' b hb).symm)
 
-/-- Under negation, the bound and free construals of the situation argument of *bí* coincide, as the
-explanation of (15) requires. -/
-theorem bi_negation_construals_collapse {S E : Type*}
-    (f : S → ChoiceFunction E) (s₀ : S) (P : S → E → Prop) (VP : E → S → Prop) :
-    (fun p s ↦ ¬ p s) (fun s ↦ VP (f s (P s)) s) s₀ ↔
-      (fun p s ↦ ¬ p s) (fun s ↦ VP (f s₀ (P s₀)) s) s₀ :=
-  iff_of_eq <| ModalLogic.isExtensionalAt_iff_forall_diag.mp ModalLogic.IsExtensionalAt.neg
-    fun σ s ↦ VP (f σ (P σ)) s
+/-- Under an operator that is not intensional, such as negation, the bound and free construals of
+the situation argument of *bí* (16a) coincide, so that the operator cannot shift it, as the
+explanation of (15) requires (p. 7). -/
+theorem bi_construals_collapse {S E : Type*} {O : (S → Prop) → S → Prop} {s₀ : S}
+    (hO : Montague.IsExtensionalAt O s₀) (f : S → ChoiceFunction E) (P : S → E → Prop)
+    (VP : E → S → Prop) :
+    smallScope O VP (fun s ↦ f s (P s)) s₀ = largeScope O VP (fun s ↦ f s (P s)) s₀ :=
+  (hO.largeScope_eq_smallScope VP _).symm
+
+example {S E : Type*} (f : S → ChoiceFunction E) (s₀ : S) (P : S → E → Prop)
+    (VP : E → S → Prop) :
+    smallScope (fun p s ↦ ¬ p s) VP (fun s ↦ f s (P s)) s₀ =
+      largeScope (fun p s ↦ ¬ p s) VP (fun s ↦ f s (P s)) s₀ :=
+  bi_construals_collapse Montague.isExtensionalAt_not f P VP
 
 end Zimmermann2026
diff --git a/references.bib b/references.bib
index 43a2247145..f9752c7925 100644
--- a/references.bib
+++ b/references.bib
@@ -5006,7 +5006,7 @@ @book{gallin-1975
   role      = {cited},
   doi       = {10.1016/s0304-0208(08)x7029-x},
   validated = {true},
-  sources   = {Semantics/Intensional/Rigidity.lean;Semantics/Intensional/Algebra.lean;Semantics/Intensional/Defs.lean;Core/Logic/Temporal/Basic.lean;Core/Logic/Modal/Basic.lean}
+  sources   = {Logic/Modal/Basic.lean;Logic/Temporal/Basic.lean;Semantics/Composition/Ty.lean;Semantics/Reference/Rigidity.lean}
 }
 @inproceedings{kagan-alexeyenko-2011,
   author    = {Kagan, Olga and Alexeyenko, Sascha},
@@ -5033,7 +5033,7 @@ @incollection{kamp-1975
   role      = {cited},
   doi       = {10.1017/cbo9780511897696.011},
   validated = {true},
-  sources   = {Semantics/Degree/Delineation.lean;Semantics/Modification/Basic.lean;Semantics/Modification/Classification.lean;Studies/ChatzikyriakidisLuo2020.lean;Studies/DAmbrosioHedden2024.lean;Studies/DelPinal2015.lean;Studies/Elbourne2026.lean;Studies/Fine1975.lean;Studies/Kamp1975.lean;Studies/Klein1980.lean;Studies/Partee2010.lean}
+  sources   = {Semantics/Composition/Extensional.lean;Semantics/Degree/Delineation.lean;Semantics/Modification/Basic.lean;Semantics/Modification/Classification.lean;Studies/ChatzikyriakidisLuo2020.lean;Studies/DAmbrosioHedden2024.lean;Studies/DelPinal2015.lean;Studies/Elbourne2026.lean;Studies/Fine1975.lean;Studies/Kamp1975.lean;Studies/Klein1980.lean;Studies/Partee2010.lean}
 }
 @book{huddleston-pullum-2002,
   author    = {Huddleston, Rodney and Pullum, Geoffrey K.},
@@ -10128,7 +10128,7 @@ @book{fitting-mendelsohn-2023
   subfield  = {semantics/modality},
   validated = {true},
   role      = {cited},
-  sources   = {Logic/Modal/FirstOrder/Semantics.lean}
+  sources   = {Logic/Modal/FirstOrder/Semantics.lean;Logic/Modal/FirstOrder/Syntax.lean}
 }
 
 @book{blackburn-derijke-venema-2001,
@@ -34836,7 +34836,7 @@ @article{zimmermann-2026
   doi       = {10.1111/lnc3.70025},
   subfield  = {semantics/nominal},
   role      = {formalized},
-  sources   = {Studies/Zimmermann2026.lean}
+  sources   = {Semantics/Composition/Extensional.lean;Studies/Zimmermann2026.lean}
 }
 @book{matthewson-2008,
   editor    = {Matthewson, Lisa},