Model-theoretic semantics for type-driven composition

A composition model is a mathlib first-order Structure over an entity domain, indexed by a world set (constant-domain intensional first-order). Content-predicate denotations are sourced from the model via Structure.RelMap, exactly as DRT sources atomic-condition truth (Semantics/Dynamic/DRS/); higher-order denotations (GQs, type-shifts) and worlds ride on top in Lean and in the .intens types, so the existing Tree.interp engine composes a model-sourced lexicon unchanged.

API objects (Pronoun, …) and Fragments/ stay minimal data: the engine projects them into typed terms — a pronoun occurrence to a trace valued by the assignment over the model's entity domain, φ-features to restrictions read off the model — and the model interprets those terms. Nothing model-theoretic lives on the objects or in the lexicon data.

Main declarations

• Model — entity domain E, worlds W, and a world-indexed family interp : W → L.Structure E
• Model.pred₁ / Model.pred₂ — model-sourced intensional predicate denotations; Model.const, Model.pred₁ext / Model.pred₂ext — their extensions at a world
• LexNaming, Model.lexiconAt — build a Lexicon from naming maps into the signature
• interp_model_sourced, interp_lexiconAt_predication — the real Tree.interp composes a model-sourced lexicon, truth bottoming out in RelMap
• barbara — cross-model logical consequence (truth in all models), the payoff over a fixed entity/world frame
• interp_pronoun_trace, genderRestriction — the projection discipline for API objects

Implementation notes

interp : W → L.Structure E carries structures as terms, not instances — a world-indexed family of structures on one carrier cannot be instance-based (same rationale as equational_theories' term-level Magma.FOStructure). The cost is explicit instance threading (letI := m.interp w) when interfacing with instance-based mathlib API such as Formula.Realize. Concrete fragments should follow mathlib's concrete-language idiom (Mathlib/ModelTheory/Algebra/Ring/Basic.lean): arity-indexed symbol inductives, per-symbol defeq abbrevs, and one @[simp] funMap/RelMap lemma per symbol — see Fragments/English/Toy.lean.

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

A composition model: a constant entity domain E, a world set W, and a world-indexed family of first-order L-structures (the lexicon interpretation), with the content lexicon as a mathlib Language signature (constant-domain intensional first-order).

• E : Type

  Entity domain.

• W : Type

  World/index set.

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

  World-indexed interpretation of the lexical signature.

def Semantics.Composition.Model.pred₁ {L : FirstOrder.Language} (m : Model L) (R : L.Relations 1) : Intensional.Denot m.E m.W (Intensional.Ty.e ⇒ Intensional.Ty.t.intens)

A unary content predicate's denotation, sourced from the model: world-relativized, bottoming out in Structure.RelMap. Type e ⇒ ⟨s,t⟩ — an intensional one-place predicate.

Equations

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

def Semantics.Composition.Model.pred₂ {L : FirstOrder.Language} (m : Model L) (R : L.Relations 2) : Intensional.Denot m.E m.W (Intensional.Ty.e ⇒ Intensional.Ty.e ⇒ Intensional.Ty.t.intens)

A binary content predicate's denotation, sourced from the model (e ⇒ e ⇒ ⟨s,t⟩, object-first then subject, matching the eet convention).

Equations

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

def Semantics.Composition.Model.const {L : FirstOrder.Language} (m : Model L) (c : L.Constants) (w : m.W) : Intensional.Denot m.E m.W Intensional.Ty.e

A constant's (proper name's) interpretation at world w (the world-indexed Structure.constantMap).

Equations

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

def Semantics.Composition.Model.pred₁ext {L : FirstOrder.Language} (m : Model L) (R : L.Relations 1) (w : m.W) : Intensional.Denot m.E m.W (Intensional.Ty.e ⇒ Intensional.Ty.t)

A unary predicate's extensional denotation at world w (e ⇒ t): the extension of Model.pred₁.

Equations

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

def Semantics.Composition.Model.pred₂ext {L : FirstOrder.Language} (m : Model L) (R : L.Relations 2) (w : m.W) : Intensional.Denot m.E m.W (Intensional.Ty.e ⇒ Intensional.Ty.e ⇒ Intensional.Ty.t)

A binary predicate's extensional denotation at world w (e ⇒ e ⇒ t, object-first): the extension of Model.pred₂.

Equations

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

@[simp]

theorem Semantics.Composition.Model.pred₁_apply {L : FirstOrder.Language} (m : Model L) (R : L.Relations 1) (x : m.E) (w : m.W) : m.pred₁ R x w = m.pred₁ext R w x

@[simp]

theorem Semantics.Composition.Model.pred₂_apply {L : FirstOrder.Language} (m : Model L) (R : L.Relations 2) (y x : m.E) (w : m.W) : m.pred₂ R y x w = m.pred₂ext R w y x

Lexicon from signature

A fragment supplies naming maps from word forms into the signature; the model induces the lexicon. Denotations never live in the fragment data — they are read off funMap/RelMap.

structure Semantics.Composition.LexNaming (L : FirstOrder.Language) : Type (max u v)

Naming maps from word forms into a signature: proper names to constants, content words to relation symbols.

• names : String → Option L.Constants

  Proper names denote constants.

• preds₁ : String → Option (L.Relations 1)

  Common nouns / intransitive verbs denote unary relation symbols.

• preds₂ : String → Option (L.Relations 2)

  Transitive verbs denote binary relation symbols.

def Semantics.Composition.Model.lexiconAt {L : FirstOrder.Language} (m : Model L) (nm : LexNaming L) (w : m.W) : Montague.Lexicon m.E m.W

The extensional lexicon a naming map induces at world w: names denote constants' interpretations (e), unary symbols extensional predicates (e ⇒ t), binary symbols object-first relations (e ⇒ e ⇒ t) — all sourced from the model.

Equations

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

Engine integration: the real Tree.interp composes a model-sourced lexicon

def Semantics.Composition.lexFromModel {L : FirstOrder.Language} (m : Model L) (subj : m.E) (R : L.Relations 1) : Montague.Lexicon m.E m.W

A minimal model-sourced lexicon: "subj" denotes subj, and the intransitive verb "V" has the model's interpretation of a unary symbol R as its (intensional) denotation.

Equations

• Semantics.Composition.lexFromModel m subj R "subj" = some { ty := Intensional.Ty.e, denot := subj }
• Semantics.Composition.lexFromModel m subj R "V" = some { ty := Intensional.Ty.e ⇒ Intensional.Ty.t.intens, denot := m.pred₁ R }
• Semantics.Composition.lexFromModel m subj R s = none

def Semantics.Composition.predicationTree : Syntax.Tree Unit String

"subj V" — a one-place predication.

Equations

• Semantics.Composition.predicationTree = Syntax.Tree.node () [Syntax.Tree.terminal () "subj", Syntax.Tree.terminal () "V"]

theorem Semantics.Composition.interp_model_sourced {L : FirstOrder.Language} (m : Model L) (subj : m.E) (R : L.Relations 1) (g : Core.Assignment m.E) : Tree.interp m.E m.W (lexFromModel m subj R) g predicationTree = some { ty := Intensional.Ty.t.intens, val := fun (w : m.W) => FirstOrder.Language.Structure.RelMap R fun (x : Fin 1) => subj }

Engine integration: the actual Tree.interp composes the model-sourced lexicon (via real backward FA) to a proposition ⟨s,t⟩, threading worlds through the .intens type; its truth at a world bottoms out in Structure.RelMap. The engine needs no model-specific machinery.

theorem Semantics.Composition.interp_lexiconAt_predication {L : FirstOrder.Language} (m : Model L) (nm : LexNaming L) (w : m.W) (g : Core.Assignment m.E) {s v : String} {c : L.Constants} {R : L.Relations 1} (hs : nm.names s = some c) (hv : nm.names v = none) (hv₁ : nm.preds₁ v = some R) : Tree.interp m.E m.W (m.lexiconAt nm w) g (Syntax.Tree.node () [Syntax.Tree.terminal () s, Syntax.Tree.terminal () v]) = some { ty := Intensional.Ty.t, val := FirstOrder.Language.Structure.RelMap R fun (x : Fin 1) => m.const c w }

Engine integration for lexiconAt: a name–verb predication composes (via real backward FA) to a truth value read off RelMap at the lexicon's world. The fragment supplies only the naming maps.

Cross-model logical consequence

theorem Semantics.Composition.barbara {L : FirstOrder.Language} (m : Model L) (w : m.W) (P Q R : L.Relations 1) (hQR : ∀ (x : m.E), (FirstOrder.Language.Structure.RelMap Q fun (x_1 : Fin 1) => x) → FirstOrder.Language.Structure.RelMap R fun (x_1 : Fin 1) => x) (hPQ : ∀ (x : m.E), (FirstOrder.Language.Structure.RelMap P fun (x_1 : Fin 1) => x) → FirstOrder.Language.Structure.RelMap Q fun (x_1 : Fin 1) => x) (x : m.E) : (FirstOrder.Language.Structure.RelMap P fun (x_1 : Fin 1) => x) → FirstOrder.Language.Structure.RelMap R fun (x_1 : Fin 1) => x

Cross-model consequence (the payoff over a fixed frame): with content predicates sourced from the model and the quantifier in Lean, the syllogism every Q is R, every P is Q ⊨ every P is R holds in every model m and world w — genuine logical consequence, ∀ models.

Projection discipline for API objects

API objects carry minimal data; the engine projects them into model-theoretic terms. A pronoun occurrence projects to a trace, interpreted as the assignment value over the model's entity domain; its φ-features project to restrictions read off the model. Nothing model-theoretic is stored on the Pronoun object (which has "no denotation of its own").

theorem Semantics.Composition.interp_pronoun_trace {L : FirstOrder.Language} (m : Model L) (lex : Montague.Lexicon m.E m.W) (g : Core.Assignment m.E) (n : ℕ) : Tree.interp m.E m.W lex g (Syntax.Tree.trace n ()) = some { ty := Intensional.Ty.e, val := g n }

A pronoun occurrence projects to a trace term: the engine interprets heₙ as the assignment value g n, an entity in the model's domain. The object supplies only the index.

def Semantics.Composition.genderRestriction {L : FirstOrder.Language} (m : Model L) (masc : L.Relations 1) (w : m.W) (g : Core.Assignment m.E) (n : ℕ) : Prop

A φ-feature (here masculine gender) projects to a restriction on the referent, read off the model: masc(g n) at world w. The pronoun carries the feature; the model interprets it.

Equations

• Semantics.Composition.genderRestriction m masc w g n = FirstOrder.Language.Structure.RelMap masc fun (x : Fin 1) => g n