Variable Binding and Assignment Functions

@cite{heim-kratzer-1998} @cite{charlow-2018}

Framework-neutral infrastructure for interpreting expressions with free variables, built on Core.Logic.Intensional.Frame.

Main definitions

• Assignment (from Core/Assignment.lean) instantiated at F.Entity for entity pronouns and F.Index for situation pronouns
• DenotG — assignment-relative denotations
• applyG, lambdaAbsG, constDenot — composition with assignments
• Applicative functor laws (@cite{charlow-2018})
• Cylindric algebra bridge (@cite{henkin-monk-tarski-1971})

def Core.Logic.Intensional.Variables.«term_[_↦_]» : Lean.TrailingParserDescr

Equations

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

@[simp]

theorem Core.Logic.Intensional.Variables.update_same {F : Frame} (g : Assignment F.Entity) (n : ℕ) (x : F.Entity) : g.update n x n = x

@[simp]

theorem Core.Logic.Intensional.Variables.update_other {F : Frame} (g : Assignment F.Entity) (n i : ℕ) (x : F.Entity) (h : i ≠ n) : g.update n x i = g i

theorem Core.Logic.Intensional.Variables.update_update_same {F : Frame} (g : Assignment F.Entity) (n : ℕ) (x y : F.Entity) : (g.update n x).update n y = g.update n y

theorem Core.Logic.Intensional.Variables.update_update_comm {F : Frame} (g : Assignment F.Entity) (n₁ n₂ : ℕ) (x₁ x₂ : F.Entity) (h : n₁ ≠ n₂) : (g.update n₁ x₁).update n₂ x₂ = (g.update n₂ x₂).update n₁ x₁

theorem Core.Logic.Intensional.Variables.update_self {F : Frame} (g : Assignment F.Entity) (n : ℕ) : g.update n (g n) = g

def Core.Logic.Intensional.Variables.DenotG (F : Frame) (ty : Ty) : Type

Denotation depending on assignment function.

Equations

• Core.Logic.Intensional.Variables.DenotG F ty = (Core.Assignment F.Entity → F.Denot ty)

def Core.Logic.Intensional.Variables.interpPronoun {F : Frame} (n : ℕ) : DenotG F Ty.e

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

Equations

• Core.Logic.Intensional.Variables.interpPronoun n g = g n

def Core.Logic.Intensional.Variables.constDenot {F : Frame} {ty : Ty} (d : F.Denot ty) : DenotG F ty

Lift constant denotation to assignment-relative form.

Equations

• Core.Logic.Intensional.Variables.constDenot d x✝ = d

theorem Core.Logic.Intensional.Variables.constDenot_independent {F : Frame} {ty : Ty} (d : F.Denot ty) (g₁ g₂ : Assignment F.Entity) : constDenot d g₁ = constDenot d g₂

def Core.Logic.Intensional.Variables.applyG {F : Frame} {σ τ : Ty} (f : DenotG F (σ ⇒ τ)) (x : DenotG F σ) : DenotG F τ

Function application with assignments.

Equations

• Core.Logic.Intensional.Variables.applyG f x g = f g (x g)

def Core.Logic.Intensional.Variables.lambdaAbsG {F : Frame} {τ : Ty} (n : ℕ) (body : DenotG F τ) : DenotG F (Ty.e ⇒ τ)

Lambda abstraction with variable binding.

Equations

• Core.Logic.Intensional.Variables.lambdaAbsG n body g x = body (g.update n x)

theorem Core.Logic.Intensional.Variables.lambdaAbsG_apply {F : Frame} {τ : Ty} (n : ℕ) (body : DenotG F τ) (arg : F.Entity) (g : Assignment F.Entity) : lambdaAbsG n body g arg = body (g.update n arg)

theorem Core.Logic.Intensional.Variables.lambdaAbsG_alpha {F : Frame} {τ : Ty} (n₁ n₂ : ℕ) (body : DenotG F τ) (g : Assignment F.Entity) (h_fresh : ∀ (g' : Assignment F.Entity) (x : F.Entity), body (g'.update n₁ x) = body (g'.update n₂ x)) : lambdaAbsG n₁ body g = lambdaAbsG n₂ body g

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}). The four applicative functor laws hold definitionally.

theorem Core.Logic.Intensional.Variables.constDenot_applyG {F : Frame} {σ τ : Ty} (f : F.Denot (σ ⇒ τ)) (x : F.Denot σ) : applyG (constDenot f) (constDenot x) = constDenot (f x)

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

theorem Core.Logic.Intensional.Variables.applyG_constDenot_id {F : Frame} {σ : Ty} (v : DenotG F σ) : applyG (constDenot id) v = v

Identity: ρ id ⊛ v = v.

theorem Core.Logic.Intensional.Variables.applyG_constDenot_interchange {F : Frame} {σ τ : Ty} (u : DenotG F (σ ⇒ τ)) (y : F.Denot σ) : applyG u (constDenot y) = applyG (constDenot fun (f : F.Denot (σ ⇒ τ)) => f y) u

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

theorem Core.Logic.Intensional.Variables.applyG_composition {F : Frame} {σ τ υ : Ty} (u : DenotG F (τ ⇒ υ)) (v : DenotG F (σ ⇒ τ)) (w : DenotG F σ) : applyG (applyG (applyG (constDenot fun (f : F.Denot (τ ⇒ υ)) (g : F.Denot (σ ⇒ τ)) (x : F.Denot σ) => f (g x)) u) v) w = applyG u (applyG v w)

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

def Core.Logic.Intensional.Variables.denotGJoin {F : Frame} {A : Type} (ho : Assignment F.Entity → Assignment F.Entity → A) : Assignment F.Entity → 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

• Core.Logic.Intensional.Variables.denotGJoin ho g = ho g g

theorem Core.Logic.Intensional.Variables.denotGJoin_const {F : Frame} {A : Type} (d : Assignment F.Entity → A) : (denotGJoin fun (x : Assignment F.Entity) => d) = d

Left identity: μ (ρ d) = d.

theorem Core.Logic.Intensional.Variables.denotGJoin_inner_const {F : Frame} {A : Type} (d : Assignment F.Entity → A) : (denotGJoin fun (g x : Assignment F.Entity) => d g) = d

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

theorem Core.Logic.Intensional.Variables.denotGJoin_assoc {F : Frame} {A : Type} (hho : Assignment F.Entity → Assignment F.Entity → Assignment F.Entity → A) : denotGJoin (denotGJoin hho) = denotGJoin fun (g : Assignment F.Entity) => denotGJoin (hho g)

Associativity: μ ∘ μ = μ ∘ fmap μ.

Assignments as a cylindric set algebra

@cite{heim-kratzer-1998} 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}).

def Core.Logic.Intensional.Variables.existsClosure {F : Frame} (n : ℕ) (φ : Assignment F.Entity → Prop) : Assignment F.Entity → Prop

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

Equations

• Core.Logic.Intensional.Variables.existsClosure n φ g = ∃ (x : F.Entity), φ (g.update n x)

def Core.Logic.Intensional.Variables.diag {F : Frame} (n k : ℕ) : Assignment F.Entity → Prop

Diagonal element: assignments where variables n and k agree.

Equations

• Core.Logic.Intensional.Variables.diag n k g = (g n = g k)

theorem Core.Logic.Intensional.Variables.existsClosure_bot {F : Frame} (n : ℕ) : (existsClosure n fun (x : Assignment F.Entity) => False) = fun (x : Assignment F.Entity) => False

C₁: Existential closure of False is False.

theorem Core.Logic.Intensional.Variables.le_existsClosure {F : Frame} (n : ℕ) (φ : Assignment F.Entity → Prop) (g : Assignment F.Entity) : φ g → existsClosure n φ g

C₂: φ implies its existential closure.

theorem Core.Logic.Intensional.Variables.diag_refl {F : Frame} (n : ℕ) : diag n n = fun (x : Assignment F.Entity) => True

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

def Core.Logic.Intensional.Variables.resolve {F : Frame} (κ l : ℕ) (φ : Assignment F.Entity → Prop) : Assignment F.Entity → Prop

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

Equations

• Core.Logic.Intensional.Variables.resolve κ l φ g = φ (g.update κ (g l))

theorem Core.Logic.Intensional.Variables.resolve_eq_existsClosure_diag {F : Frame} (κ l : ℕ) (φ : Assignment F.Entity → Prop) (h : κ ≠ l) (g : Assignment F.Entity) : resolve κ l φ g ↔ existsClosure κ (fun (g' : Assignment F.Entity) => diag κ l g' ∧ φ g') g

Substitution = resolution.

theorem Core.Logic.Intensional.Variables.existsClosure_eq_exists_lambda {F : Frame} (n : ℕ) (body : DenotG F Ty.t) (g : Assignment F.Entity) : existsClosure n (fun (g' : Assignment F.Entity) => body g') g ↔ ∃ (x : F.Entity), lambdaAbsG n body g x

Lambda abstraction at n is the "integrand" of existential closure.

theorem Core.Logic.Intensional.Variables.existsClosure_eq_cylindrify {F : Frame} (n : ℕ) (φ : Assignment F.Entity → Prop) : existsClosure n φ = CylindricAlgebra.cylindrify n φ

theorem Core.Logic.Intensional.Variables.diag_eq_diagonal {F : Frame} (n k : ℕ) : diag n k = CylindricAlgebra.diagonal n k

theorem Core.Logic.Intensional.Variables.resolve_eq_directSubst {F : Frame} (κ l : ℕ) (φ : Assignment F.Entity → Prop) : resolve κ l φ = CylindricAlgebra.directSubst κ l φ

Situation pronouns as the type-level dual of entity pronouns

Hanink (2018, 2021), Bondarenko (2022, 2023) and the broader post-Schwarz literature on situational vs anaphoric definites argue that a situation argument can be a bound variable (a "situation pronoun"), not just a free parameter handed to an interpretation function.

Type-theoretically this is the dual of entity binding under Ty.intens: where entity pronouns are interpreted relative to Assignment F.Entity := ℕ → F.Entity, situation pronouns are interpreted relative to SitAssignment F := ℕ → F.Index. Both reuse Core.Assignment at different instantiations, so the update lemmas (update_at, update_ne, update_overwrite, update_comm, update_self) come for free.

@[reducible, inline]

abbrev Core.Logic.Intensional.Variables.SitAssignment (F : Frame) : Type

Situation assignment: maps situation-pronoun indices to frame indices. Reuses Assignment at type F.Index.

Equations

• Core.Logic.Intensional.Variables.SitAssignment F = Core.Assignment F.Index

def Core.Logic.Intensional.Variables.interpSitPronoun {F : Frame} (n : ℕ) : SitAssignment F → F.Index

Situation-pronoun denotation: ⟦sₙ⟧^{gs} = gs(n). Parallels interpPronoun.

Equations

• Core.Logic.Intensional.Variables.interpSitPronoun n gs = gs n

def Core.Logic.Intensional.Variables.DenotGS (F : Frame) (ty : Ty) : Type

Bi-assignment-relative denotation: depends on both an entity assignment and a situation assignment. Used by any module that interprets expressions containing both entity pronouns and situation pronouns (definites, attitude reports, modal scope, world-variable binding).

Equations

• Core.Logic.Intensional.Variables.DenotGS F ty = (Core.Assignment F.Entity → Core.Logic.Intensional.Variables.SitAssignment F → F.Denot ty)

def Core.Logic.Intensional.Variables.DenotGS.ofDenotG {F : Frame} {ty : Ty} (d : DenotG F ty) : DenotGS F ty

Lift a pure entity-assignment-relative denotation to bi-assignment form (ignores the situation assignment).

Equations

• Core.Logic.Intensional.Variables.DenotGS.ofDenotG d g x✝ = d g

def Core.Logic.Intensional.Variables.DenotGS.const {F : Frame} {ty : Ty} (d : F.Denot ty) : DenotGS F ty

Lift a constant denotation to bi-assignment form (ignores both assignments).

Equations

• Core.Logic.Intensional.Variables.DenotGS.const d x✝¹ x✝ = d

theorem Core.Logic.Intensional.Variables.DenotGS.ofDenotG_const {F : Frame} {ty : Ty} (d : F.Denot ty) : ofDenotG (constDenot d) = const d

Bi-assignment lift of a pure constant is the same as DenotG-lift of a constant — the two const paths agree.