@[reducible, inline]

abbrev Semantics.Montague.Variables.Assignment (m : Model) : Type

Assignment function: maps variable indices to entities.

Unified with Core.Assignment — this is Nat → m.Entity. All variable-binding frameworks in the library (Montague, DRT, DPL, CDRT, cylindric algebra) share this canonical type, differing only in the entity parameter.

Equations

• Semantics.Montague.Variables.Assignment m = Core.Assignment m.Entity

def Semantics.Montague.Variables.Assignment.update {m : Model} (g : Assignment m) (n : ℕ) (x : m.Entity) : Assignment m

Modified assignment g[n↦x]. Delegates to Core.Assignment.update.

Equations

• g.update n x = Core.Assignment.update g n x

def Semantics.Montague.Variables.«term_[_↦_]» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Semantics.Montague.Variables.update_same {m : Model} (g : Assignment m) (n : ℕ) (x : m.Entity) : g.update n x n = x

@[simp]

theorem Semantics.Montague.Variables.update_other {m : Model} (g : Assignment m) (n i : ℕ) (x : m.Entity) (h : i ≠ n) : g.update n x i = g i

theorem Semantics.Montague.Variables.update_update_same {m : Model} (g : Assignment m) (n : ℕ) (x y : m.Entity) : (g.update n x).update n y = g.update n y

theorem Semantics.Montague.Variables.update_update_comm {m : Model} (g : Assignment m) (n₁ n₂ : ℕ) (x₁ x₂ : m.Entity) (h : n₁ ≠ n₂) : (g.update n₁ x₁).update n₂ x₂ = (g.update n₂ x₂).update n₁ x₁

theorem Semantics.Montague.Variables.update_self {m : Model} (g : Assignment m) (n : ℕ) : g.update n (g n) = g

def Semantics.Montague.Variables.DenotG (m : Model) (ty : Ty) : Type

Denotation depending on assignment function.

Equations

• Semantics.Montague.Variables.DenotG m ty = (Semantics.Montague.Variables.Assignment m → m.interpTy ty)

def Semantics.Montague.Variables.interpPronoun {m : Model} (n : ℕ) : DenotG m Ty.e

Pronoun/variable denotation: ⟦xₙ⟧^g = g(n).

Equations

• Semantics.Montague.Variables.interpPronoun n g = g n

def Semantics.Montague.Variables.constDenot {m : Model} {ty : Ty} (d : m.interpTy ty) : DenotG m ty

Lift constant denotation to assignment-relative form.

Equations

• Semantics.Montague.Variables.constDenot d x✝ = d

theorem Semantics.Montague.Variables.constDenot_independent {m : Model} {ty : Ty} (d : m.interpTy ty) (g₁ g₂ : Assignment m) : constDenot d g₁ = constDenot d g₂

def Semantics.Montague.Variables.applyG {m : Model} {σ τ : Ty} (f : DenotG m (σ ⇒ τ)) (x : DenotG m σ) : DenotG m τ

Function application with assignments.

Equations

• Semantics.Montague.Variables.applyG f x g = f g (x g)

def Semantics.Montague.Variables.lambdaAbsG {m : Model} {τ : Ty} (n : ℕ) (body : DenotG m τ) : DenotG m (Ty.e ⇒ τ)

Lambda abstraction with variable binding.

Equations

• Semantics.Montague.Variables.lambdaAbsG n body g x = body (g.update n x)

theorem Semantics.Montague.Variables.lambdaAbsG_apply {m : Model} {τ : Ty} (n : ℕ) (body : DenotG m τ) (arg : m.Entity) (g : Assignment m) : lambdaAbsG n body g arg = body (g.update n arg)

theorem Semantics.Montague.Variables.lambdaAbsG_alpha {m : Model} {τ : Ty} (n₁ n₂ : ℕ) (body : DenotG m τ) (g : Assignment m) (h_fresh : ∀ (g' : Assignment m) (x : m.Entity), body (g'.update n₁ x) = body (g'.update n₂ x)) : lambdaAbsG n₁ body g = lambdaAbsG n₂ body g

def Semantics.Montague.Variables.g₀ : Assignment toyModel

Equations

• Semantics.Montague.Variables.g₀ x✝ = Semantics.Montague.ToyEntity.john

def Semantics.Montague.Variables.sleeps_lambda : DenotG toyModel (Ty.e ⇒ Ty.t)

Equations

• One or more equations did not get rendered due to their size.

theorem Semantics.Montague.Variables.sleeps_lambda_eq : sleeps_lambda g₀ = ToyLexicon.sleeps_sem

Assignment-sensitive composition as an applicative functor

@cite{charlow-2018} observes that constDenot (ρ) and applyG (⊛) form an applicative functor for the Reader type constructor G a := g → a (@cite{mcbride-paterson-2008}). These are not new operations — they are factored out of the standard @cite{heim-kratzer-1998} account. The four applicative functor laws hold definitionally.

Adding the join operation denotGJoin (μ) — which flattens doubly assignment-dependent meanings by feeding the same assignment twice — upgrades the structure to a monad (the Reader/Environment monad), enabling analyses of paycheck pronouns and binding reconstruction.

theorem Semantics.Montague.Variables.constDenot_applyG {m : Model} {σ τ : Ty} (f : m.interpTy (σ ⇒ τ)) (x : m.interpTy σ) : applyG (constDenot f) (constDenot x) = constDenot (f x)

Homomorphism: ρ f ⊛ ρ x = ρ (f x).

theorem Semantics.Montague.Variables.applyG_constDenot_id {m : Model} {σ : Ty} (v : DenotG m σ) : applyG (constDenot id) v = v

Identity: ρ id ⊛ v = v.

theorem Semantics.Montague.Variables.applyG_constDenot_interchange {m : Model} {σ τ : Ty} (u : DenotG m (σ ⇒ τ)) (y : m.interpTy σ) : applyG u (constDenot y) = applyG (constDenot fun (f : m.interpTy (σ ⇒ τ)) => f y) u

Interchange: u ⊛ ρ y = ρ (· y) ⊛ u.

theorem Semantics.Montague.Variables.applyG_composition {m : Model} {σ τ υ : Ty} (u : DenotG m (τ ⇒ υ)) (v : DenotG m (σ ⇒ τ)) (w : DenotG m σ) : applyG (applyG (applyG (constDenot fun (f : m.interpTy (τ ⇒ υ)) (g : m.interpTy (σ ⇒ τ)) (x : m.interpTy σ) => f (g x)) u) v) w = applyG u (applyG v w)

Composition: ρ comp ⊛ u ⊛ v ⊛ w = u ⊛ (v ⊛ w).

def Semantics.Montague.Variables.denotGJoin {m : Model} {A : Type} (ho : Assignment m → Assignment m → A) : Assignment m → A

Join (μ): flatten a doubly assignment-dependent meaning.

@cite{charlow-2018} §4.2: μ m := λg. m g g.

Enables higher-order variables: a pronoun anaphoric to an intension (type g → g → a) is flattened to a standard denotation (type g → a) by evaluating the retrieved intension at the current assignment.

Equations

• Semantics.Montague.Variables.denotGJoin ho g = ho g g

theorem Semantics.Montague.Variables.denotGJoin_const {m : Model} {A : Type} (d : Assignment m → A) : (denotGJoin fun (x : Assignment m) => d) = d

Left identity: μ (ρ d) = d.

theorem Semantics.Montague.Variables.denotGJoin_inner_const {m : Model} {A : Type} (d : Assignment m → A) : (denotGJoin fun (g x : Assignment m) => d g) = d

Right identity: μ (λg. ρ(d g)) = d.

theorem Semantics.Montague.Variables.denotGJoin_assoc {m : Model} {A : Type} (hho : Assignment m → Assignment m → Assignment m → A) : denotGJoin (denotGJoin hho) = denotGJoin fun (g : Assignment m) => denotGJoin (hho g)

Associativity: μ ∘ μ = μ ∘ fmap μ.

Assignments as a cylindric set algebra

Heim & Kratzer's assignment functions satisfy the same algebraic axioms as DRT's dynamic assignments: predicates on assignments form a cylindric set algebra (@cite{henkin-monk-tarski-1971}). The operations:

• Existential closure ∃n.φ(g) = ∃x.φ(g[n↦x]) = cylindrification
• Identity g(n) = g(m) = diagonal element
• Lambda abstraction λn.φ = fun x => φ(g[n↦x]) = the integrand of cylindrification
• Pronoun resolution (binding n to m) = cylindric substitution

This section develops these correspondences purely within the Montague Assignment type, without importing the dynamic semantics stack.

def Semantics.Montague.Variables.existsClosure {m : Model} (n : ℕ) (φ : Assignment m → Prop) : Assignment m → Prop

Existential closure at variable n: (∃n.φ)(g) = ∃x. φ(g[n↦x]).

This is cylindrification on Montague assignments (@cite{henkin-monk-tarski-1971}, @cite{heim-kratzer-1998} Ch. 5).

Equations

• Semantics.Montague.Variables.existsClosure n φ g = ∃ (x : m.Entity), φ (g.update n x)

def Semantics.Montague.Variables.diag {m : Model} (n k : ℕ) : Assignment m → Prop

Diagonal element: assignments where variables n and k agree. Dnk = {g : g(n) = g(k)}.

Equations

• Semantics.Montague.Variables.diag n k g = (g n = g k)

theorem Semantics.Montague.Variables.existsClosure_bot {m : Model} (n : ℕ) : (existsClosure n fun (x : Assignment m) => False) = fun (x : Assignment m) => False

C₁: Existential closure of False is False.

theorem Semantics.Montague.Variables.le_existsClosure {m : Model} (n : ℕ) (φ : Assignment m → Prop) (g : Assignment m) : φ g → existsClosure n φ g

C₂: φ implies its existential closure.

theorem Semantics.Montague.Variables.diag_refl {m : Model} (n : ℕ) : diag n n = fun (x : Assignment m) => True

C₅: Dnn = ⊤ (reflexivity of equality).

def Semantics.Montague.Variables.resolve {m : Model} (κ l : ℕ) (φ : Assignment m → Prop) : Assignment m → Prop

Pronoun resolution: setting variable κ to read from variable l.

When pronoun κ is bound by a binder at index l, the semantic effect is φ(g[κ↦g(l)]). This is the cylindric algebra's direct substitution σ^κ_l.

Equations

• Semantics.Montague.Variables.resolve κ l φ g = φ (g.update κ (g l))

theorem Semantics.Montague.Variables.resolve_eq_existsClosure_diag {m : Model} (κ l : ℕ) (φ : Assignment m → Prop) (h : κ ≠ l) (g : Assignment m) : resolve κ l φ g ↔ existsClosure κ (fun (g' : Assignment m) => diag κ l g' ∧ φ g') g

Substitution = resolution.

Algebraic substitution cκ(Dκl · φ) — cylindrification after constraining κ to equal l via the diagonal — computes the same predicate as direct pronoun resolution φ(g[κ↦g(l)]).

theorem Semantics.Montague.Variables.existsClosure_eq_exists_lambda {m : Model} (n : ℕ) (body : DenotG m Ty.t) (g : Assignment m) : existsClosure n (fun (g' : Assignment m) => body g' = true) g ↔ ∃ (x : m.Entity), lambdaAbsG n body g x = true

Lambda abstraction at n is the "integrand" of existential closure: ∃n.φ = ∃x. (λn.φ)(g)(x).

Montague ≡ Core.CylindricAlgebra

The operations in this section — existsClosure, diag, resolve — are the same functions as cylindrify, diagonal, directSubst from Core.CylindricAlgebra. Both are defined via Core.Assignment.update. The identities are definitional (rfl).

Together with the DPL ↔ Cylindric Algebra bridge in DPL/Bridge.lean (which proves closure(∃x.φ) = cylindrify x (closure φ)), this establishes a three-way connection:

  Montague (static)         DPL (dynamic)
  existsClosure n φ         DPLRel.exists_ x φ
        │                         │
        │ rfl                     │ closure
        ▼                         ▼
  Core.CylindricAlgebra.cylindrify n

H&K's static binding and DPL's dynamic binding are both instances of cylindrification — they differ only in whether the output assignment is visible (DPL: relation g → h → Prop) or projected away (Montague: predicate g → Prop).

theorem Semantics.Montague.Variables.existsClosure_eq_cylindrify {m : Model} (n : ℕ) (φ : Assignment m → Prop) : existsClosure n φ = Core.CylindricAlgebra.cylindrify n φ

existsClosure IS cylindrify: H&K's existential closure is literally cylindrification on the assignment algebra.

theorem Semantics.Montague.Variables.diag_eq_diagonal {m : Model} (n k : ℕ) : diag n k = Core.CylindricAlgebra.diagonal n k

diag IS diagonal: H&K's variable identity test is literally the cylindric algebra's diagonal element.

theorem Semantics.Montague.Variables.resolve_eq_directSubst {m : Model} (κ l : ℕ) (φ : Assignment m → Prop) : resolve κ l φ = Core.CylindricAlgebra.directSubst κ l φ

resolve IS directSubst: H&K's pronoun resolution is literally cylindric substitution.