Docs / Semantics / Composition / FirstOrder

The first-order fragment of type-driven composition

import Linglib.Semantics.Composition.FirstOrder

Source

A logical form built only from names, predicates, the determiners every, some and no, and the truth-functional connectives reads back to a first-order formula with the same truth conditions, soundly. So a tree holds exactly where its readback is true, entailment between trees is first-order consequence, and families of trees satisfy compactness.

Main definitions

Implementation notes

The syntactic model is built from mathlib's terms and bounded formulas, and 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

First-order constants

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.

inductive Montague.FirstOrderConstantL60–72
(L : FirstOrder.Language) :
Ty → Type (max u v)

Used by Montague.FirstOrderConstant.interp, Montague.Model.lexicon, Montague.FirstOrderConstant.readback, Montague.Term.toFormula, Montague.FirstOrderConstant.realizes_readback, Montague.Term.realizeAt_toFormula, PhraseStructure.Tree.holdsAt_iff_eval, PhraseStructure.Tree.holdsAt_iff_realizeAt, PhraseStructure.Tree.holdsAt_of_models, PhraseStructure.Tree.models_imp_iff_entails, PhraseStructure.Tree.holdsAt_compactness

Used in BarwiseCooper1981, HeimKratzer1998

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.

def Montague.FirstOrderConstant.interpL74–87
{L : FirstOrder.Language} (m : Model L) (w : m.W) {ty : Ty} :
FirstOrderConstant L ty → Ty.Domain m.E m.W ty
Equations

Built from

Used by Montague.Model.lexicon, Montague.FirstOrderConstant.realizes_readback, Montague.Term.realizeAt_toFormula, PhraseStructure.Tree.holdsAt_iff_eval

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

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

Built from ,

Used by PhraseStructure.Tree.holdsAt_iff_eval, PhraseStructure.Tree.holdsAt_iff_realizeAt, PhraseStructure.Tree.holdsAt_of_models, PhraseStructure.Tree.models_imp_iff_entails, PhraseStructure.Tree.holdsAt_compactness

Used in BarwiseCooper1981, HeimKratzer1998

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.

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. The other sorts, worlds among them, are trivial, so an intension is a function that ignores its world.

@[reducible, inline] abbrev Montague.Ty.SyntacticDomainL102–110
(L : FirstOrder.Language) (α : Type w) :
Ty → ℕ → Type (max u w)

Used by Montague.Ty.SyntacticDomain.applyNext, Montague.Ty.Realizes, Montague.Mode.readback, Montague.FirstOrderConstant.readback, Montague.Term.readback, Montague.Mode.realizes_readback, Montague.Term.realizes_readback

L112–116

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.

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

The definition is too large to print here; read it in the source.

Built from

Used by Montague.Mode.realizes_readback, Montague.Term.realizes_readback, Montague.FirstOrderConstant.realizes_readback

L141–158
L160–175

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.

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

The definition is too large to print here; read it in the source.

Built from ,

Used by Montague.Term.toFormula, Montague.Term.realizes_readback

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

def Montague.Term.toFormulaL192–195
{L : FirstOrder.Language} (u : Term individualIndices (FirstOrderConstant L) Ty.t) :
L.Formula ℕ

Built from , ,

Used by Montague.Term.realizeAt_toFormula, PhraseStructure.Tree.holdsAt_iff_realizeAt, PhraseStructure.Tree.holdsAt_of_models, PhraseStructure.Tree.models_imp_iff_entails, PhraseStructure.Tree.holdsAt_compactness

Soundness of the readback

L230–261

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 Montague.Term.realizes_readbackL263–285
{L : FirstOrder.Language} {α : Type w} {M W : Type} {Q : Sorts} (S : L.Structure M) (v : α → M) {K : Ty → Type u_1} {R : {ty : Ty} → (n : ℕ) → K ty → Ty.SyntacticDomain L α ty n} {I : {ty : Ty} → K ty → Ty.Domain M W ty Q} (hR : ∀ {ty : Ty} (c : K ty) (n : ℕ) (xs : Fin n → M), Ty.Realizes S v ty n xs (R n c) (I c)) {ty : Ty} (u : Term individualIndices K ty) {n : ℕ} {ρ : ℕ → L.Term (α ⊕ Fin n)} {xs : Fin n → M} {g : Assignment M} (hρ : ∀ (i : ℕ), Ty.Realizes S v Ty.e n xs (ρ i) (g i)) :
Ty.Realizes S v ty n xs (readback (fun {ty : Ty} => R) n ρ u) (eval (fun {ty : Ty} => I) g u)

Built from , ,

L287–342
L344–352

Trees

L377–384

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

theorem PhraseStructure.Tree.holdsAt_iff_realizeAtL386–393
{L : FirstOrder.Language} {C : Type} {X : Type u_1} {words : X → Option ((ty : Montague.Ty) × Montague.FirstOrderConstant L ty)} (m : Montague.Model L) (w : m.W) {t : Tree C X} {u : Montague.Term Montague.individualIndices (Montague.FirstOrderConstant L) Montague.Ty.t} (h : translate Montague.individualIndices 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

Built from , ,

L395–406

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.

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

theorem PhraseStructure.Tree.models_imp_iff_entailsL426–447
{L₀ : FirstOrder.Language} {C : Type} {X : Type u_1} {words : X → Option ((ty : Montague.Ty) × Montague.FirstOrderConstant L₀ ty)} {t₁ t₂ : Tree C X} {u₁ u₂ : Montague.Term Montague.individualIndices (Montague.FirstOrderConstant L₀) Montague.Ty.t} (h₁ : translate Montague.individualIndices words t₁ = some ⟨Montague.Ty.t, u₁⟩) (h₂ : translate Montague.individualIndices words t₂ = some ⟨Montague.Ty.t, u₂⟩) :
∅ ⊨ᵇ u₁.toFormula.imp u₂.toFormula ↔ ∀ (m : Montague.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₂

Built from , ,

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.

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

Built from , ,