Model-theoretic semantics for type-driven composition

A composition model is a mathlib first-order structure on one entity domain at each world of a world set. The symbols of the signature denote what the structure gives them, read off through Structure.funMap and Structure.RelMap as DRT reads off the truth of atomic conditions (Semantics/Dynamic/DRS/), and world dependence stays in the .intens types. The words of a first-order fragment translate to these symbols (Composition/Reduction.lean).

Main definitions

• Model: an entity domain E, worlds W, and a structure interp w at each world.
• Model.const, Model.pred₁, Model.pred₂: the denotations of a constant and of unary and binary relation symbols at a world.

Implementation notes

interp : W → L.Structure E carries structures as terms rather than instances, since a world-indexed family of structures on one carrier cannot be instance-based; formulas are realized at a world by Formula.RealizeAt m.interp w. The concrete model in Semantics/Composition/Toy.lean follows mathlib's concrete-language idiom.

References

• [HK98]

structure HeimKratzer.Model (L : FirstOrder.Language) : Type (max (max 1 u) v)

A composition model has a constant entity domain E, a world set W, and at each world a first-order L-structure interpreting the content signature.

• E : Type

  The entity domain is shared by all worlds.

• W : Type

  The worlds index the interpretations.

• interp : self.W → L.Structure self.E

  At each world a structure interprets the signature.

def HeimKratzer.Model.const {L : FirstOrder.Language} (m : Model L) (c : L.Constants) (w : m.W) : Montague.Ty.Domain m.E m.W Montague.Ty.e

The interpretation of a constant at world w is the entity the structure there assigns it.

Equations

• m.const c w = FirstOrder.Language.Structure.funMap c default

def HeimKratzer.Model.pred₁ {L : FirstOrder.Language} (m : Model L) (R : L.Relations 1) (w : m.W) : Montague.Ty.Domain m.E m.W (Montague.Ty.e ⇒ Montague.Ty.t)

The denotation e ⇒ t of a unary symbol at world w holds of the entities the structure there relates by it.

Equations

• m.pred₁ R w x = FirstOrder.Language.Structure.RelMap R fun (x_1 : Fin 1) => x

def HeimKratzer.Model.pred₂ {L : FirstOrder.Language} (m : Model L) (R : L.Relations 2) (w : m.W) : Montague.Ty.Domain m.E m.W (Montague.Ty.e ⇒ Montague.Ty.e ⇒ Montague.Ty.t)

The denotation e ⇒ e ⇒ t of a binary symbol at world w takes the object first and the subject second, as transitive verbs do.

Equations

• m.pred₂ R w y x = FirstOrder.Language.Structure.RelMap R fun (i : Fin 2) => if i = 0 then x else y