From 68f96e45e3823164c45b519a0f060137c9d4f97a Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Tue, 27 Oct 2026 13:55:31 -0700 Subject: [PATCH 1/2] docs(Semantics/Composition): coordinator results as linked prose --- Linglib/Semantics/Composition/Coordinator.lean | 10 +++------- 1 file changed, 3 insertions(+), 7 deletions(-) diff --git a/Linglib/Semantics/Composition/Coordinator.lean b/Linglib/Semantics/Composition/Coordinator.lean index 582c723c78..34f53c712b 100644 --- a/Linglib/Semantics/Composition/Coordinator.lean +++ b/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 From ea51636158b7c4d76880676bba4a0502273363da Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Tue, 27 Oct 2026 14:04:37 -0700 Subject: [PATCH 2/2] refactor(Semantics/Composition): a type of worlds, intensions from it --- Linglib/Logic/Modal/Basic.lean | 22 ++++----- Linglib/Logic/Modal/Defs.lean | 26 +++-------- Linglib/Logic/Modal/Epistemic.lean | 22 +++------ .../Modal/FirstOrder/Correspondence.lean | 12 ++--- Linglib/Logic/Modal/FirstOrder/Semantics.lean | 11 ++--- Linglib/Semantics/Composition/FirstOrder.lean | 45 ++++++++++++++----- Linglib/Semantics/Composition/Partial.lean | 15 ++++--- Linglib/Semantics/Composition/Ty.lean | 44 +++++++++--------- Studies/Gajewski2002.lean | 6 +-- 9 files changed, 101 insertions(+), 102 deletions(-) diff --git a/Linglib/Logic/Modal/Basic.lean b/Linglib/Logic/Modal/Basic.lean index 004250f4e7..e3584779d9 100644 --- a/Linglib/Logic/Modal/Basic.lean +++ b/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 diff --git a/Linglib/Logic/Modal/Defs.lean b/Linglib/Logic/Modal/Defs.lean index fcb28133a2..d41ed20cef 100644 --- a/Linglib/Logic/Modal/Defs.lean +++ b/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 diff --git a/Linglib/Logic/Modal/Epistemic.lean b/Linglib/Logic/Modal/Epistemic.lean index c62e18a5ec..fce16e5f95 100644 --- a/Linglib/Logic/Modal/Epistemic.lean +++ b/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 diff --git a/Linglib/Logic/Modal/FirstOrder/Correspondence.lean b/Linglib/Logic/Modal/FirstOrder/Correspondence.lean index 8a615f71aa..1e6ae08d81 100644 --- a/Linglib/Logic/Modal/FirstOrder/Correspondence.lean +++ b/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 diff --git a/Linglib/Logic/Modal/FirstOrder/Semantics.lean b/Linglib/Logic/Modal/FirstOrder/Semantics.lean index 3d3027ff02..f39a89ad44 100644 --- a/Linglib/Logic/Modal/FirstOrder/Semantics.lean +++ b/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 diff --git a/Linglib/Semantics/Composition/FirstOrder.lean b/Linglib/Semantics/Composition/FirstOrder.lean index cc8611aab1..4ac3f6ad87 100644 --- a/Linglib/Semantics/Composition/FirstOrder.lean +++ b/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, diff --git a/Linglib/Semantics/Composition/Partial.lean b/Linglib/Semantics/Composition/Partial.lean index 675bff6d87..978abd1a5c 100644 --- a/Linglib/Semantics/Composition/Partial.lean +++ b/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 diff --git a/Linglib/Semantics/Composition/Ty.lean b/Linglib/Semantics/Composition/Ty.lean index 1b9040dd11..d53d065a3c 100644 --- a/Linglib/Semantics/Composition/Ty.lean +++ b/Linglib/Semantics/Composition/Ty.lean @@ -7,16 +7,18 @@ public import Mathlib.Order.CompleteBooleanAlgebra # Semantic types and denotation domains In Montague semantics every expression has a *semantic type*, which fixes the kind of thing it -denotes: an individual ($e$), a truth value ($t$), a function from denotations of type $a$ to -denotations of type $b$ ($\langle a,b\rangle$), or an *intension* ($\langle s,a\rangle$), a -function from worlds to denotations of type $a$. Later work adds sorts for degrees, cardinalities, -and events and states. Each type has a *domain* of possible denotations, built from a set of -individuals and a set of worlds, and the domain of a type that ends in $t$ is a Boolean algebra, -pointwise. +denotes: an individual ($e$), a truth value ($t$), a world ($s$), or a function from denotations +of type $a$ to denotations of type $b$ ($\langle a,b\rangle$). An *intension*, of type +$\langle s,a\rangle$, is a function from worlds; Montague's intensional logic has no type $s$ of +its own, and the two-sorted type theory of Gallin adds it. Later work adds sorts for degrees, +cardinalities, and events and states. Each type has a *domain* of possible denotations, built from +a set of individuals and a set of worlds, and the domain of a type that ends in $t$ is a Boolean +algebra, pointwise. ## Main definitions * `Montague.Ty`: semantic types. +* `Montague.Ty.intens`: intensions, the functions from worlds. * `Montague.Sorts`: the carriers of the degree and eventuality sorts. * `Montague.Ty.Domain E W ty S`: the denotation domain of `ty`. * `Montague.Denotation E W M S`: a semantic type with an `M`-computation in its domain. @@ -44,13 +46,14 @@ composition engine's dispatch on types at run time. namespace Montague -/-- The semantic types are Montague's `e`, `t`, `fn a b` (⟨a,b⟩) and `intens a` (⟨s,a⟩), the -degree sort `d` ([heim-2001], [wellwood-2015]), the cardinality sort `n` ([sudo-2016], -[scontras-2014], [little-moroney-royer-2022]), and the eventuality sort `v` ([davidson-1967], -[parsons-1990]). Kratzer's type `s` of events, of which actions and states are subkinds -([kratzer-1996]), is `v`, as are Hanink and Koontz-Garboden's states -([hanink-koontz-garboden-2025]); events and states are distinguished within it -([yu-ausensi-smith-2023]), not as two types. -/ +/-- The semantic types are the entities `e`, the truth values `t`, the worlds `s`, and the +functions `fn a b` (⟨a,b⟩) of two-sorted type theory ([gallin-1975]), in which Montague's +intensions ⟨s,a⟩ are the functions from worlds (`Ty.intens`), together with the degree sort `d` +([heim-2001], [wellwood-2015]), the cardinality sort `n` ([sudo-2016], [scontras-2014], +[little-moroney-royer-2022]), and the eventuality sort `v` ([davidson-1967], [parsons-1990]). +Kratzer's type `s` of events, of which actions and states are subkinds ([kratzer-1996]), is `v`, +not the worlds `s`, as are Hanink and Koontz-Garboden's states ([hanink-koontz-garboden-2025]); +events and states are distinguished within it ([yu-ausensi-smith-2023]), not as two types. -/ inductive Ty where /-- Entities. -/ | e @@ -62,14 +65,17 @@ inductive Ty where | n /-- Eventualities, events and states alike. -/ | v + /-- Worlds, or situations: the indices of evaluation. -/ + | s /-- Functions `⟨a,b⟩`. -/ | fn : Ty → Ty → Ty - /-- Intensions `⟨s,a⟩`. -/ - | intens : Ty → Ty deriving Repr, DecidableEq @[inherit_doc] scoped infixr:25 " ⇒ " => Ty.fn +/-- Intensions `⟨s,a⟩`, the functions from worlds. -/ +@[match_pattern] abbrev Ty.intens (a : Ty) : Ty := .fn .s a + /-- `⟨e,t⟩`, properties of individuals. -/ abbrev Ty.et : Ty := .e ⇒ .t /-- `⟨e,⟨e,t⟩⟩`, relations between individuals. -/ @@ -92,7 +98,8 @@ structure Sorts where eventuality : Type := Empty /-- The type `e` denotes in `E`, `t` in `Prop`, `d` in the scale of degrees, `n` in `ℕ`, `v` in -the eventualities, `⟨a,b⟩` in `Ty.Domain a → Ty.Domain b` and `⟨s,a⟩` in `W → Ty.Domain a`. -/ +the eventualities, `s` in `W`, and `⟨a,b⟩` in `Ty.Domain a → Ty.Domain b`, so that an intension +`⟨s,a⟩` denotes in `W → Ty.Domain a`. -/ abbrev Ty.Domain (E W : Type) (ty : Ty) (S : Sorts := {}) : Type := match ty with | .e => E @@ -100,8 +107,8 @@ abbrev Ty.Domain (E W : Type) (ty : Ty) (S : Sorts := {}) : Type := | .d => S.degree | .n => ℕ | .v => S.eventuality + | .s => W | .fn a b => Ty.Domain E W a S → Ty.Domain E W b S - | .intens a => W → Ty.Domain E W a S /-- A denotation in the Montague type system is a semantic type together with an `M`-computation in the domain of that type. `M := Id` is the pure [heim-kratzer-1998] carrier; effectful @@ -120,9 +127,6 @@ def Ty.Domain.completeBooleanAlgebra? (E W : Type) (ty : Ty) (S : Sorts := {}) : | .fn _ b => (completeBooleanAlgebra? E W b S).map fun (i : CompleteBooleanAlgebra (Ty.Domain E W b S)) => letI := i; inferInstance - | .intens a => - (completeBooleanAlgebra? E W a S).map fun (i : CompleteBooleanAlgebra (Ty.Domain E W a S)) => - letI := i; inferInstance | _ => none end Montague diff --git a/Studies/Gajewski2002.lean b/Studies/Gajewski2002.lean index 2af236f24c..4ff6056ba3 100644 --- a/Studies/Gajewski2002.lean +++ b/Studies/Gajewski2002.lean @@ -53,8 +53,8 @@ concedes and `exceptiveSkeleton_most_not_isLAnalytic` states. ## Implementation notes * The paper's type hierarchy has `e`, `t` and function types only; `permLift` extends it to - the rest of `Montague.Ty` by the identity at the degree, cardinality and eventuality sorts - and pointwise at intensions, with `Unit` as the inert index sort of the extensional + the rest of `Montague.Ty` by the identity at the degree, cardinality, eventuality and world + sorts, so pointwise at intensions, with `Unit` as the inert index sort of the extensional fragment. * The denotation of *but* is the paper's schema factored compositionally, but where the printed uniqueness clause reads `g ⊆ j` the least-exception schema it factors requires @@ -111,8 +111,8 @@ def permLift (π : Equiv.Perm E) : ∀ ty : Ty, Equiv.Perm (Ty.Domain E Unit ty) | .d => Equiv.refl _ | .n => Equiv.refl _ | .v => Equiv.refl _ + | .s => Equiv.refl _ | .fn a b => (permLift π a).arrowCongr (permLift π b) - | .intens a => (Equiv.refl Unit).arrowCongr (permLift π a) @[simp] theorem permLift_et_apply (π : Equiv.Perm E) (P : E → Prop) : permLift π Ty.et P = P ∘ ⇑π.symm :=