The first-order fragment of type-driven composition

The first-order constants over a signature are its constant and relation symbols, the determiners every, some and no, negation, conjunction and disjunction. Every logical form over them reads back to a first-order formula whose realization is the logical form's denotation. The readback evaluates the logical form in a syntactic model built from mathlib's terms and bounded formulas, and a logical relation with the standard model proves it sound, so first-order consequence between readbacks is entailment between trees, as Semantics/Dynamic/DRS/Reduction.lean shows for DRT.

Main definitions

• FirstOrderConstant, FirstOrderConstant.interp: the first-order constants and their denotations in a composition model at a world; Model.lexicon interprets the words of a fragment through them.
• Ty.SyntacticDomain: the syntactic model, by type and number of bound variables.
• Term.readback, Term.toFormula: the readback of a logical form.
• Ty.Realizes: the logical relation between the syntactic and the standard model.
• Tree.HoldsAt: truth of a tree under a lexicon and an assignment.

Main results

• Term.realizes_readback: a logical form's readback realizes its denotation whenever the readbacks of its constants realize theirs.
• Term.realizeAt_toFormula: a first-order logical form denotes the realization of its readback.
• Tree.holdsAt_iff_realizeAt, Tree.holdsAt_of_models, Tree.models_imp_iff_entails, Tree.holdsAt_compactness: a tree holds where its readback is realized, entailment between trees is first-order consequence, and families of trees satisfy compactness.

Implementation notes

The syntactic model is indexed by the number of bound variables in scope, and gives truth values and functions at every larger number, so a determiner binds the next de Bruijn variable of BoundedFormula without computing a fresh name. Formulas are never carried to more bound variables, since BoundedFormula.castLE keeps the index an inner quantifier binds. Most is not first-order definable, as Barwise and Cooper showed, so it is not a first-order constant.

References

• [HK98]
• [BC81]
• [Mon73]

First-order constants

inductive HeimKratzer.FirstOrderConstant (L : FirstOrder.Language) : Montague.Ty → Type (max u v)

The first-order constants over a signature L are its constant symbols at type e, its unary and binary relation symbols at e ⇒ t and e ⇒ e ⇒ t, the determiners every, some and no, negation, and conjunction and disjunction.

• name {L : FirstOrder.Language} (c : L.Constants) : FirstOrderConstant L Montague.Ty.e
• rel₁ {L : FirstOrder.Language} (R : L.Relations 1) : FirstOrderConstant L (Montague.Ty.e ⇒ Montague.Ty.t)
• rel₂ {L : FirstOrder.Language} (R : L.Relations 2) : FirstOrderConstant L (Montague.Ty.e ⇒ Montague.Ty.e ⇒ Montague.Ty.t)
• every {L : FirstOrder.Language} : FirstOrderConstant L Montague.Ty.det
• some {L : FirstOrder.Language} : FirstOrderConstant L Montague.Ty.det
• no {L : FirstOrder.Language} : FirstOrderConstant L Montague.Ty.det
• neg {L : FirstOrder.Language} : FirstOrderConstant L (Montague.Ty.t ⇒ Montague.Ty.t)
• conj {L : FirstOrder.Language} : FirstOrderConstant L (Montague.Ty.t ⇒ Montague.Ty.t ⇒ Montague.Ty.t)
• disj {L : FirstOrder.Language} : FirstOrderConstant L (Montague.Ty.t ⇒ Montague.Ty.t ⇒ Montague.Ty.t)

def HeimKratzer.FirstOrderConstant.interp {L : FirstOrder.Language} (m : Model L) (w : m.W) {ty : Montague.Ty} : FirstOrderConstant L ty → Montague.Ty.Domain m.E m.W ty

At a world of a composition model a symbol denotes what the structure there gives it, the determiners denote those of Quantification, and conjunction and disjunction take the second conjunct first, as a right-branching coordination [t₁ [and t₂]] composes.

Equations

• HeimKratzer.FirstOrderConstant.interp m w (HeimKratzer.FirstOrderConstant.name c) = m.const c w
• HeimKratzer.FirstOrderConstant.interp m w (HeimKratzer.FirstOrderConstant.rel₁ R) = m.pred₁ R w
• HeimKratzer.FirstOrderConstant.interp m w (HeimKratzer.FirstOrderConstant.rel₂ R) = m.pred₂ R w
• HeimKratzer.FirstOrderConstant.interp m w HeimKratzer.FirstOrderConstant.every = Quantifier.GQ.every
• HeimKratzer.FirstOrderConstant.interp m w HeimKratzer.FirstOrderConstant.some = Quantifier.GQ.some
• HeimKratzer.FirstOrderConstant.interp m w HeimKratzer.FirstOrderConstant.no = Quantifier.GQ.no
• HeimKratzer.FirstOrderConstant.interp m w HeimKratzer.FirstOrderConstant.neg = Not
• HeimKratzer.FirstOrderConstant.interp m w HeimKratzer.FirstOrderConstant.conj = fun (q p : Montague.Ty.Domain m.E m.W Montague.Ty.t) => p ∧ q
• HeimKratzer.FirstOrderConstant.interp m w HeimKratzer.FirstOrderConstant.disj = fun (q p : Montague.Ty.Domain m.E m.W Montague.Ty.t) => p ∨ q

def HeimKratzer.Model.lexicon {L : FirstOrder.Language} {X : Type u_1} (m : Model L) (words : X → Option ((ty : Montague.Ty) × FirstOrderConstant L ty)) (w : m.W) : X → Option (Montague.Denotation m.E m.W)

The lexicon a composition model induces at a world from a translation of words into first-order constants.

Equations

• m.lexicon words w x = Option.map (fun (c : (ty : Montague.Ty) × HeimKratzer.FirstOrderConstant L ty) => ⟨c.fst, HeimKratzer.FirstOrderConstant.interp m w c.snd⟩) (words x)

The syntactic model

The syntactic model takes the function and relation symbols of the signature in one universe, so that terms and bounded formulas share it.

@[reducible, inline]

abbrev Montague.Ty.SyntacticDomain (L : FirstOrder.Language) (α : Type w) : Ty → ℕ → Type (max u w)

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.

Equations

• Montague.Ty.SyntacticDomain L α Montague.Ty.e x✝ = L.Term (α ⊕ Fin x✝)
• Montague.Ty.SyntacticDomain L α Montague.Ty.t x✝ = ((k : ℕ) → x✝ ≤ k → L.BoundedFormula α k)
• Montague.Ty.SyntacticDomain L α (σ ⇒ τ) x✝ = ((k : ℕ) → x✝ ≤ k → Montague.Ty.SyntacticDomain L α σ k → Montague.Ty.SyntacticDomain L α τ k)
• Montague.Ty.SyntacticDomain L α σ.intens x✝ = Montague.Ty.SyntacticDomain L α σ x✝
• Montague.Ty.SyntacticDomain L α x✝¹ x✝ = PUnit.{max (?u.10 + 1) (?u.9 + 1)}

def Montague.Ty.SyntacticDomain.applyNext {L : FirstOrder.Language} {α : Type w} {k j : ℕ} (P : SyntacticDomain L α (e ⇒ t) k) (h : k ≤ j) : L.BoundedFormula α (j + 1)

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.

Equations

• P.applyNext h = P (j + 1) ⋯ (FirstOrder.Language.var (Sum.inr (Fin.last j))) (j + 1) ⋯

def Montague.Ty.Realizes {L : FirstOrder.Language} {α : Type w} {M W D : Type} (S : L.Structure M) (v : α → M) (ty : Ty) (n : ℕ) : (Fin n → M) → SyntacticDomain L α ty n → Domain M W ty D → Prop

The logical relation between the syntactic model and the standard one over a structure, 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.

Equations

• One or more equations did not get rendered due to their size.
• Montague.Ty.Realizes S v Montague.Ty.e x✝² x✝¹ x✝ a = (FirstOrder.Language.Term.realize (Sum.elim v x✝¹) x✝ = a)
• Montague.Ty.Realizes S v Montague.Ty.t x✝² x✝¹ x✝ p = ∀ (k : ℕ) (hk : x✝² ≤ k) (ys : Fin k → M), ys ∘ Fin.castLE hk = x✝¹ → ((x✝ k hk).Realize v ys ↔ p)
• Montague.Ty.Realizes S v σ.intens x✝² x✝¹ x✝ a = ∀ (w : W), Montague.Ty.Realizes S v σ x✝² x✝¹ x✝ (a w)
• Montague.Ty.Realizes S v x✝⁴ x✝³ x✝² x✝¹ x✝ = True

def HeimKratzer.Mode.readback {L : FirstOrder.Language} {α : Type w} {σ₁ σ₂ τ : Montague.Ty} {n : ℕ} : Mode σ₁ σ₂ τ → Montague.Ty.SyntacticDomain L α σ₁ n → Montague.Ty.SyntacticDomain L α σ₂ n → Montague.Ty.SyntacticDomain L α τ n

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.

Equations

• One or more equations did not get rendered due to their size.
• HeimKratzer.Mode.functionalLeft.readback f x✝ = f n ⋯ x✝
• HeimKratzer.Mode.functionalRight.readback x✝ f = f n ⋯ x✝
• HeimKratzer.Mode.intensionalLeft.readback f x✝ = f n ⋯ x✝
• HeimKratzer.Mode.intensionalRight.readback x✝ f = f n ⋯ x✝
• HeimKratzer.Mode.predicateModification.readback p q = fun (k : ℕ) (hk : n ≤ k) (x : Montague.Ty.SyntacticDomain L α Montague.Ty.e k) (j : ℕ) (hj : k ≤ j) => p k hk x j hj ⊓ q k hk x j hj

def HeimKratzer.FirstOrderConstant.readback {L : FirstOrder.Language} {α : Type w} {ty : Montague.Ty} (n : ℕ) : FirstOrderConstant L ty → Montague.Ty.SyntacticDomain L α ty n

In the syntactic model a symbol is an atom, a determiner binds the next bound variable where its scope is complete, and negation and the connectives are the formula connectives.

Equations

• One or more equations did not get rendered due to their size.
• HeimKratzer.FirstOrderConstant.readback x✝ (HeimKratzer.FirstOrderConstant.name c) = c.term
• HeimKratzer.FirstOrderConstant.readback x✝ HeimKratzer.FirstOrderConstant.neg = fun (x : ℕ) (x_1 : x✝ ≤ x) (φ : Montague.Ty.SyntacticDomain L α Montague.Ty.t x) (j : ℕ) (hj : x ≤ j) => (φ j hj).not

def HeimKratzer.Term.readback {L : FirstOrder.Language} {α : Type w} {K : Montague.Ty → Type u_1} (R : {ty : Montague.Ty} → (n : ℕ) → K ty → Montague.Ty.SyntacticDomain L α ty n) (n : ℕ) (ρ : ℕ → L.Term (α ⊕ Fin n)) {ty : Montague.Ty} : Term K ty → Montague.Ty.SyntacticDomain L α ty n

The readback of a term in the syntactic model, given readbacks of its constants, with n bound variables in scope and a valuation ρ of its variables in terms. An abstraction reads back to a function at every larger number of bound variables, under ρ carried there and updated at its variable.

Equations

• One or more equations did not get rendered due to their size.
• HeimKratzer.Term.readback R n ρ (HeimKratzer.Term.const c) = R n c
• HeimKratzer.Term.readback R n ρ (HeimKratzer.Term.var i) = ρ i

def HeimKratzer.Term.toFormula {L : FirstOrder.Language} (u : Term (FirstOrderConstant L) Montague.Ty.t) : L.Formula ℕ

The first-order formula a logical form over the first-order constants reads back to, whose free variables are the logical form's variables.

Equations

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

Soundness of the readback

theorem HeimKratzer.Mode.realizes_readback {L : FirstOrder.Language} {α : Type w} {M W D : Type} (S : L.Structure M) (v : α → M) {σ₁ σ₂ τ : Montague.Ty} (μ : Mode σ₁ σ₂ τ) {n : ℕ} {xs : Fin n → M} {a : Montague.Ty.SyntacticDomain L α σ₁ n} {b : Montague.Ty.SyntacticDomain L α σ₂ n} {a' : Montague.Ty.Domain M W σ₁ D} {b' : Montague.Ty.Domain M W σ₂ D} (ha : Montague.Ty.Realizes S v σ₁ n xs a a') (hb : Montague.Ty.Realizes S v σ₂ n xs b b') : Montague.Ty.Realizes S v τ n xs (μ.readback a b) (μ.eval a' b')

A composition mode preserves the logical relation.

theorem HeimKratzer.Term.realizes_readback {L : FirstOrder.Language} {α : Type w} {M W D : Type} (S : L.Structure M) (v : α → M) {K : Montague.Ty → Type u_1} {R : {ty : Montague.Ty} → (n : ℕ) → K ty → Montague.Ty.SyntacticDomain L α ty n} {I : {ty : Montague.Ty} → K ty → Montague.Ty.Domain M W ty D} (hR : ∀ {ty : Montague.Ty} (c : K ty) (n : ℕ) (xs : Fin n → M), Montague.Ty.Realizes S v ty n xs (R n c) (I c)) {ty : Montague.Ty} (u : Term K ty) {n : ℕ} {ρ : ℕ → L.Term (α ⊕ Fin n)} {xs : Fin n → M} {g : Assignment M} (hρ : ∀ (i : ℕ), Montague.Ty.Realizes S v Montague.Ty.e n xs (ρ i) (g i)) : Montague.Ty.Realizes S v ty n xs (readback (fun {ty : Montague.Ty} => R) n ρ u) (eval (fun {ty : Montague.Ty} => I) g u)

When the readbacks of the constants realize their denotations, the readback of a term under a valuation of its variables realizes the term's denotation under the assignment that valuation realizes. This is the fundamental lemma of the logical relation.

theorem HeimKratzer.FirstOrderConstant.realizes_readback {L : FirstOrder.Language} {α : Type w} (m : Model L) (w : m.W) (v : α → m.E) {ty : Montague.Ty} (c : FirstOrderConstant L ty) (n : ℕ) (xs : Fin n → m.E) : Montague.Ty.Realizes (m.interp w) v ty n xs (readback n c) (interp m w c)

The readbacks of the first-order constants realize their denotations in a composition model at a world.

theorem HeimKratzer.Term.realizeAt_toFormula {L : FirstOrder.Language} (m : Model L) (w : m.W) (u : Term (FirstOrderConstant L) Montague.Ty.t) (g : Assignment m.E) : u.toFormula.RealizeAt m.interp w g ↔ eval (fun {ty : Montague.Ty} => FirstOrderConstant.interp m w) g u

A first-order logical form denotes, at a world of a composition model and under an assignment, the realization of its readback there.

Trees

def HeimKratzer.Tree.HoldsAt {C : Type} {X : Type u_1} {E W : Type} (lex : X → Option (Montague.Denotation E W)) (g : Assignment E) (t : PhraseStructure.Tree C X) : Prop

A tree holds under a lexicon and an assignment when it composes to a true truth value.

Equations

• HeimKratzer.Tree.HoldsAt lex g t = ∃ (p : Id (Montague.Ty.Domain E W Montague.Ty.t)), HeimKratzer.Tree.interp lex g t = some ⟨Montague.Ty.t, p⟩ ∧ p

theorem HeimKratzer.Tree.holdsAt_iff_eval {L : FirstOrder.Language} {C : Type} {X : Type u_1} {words : X → Option ((ty : Montague.Ty) × FirstOrderConstant L ty)} (m : Model L) (w : m.W) {t : PhraseStructure.Tree C X} {u : Term (FirstOrderConstant L) Montague.Ty.t} (h : translate words t = some ⟨Montague.Ty.t, u⟩) (g : Assignment m.E) : HoldsAt (m.lexicon words w) g t ↔ Term.eval (fun {ty : Montague.Ty} => FirstOrderConstant.interp m w) g u

A tree that translates to a logical form of type t holds where the logical form is true.

theorem HeimKratzer.Tree.holdsAt_iff_realizeAt {L : FirstOrder.Language} {C : Type} {X : Type u_1} {words : X → Option ((ty : Montague.Ty) × FirstOrderConstant L ty)} (m : Model L) (w : m.W) {t : PhraseStructure.Tree C X} {u : Term (FirstOrderConstant L) Montague.Ty.t} (h : translate words t = some ⟨Montague.Ty.t, u⟩) (g : Assignment m.E) : HoldsAt (m.lexicon words w) g t ↔ u.toFormula.RealizeAt m.interp w g

A tree that translates to a logical form of type t holds where the readback of the logical form is realized.

theorem HeimKratzer.Tree.holdsAt_of_models {L : FirstOrder.Language} {C : Type} {X : Type u_1} {words : X → Option ((ty : Montague.Ty) × FirstOrderConstant L ty)} {t₁ t₂ : PhraseStructure.Tree C X} {u₁ u₂ : Term (FirstOrderConstant L) Montague.Ty.t} (h₁ : translate words t₁ = some ⟨Montague.Ty.t, u₁⟩) (h₂ : translate words t₂ = some ⟨Montague.Ty.t, u₂⟩) (hmod : ∀ (M : Type) (S : L.Structure M) (v : ℕ → M), u₁.toFormula.Realize v → u₂.toFormula.Realize v) (m : Model L) (w : m.W) (g : Assignment m.E) : HoldsAt (m.lexicon words w) g t₁ → HoldsAt (m.lexicon words w) g t₂

First-order consequence between the readbacks of two trees yields entailment between the trees in every composition model, at every world and under every assignment.

Consequence and compactness

For universe-0 languages, composition models and mathlib's bundled models coincide: entailment between trees over composition models with nonempty domains is first-order consequence over the empty theory, and compactness transfers to families of trees. Mathlib's ModelType has nonempty carriers, hence the restriction to nonempty domains, which is standard in the study of generalized quantifiers.

def HeimKratzer.Model.ofStructure {L : FirstOrder.Language} (M : Type) (S : L.Structure M) : Model L

A first-order structure as a one-world composition model.

Equations

• HeimKratzer.Model.ofStructure M S = { E := M, W := Unit, interp := fun (x : Unit) => S }

theorem HeimKratzer.Tree.models_imp_iff_entails {L₀ : FirstOrder.Language} {C : Type} {X : Type u_1} {words : X → Option ((ty : Montague.Ty) × FirstOrderConstant L₀ ty)} {t₁ t₂ : PhraseStructure.Tree C X} {u₁ u₂ : Term (FirstOrderConstant L₀) Montague.Ty.t} (h₁ : translate words t₁ = some ⟨Montague.Ty.t, u₁⟩) (h₂ : translate words t₂ = some ⟨Montague.Ty.t, u₂⟩) : ∅ ⊨ᵇ u₁.toFormula.imp u₂.toFormula ↔ ∀ (m : Model L₀), Nonempty m.E → ∀ (w : m.W) (g : Assignment m.E), HoldsAt (m.lexicon words w) g t₁ → HoldsAt (m.lexicon words w) g t₂

Over composition models with nonempty domains, entailment between two trees is mathlib's ⊨ᵇ between their readbacks over the empty theory.

theorem HeimKratzer.Tree.holdsAt_compactness {L₀ : FirstOrder.Language} {C : Type} {X : Type u_1} {words : X → Option ((ty : Montague.Ty) × FirstOrderConstant L₀ ty)} {ι : Type} {trees : ι → PhraseStructure.Tree C X} {us : ι → Term (FirstOrderConstant L₀) Montague.Ty.t} (hc : ∀ (i : ι), translate words (trees i) = some ⟨Montague.Ty.t, us i⟩) (hcl : ∀ (i : ι), FirstOrder.Language.BoundedFormula.freeVarFinset (us i).toFormula = ∅) : (∃ (m : Model L₀) (_ : Nonempty m.E) (w : m.W) (g : Assignment m.E), ∀ (i : ι), HoldsAt (m.lexicon words w) g (trees i)) ↔ ∀ (s : Finset ι), ∃ (m : Model L₀) (_ : Nonempty m.E) (w : m.W) (g : Assignment m.E), ∀ i ∈ s, HoldsAt (m.lexicon words w) g (trees i)

A family of trees whose readbacks are closed is jointly true in a composition model with a nonempty domain iff every finite subfamily is. The nontrivial direction is mathlib's compactness theorem Theory.isSatisfiable_iff_isFinitelySatisfiable.