refactor(Semantics/Composition): a type of worlds, intensions from it

Linglib/Logic/Modal/Basic.lean

@@ -8,20 +8,14 @@ public import Mathlib.Order.Lattice
 /-!
 # 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.
+[Necessity is antitone in the accessibility relation](##box_restrict), so a conversational
+background that rules out more worlds yields a stronger modal, and necessity along the transitive
+closure of a relation [is the infinite conjunction](##box_transGen_iff)
+$\Box p \land \Box \Box p \land \cdots$, the shape of common knowledge. An operator on
+propositions is *indicial* when it is necessity along some accessibility relation, after Gallin:
+Montague's necessity is the indicial operator of the universal relation, and Scott's present
+progressive is not indicial. Along a serial relation $\Box p$, $\Box \neg p$, $\Diamond p$ and
+$\neg \Box p$ [form a square of opposition](##modalSquare_relations).
 
 ## Main definitions
 

Linglib/Logic/Modal/Defs.lean

@@ -8,26 +8,14 @@ public import Mathlib.Logic.Function.DependsOn
 # 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,
+accessible from it, and *possible* when it is true at some; the accessibility relation fixes the
+kind of modality. Each of the axioms T, D, B, 4 and 5 holds along a relation
+[exactly when the relation is reflexive](##box_T_iff), serial, symmetric, transitive or Euclidean
+respectively. Possibility is [left adjoint to necessity along the converse
+relation](##diamond_box_gc), necessity at a world
+[depends on exactly the worlds it accesses](##dependsOn_box_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).
+[exactly when the relation is the graph of a function](##box_compl_eq_iff).
 
 ## Main definitions
 

Linglib/Logic/Modal/Epistemic.lean

@@ -6,21 +6,13 @@ public import Linglib.Logic.Modal.Basic
 /-!
 # 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.
+In epistemic logic an agent *knows* a proposition at a world when it is true at every world the
+agent cannot tell apart from it. A group's *everyone*, *distributed* and *common knowledge* are
+necessity along the union, the intersection and the transitive closure of the union of its
+members' relations, and common knowledge [is the infinite conjunction of iterated knowledge by
+everyone](##commonKnowledge_iff_forall_iterate). 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
 

Linglib/Logic/Modal/FirstOrder/Correspondence.lean

@@ -7,14 +7,10 @@ public import Linglib.Logic.Modal.FirstOrder.Semantics
 # 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.
+individuals, over the *correspondence language*, which gives each symbol a world argument and adds
+an accessibility relation and a predicate true of individuals. Necessity becomes quantification
+over the accessible worlds, a Kripke model becomes one first-order structure on its worlds and
+individuals, and the translation [preserves satisfaction](##realize_st).
 
 ## Main definitions
 

Linglib/Logic/Modal/FirstOrder/Semantics.lean

@@ -6,13 +6,10 @@ public import Linglib.Logic.Modal.FirstOrder.Syntax
 /-!
 # Constant-domain Kripke semantics
 
-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 \,
+A *constant-domain* Kripke model for quantified modal logic has a set of worlds, an accessibility
+relation between them, and at each world a first-order structure on one shared domain of
+individuals. Necessity quantifies over the accessible worlds and the quantifiers over the shared
+domain, so the [Barcan formula](##realize_barcan) $\forall x \, \Box \varphi \to \Box \forall x \,
 \varphi$ and [its converse](##realize_converseBarcan) hold in every model.
 
 ## Main definitions

Linglib/Semantics/Composition/Coordinator.lean

@@ -13,18 +13,14 @@ constituents is the case of a two-element set, so one operation conjoins truth v
 predicates and generalized quantifiers, coordinates lists of any length, and builds the
 quantifiers that Japanese *ka* and *mo* form from indeterminate pronouns. The composition engine
 applies it to two sisters of one conjoinable type in `Semantics/Composition/Coordination.lean`.
+[Coordinating a constituent alone returns it](##denote_singleton), as
+[coordinating it with itself does](##denote_pair_self), except under negative coordination, and
+[the coordination of functions is computed pointwise](##denote_apply).
 
 ## Main definitions
 
 * `Coordinator.denote`: what a coordinator denotes on a set of coordinands.
 
-## Main results
-
-* `Coordinator.denote_of_conjunctive` and its siblings: the denotation by semantic type.
-* `Coordinator.denote_singleton`, `Coordinator.denote_pair_self`: coordinating a constituent
-  alone or with itself returns it, except under negative coordination.
-* `Coordinator.denote_apply`: the coordination of functions is computed pointwise.
-
 ## Implementation notes
 
 The denotation is the truth-conditional content only. The contrast an adversative coordinator

Linglib/Semantics/Composition/FirstOrder.lean

@@ -101,14 +101,25 @@ so that terms and bounded formulas share it. -/
 
 /-- In the syntactic model of the types over the free variables `α`, with `n` bound variables in
 scope, an entity is a term, and a truth value and a function are given at every larger number of
-bound variables, as a bounded formula and as a function on the values there. -/
+bound variables, as a bounded formula and as a function on the values there. The other sorts,
+worlds among them, are trivial, so an intension is a function that ignores its world. -/
 abbrev Ty.SyntacticDomain (L : Language.{u, u}) (α : Type w) : Ty → ℕ → Type (max u w)
   | .e, i => L.Term (α ⊕ Fin i)
   | .t, i => ∀ k, i ≤ k → L.BoundedFormula α k
   | .fn σ τ, i => ∀ k, i ≤ k → Ty.SyntacticDomain L α σ k → Ty.SyntacticDomain L α τ k
-  | .intens σ, i => Ty.SyntacticDomain L α σ i
   | _, _ => PUnit
 
+/-- A value of the syntactic model with `i` bound variables in scope, carried to `k ≥ i`. -/
+def Ty.SyntacticDomain.mono {L : Language.{u, u}} {α : Type w} :
+    (ty : Ty) → {i k : ℕ} → i ≤ k → Ty.SyntacticDomain L α ty i → Ty.SyntacticDomain L α ty k
+  | .e, _, _, h, x => x.relabel (Sum.map id (Fin.castLE h))
+  | .t, _, _, h, φ => fun j hj ↦ φ j (h.trans hj)
+  | .fn _ _, _, _, h, f => fun j hj ↦ f j (h.trans hj)
+  | .d, _, _, _, x => x
+  | .n, _, _, _, x => x
+  | .v, _, _, _, x => x
+  | .s, _, _, _, x => x
+
 /-- A predicate of the syntactic model applied to the next bound variable, with `j + 1` bound
 variables in scope, as a determiner applies its restrictor and scope to the variable it binds. -/
 def Ty.SyntacticDomain.applyNext {L : Language.{u, u}} {α : Type w} {k j : ℕ}
@@ -119,7 +130,7 @@ def Ty.SyntacticDomain.applyNext {L : Language.{u, u}} {α : Type w} {k j : ℕ}
 under a valuation `v` of the free variables and `xs` of the `n` bound ones. A term realizes the
 entity it denotes, a formula realizes a truth value with `xs` extended to any larger number of
 bound variables, a function realizes a function that sends realized arguments to realized values
-with `xs` so extended, and an intension is realized at every world. -/
+with `xs` so extended. -/
 def Ty.Realizes {L : Language.{u, u}} {α : Type w} {M W : Type} {Q : Sorts} (S : L.Structure M)
     (v : α → M) :
     (ty : Ty) → (n : ℕ) → (Fin n → M) → Ty.SyntacticDomain L α ty n → Ty.Domain M W ty Q → Prop
@@ -128,7 +139,6 @@ def Ty.Realizes {L : Language.{u, u}} {α : Type w} {M W : Type} {Q : Sorts} (S
       (letI := S; (φ k hk).Realize v ys ↔ p)
   | .fn σ τ, i, xs, f, f' => ∀ k (hk : i ≤ k) (ys : Fin k → M), ys ∘ Fin.castLE hk = xs →
       ∀ x a, Ty.Realizes S v σ k ys x a → Ty.Realizes S v τ k ys (f k hk x) (f' a)
-  | .intens σ, i, xs, x, a => ∀ w, Ty.Realizes S v σ i xs x (a w)
   | _, _, _, _, _ => True
 
 section SyntacticModel
@@ -140,15 +150,15 @@ section Readback
 variable {α : Type w}
 
 /-- In the syntactic model a mode applies at the current number of bound variables, the
-intensional modes to the argument itself, and predicate modification and event identification
-conjoin pointwise. -/
+intensional modes to the argument carried to every larger number, and predicate modification and
+event identification conjoin pointwise. -/
 def Mode.readback {σ₁ σ₂ τ : Ty} {n : ℕ} :
     Mode σ₁ σ₂ τ → Ty.SyntacticDomain L α σ₁ n → Ty.SyntacticDomain L α σ₂ n →
       Ty.SyntacticDomain L α τ n
   | .functionalLeft, f, a => f n le_rfl a
   | .functionalRight, a, f => f n le_rfl a
-  | .intensionalLeft, f, a => f n le_rfl a
-  | .intensionalRight, a, f => f n le_rfl a
+  | .intensionalLeft, f, a => f n le_rfl fun _ hk _ ↦ Ty.SyntacticDomain.mono _ hk a
+  | .intensionalRight, a, f => f n le_rfl fun _ hk _ ↦ Ty.SyntacticDomain.mono _ hk a
   | .predicateModification, p, q => fun k hk x j hj ↦ p k hk x j hj ⊓ q k hk x j hj
   | .eventIdentificationLeft, f, p => fun k hk x j hj e i hi ↦
       f k hk x j hj e i hi ⊓ p j (hk.trans hj) e i hi
@@ -216,6 +226,19 @@ private theorem realize_relabel_castLE {n k : ℕ} (hk : n ≤ k) (x : L.Term (
       x.realize (Sum.elim v (ys ∘ Fin.castLE hk)) := by
   rw [Term.realize_relabel, Sum.elim_comp_map, Function.comp_id]
 
+theorem Ty.Realizes.mono {ty : Ty} {n k : ℕ} {xs : Fin n → M} {x : Ty.SyntacticDomain L α ty n}
+    {a : Ty.Domain M W ty Q} (h : Ty.Realizes S v ty n xs x a) (hk : n ≤ k) {ys : Fin k → M}
+    (hys : ys ∘ Fin.castLE hk = xs) :
+    Ty.Realizes S v ty k ys (Ty.SyntacticDomain.mono ty hk x) a := by
+  cases ty with
+  | e =>
+    change (letI := S; (x.relabel (Sum.map id (Fin.castLE hk))).realize (Sum.elim v ys)) = a
+    rw [realize_relabel_castLE S v hk x ys, hys]
+    exact h
+  | t => exact fun j hj zs hzs ↦ h j (hk.trans hj) zs (comp_castLE_trans hys hzs)
+  | fn σ τ => exact fun j hj zs hzs ↦ h j (hk.trans hj) zs (comp_castLE_trans hys hzs)
+  | _ => trivial
+
 private theorem realize_applyNext {k j : ℕ} {ys : Fin k → M}
     {P : Ty.SyntacticDomain L α (.e ⇒ .t) k}
     {P' : Ty.Domain M W (.e ⇒ .t) Q} (hP : Ty.Realizes S v (.e ⇒ .t) k ys P P') (h : k ≤ j)
@@ -234,8 +257,10 @@ theorem Mode.realizes_readback {σ₁ σ₂ τ : Ty} (μ : Mode σ₁ σ₂ τ)
   cases μ with
   | functionalLeft => exact ha n le_rfl xs rfl b b' hb
   | functionalRight => exact hb n le_rfl xs rfl a a' ha
-  | intensionalLeft => exact ha n le_rfl xs rfl b (fun _ ↦ b') fun _ ↦ hb
-  | intensionalRight => exact hb n le_rfl xs rfl a (fun _ ↦ a') fun _ ↦ ha
+  | intensionalLeft =>
+    exact ha n le_rfl xs rfl _ (fun _ ↦ b') fun _ hk _ hys _ _ _ ↦ hb.mono S v hk hys
+  | intensionalRight =>
+    exact hb n le_rfl xs rfl _ (fun _ ↦ a') fun _ hk _ hys _ _ _ ↦ ha.mono S v hk hys
   | predicateModification =>
     intro k hk ys hys x c hx j hj zs hzs
     simp only [Mode.readback, Mode.eval, BoundedFormula.realize_inf,

Linglib/Semantics/Composition/Partial.lean

@@ -57,8 +57,8 @@ abbrev Ty.PDomain (E W : Type) (ty : Ty) (S : Sorts := {}) : Type :=
   | .d => S.degree
   | .n => ℕ
   | .v => S.eventuality
+  | .s => W
   | .fn a b => Ty.PDomain E W a S →. Ty.PDomain E W b S
-  | .intens a => W →. Ty.PDomain E W a S
 
 /-- A partial denotation is a semantic type with a possibly undefined value in its partial
 domain. -/
@@ -167,8 +167,8 @@ def Ty.Lifts : (ty : Ty) → Ty.Domain E W ty S → Ty.PDomain E W ty S → Prop
   | .d, x, y => x = y
   | .n, x, y => x = y
   | .v, x, y => x = y
+  | .s, x, y => x = y
   | .fn a b, f, f' => ∀ x y, Ty.Lifts a x y → ∃ z, f' y = Part.some z ∧ Ty.Lifts b (f x) z
-  | .intens a, f, f' => ∀ w, ∃ z, f' w = Part.some z ∧ Ty.Lifts a (f w) z
 
 @[simp] theorem Ty.lifts_e {x y : E} : Ty.Lifts (E := E) (W := W) (S := S) .e x y ↔ x = y :=
   Iff.rfl
@@ -214,15 +214,16 @@ def Ty.Domain.toPartial : (ty : Ty) → Ty.Domain E W ty S → Ty.PDomain E W ty
   | .d, x => x
   | .n, x => x
   | .v, x => x
+  | .s, x => x
   | .fn .e b, f => PFun.lift fun x ↦ toPartial b (f x)
-  | .fn _ _, _ => fun _ ↦ Part.none
   | .intens a, f => PFun.lift fun w ↦ toPartial a (f w)
+  | .fn _ _, _ => fun _ ↦ Part.none
 
 theorem Ty.lifts_toPartial {ty : Ty} (h : ty.FirstOrder) (x : Ty.Domain E W ty S) :
     Ty.Lifts ty x (Ty.Domain.toPartial ty x) := by
   induction h with
   | fn _ ih => exact Ty.lifts_lift fun x ↦ ih _
-  | intens _ ih => exact fun w ↦ ⟨_, rfl, ih _⟩
+  | intens _ ih => exact fun _ _ hw ↦ ⟨_, hw ▸ rfl, ih _⟩
   | _ => rfl
 
 /-- The partial denotation a total one lifts to. -/
@@ -244,9 +245,11 @@ theorem Mode.lifts_evalPartial {σ₁ σ₂ τ : Ty} (m : Mode σ₁ σ₂ τ) {
   | functionalLeft => simpa [evalPartial, eval] using ha b b' hb
   | functionalRight => simpa [evalPartial, eval] using hb a a' ha
   | intensionalLeft =>
-    simpa [evalPartial, eval] using ha (fun _ ↦ b) (fun _ ↦ Part.some b') fun _ ↦ ⟨b', rfl, hb⟩
+    simpa [evalPartial, eval] using
+      ha (fun _ ↦ b) (fun _ ↦ Part.some b') fun _ _ _ ↦ ⟨b', rfl, hb⟩
   | intensionalRight =>
-    simpa [evalPartial, eval] using hb (fun _ ↦ a) (fun _ ↦ Part.some a') fun _ ↦ ⟨a', rfl, ha⟩
+    simpa [evalPartial, eval] using
+      hb (fun _ ↦ a) (fun _ ↦ Part.some a') fun _ _ _ ↦ ⟨a', rfl, ha⟩
   | predicateModification =>
     refine ⟨_, by simp [evalPartial]; rfl, Ty.lifts_fn.mpr fun x y hxy ↦ ?_⟩
     obtain ⟨p, hp, hlp⟩ := ha x y hxy