Reduction: the FO fragment of type-driven composition

Compiles the first-order fragment of [HK98] trees into mathlib FirstOrder.Language.Formulas and proves agreement with the engine: whenever compileFO succeeds, the denotation Tree.interp composes is equivalent to mathlib Realize of the compiled formula over the model — the same triangle Semantics/Dynamic/DRS/Reduction.lean proves for DRT.

Trace indices are the formulas' free-variable type (ℕ), so the Heim-Kratzer bind index is the variable name, and assignment update g[n ↦ x] on the engine side is literally Function.update on the realize side. Quantifiers bind exactly one trace, so closure is by the computable singleton binders Formula.all₁ / Formula.ex₁ (mathlib's iAlls/iExs are noncomputable).

Main declarations

• FOWords, Model.lexiconFO — the logical vocabulary over a naming-map lexicon; FOWords.FreshFor, LexNaming.Disjoint — well-formedness
• compileFO — the partial compiler over QR'd Heim-Kratzer tree shapes
• interp_compileFO, holdsAt_iff_realize — the agreement theorem
• holdsAt_of_models — consequence transfer (cross-model entailment from first-order consequence)

Most (and the other proportional determiners) is deliberately outside the compiled fragment: its first-order undefinability is the planned Barwise-Cooper payoff theorem, and the principled reason compileFO is partial.

The logical vocabulary

structure Semantics.Composition.FOWords : Type

Word forms for the compiled logical vocabulary, parameterizable per fragment/language.

• every : String
• some_ : String
• no : String
• not_ : String
• and_ : String
• or_ : String

def Semantics.Composition.FOWords.lexicon (fw : FOWords) (E W : Type) : Montague.Lexicon E W

The logical vocabulary's lexicon entries: GQ denotations from Quantification, truth-functional connectives from Intensional. The connectives flip arguments so that [t₁ [and t₂]] composes to ⟦t₁⟧ ∧ ⟦t₂⟧.

Equations

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

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

A naming-map lexicon extended with the logical vocabulary. Content words take priority; FOWords.FreshFor rules out collisions.

Equations

• m.lexiconFO fw nm w s = (m.lexiconAt nm w s <|> fw.lexicon m.E m.W s)

def Semantics.Composition.FOWords.FreshFor {L : FirstOrder.Language} (fw : FOWords) (nm : LexNaming L) : Prop

The logical word forms are fresh for the naming maps.

Equations

• fw.FreshFor nm = ∀ s ∈ [fw.every, fw.some_, fw.no, fw.not_, fw.and_, fw.or_], nm.names s = none ∧ nm.preds₁ s = none ∧ nm.preds₂ s = none

structure Semantics.Composition.LexNaming.Disjoint {L : FirstOrder.Language} (nm : LexNaming L) : Prop

Each word form names at most one kind of symbol, so the compiler's classification of a word agrees with the lexicon's lookup order.

• names_of_preds₁ (s : String) (R : L.Relations 1) : nm.preds₁ s = some R → nm.names s = none
• names_of_preds₂ (s : String) (R : L.Relations 2) : nm.preds₂ s = some R → nm.names s = none
• preds₁_of_preds₂ (s : String) (R : L.Relations 2) : nm.preds₂ s = some R → nm.preds₁ s = none

The compiler

Recognized (QR'd Heim-Kratzer) shapes: name/trace–verb predication with optional object, sentence negation [not t], sentence coordination [t₁ [and t₂]], and quantified clauses [[Q N] [bind k body]]. Everything else — in particular most — is outside the fragment and compiles to none.

def Semantics.Composition.compileTerm {L : FirstOrder.Language} (nm : LexNaming L) : Syntax.Tree Unit String → Option (L.Term ℕ)

Compile an entity subtree: a proper name or a trace.

Equations

• Semantics.Composition.compileTerm nm (Syntax.Tree.terminal a s) = Option.map FirstOrder.Language.Constants.term (nm.names s)
• Semantics.Composition.compileTerm nm (Syntax.Tree.trace k a) = some (FirstOrder.Language.var k)
• Semantics.Composition.compileTerm nm x✝ = none

def Semantics.Composition.compilePred {L : FirstOrder.Language} (nm : LexNaming L) (τ : L.Term ℕ) : Syntax.Tree Unit String → Option (L.Formula ℕ)

Compile a predicate subtree applied to a subject term: an intransitive verb, or a transitive verb with a name/trace object.

Equations

• One or more equations did not get rendered due to their size.
• Semantics.Composition.compilePred nm τ (Syntax.Tree.terminal a v) = Option.map (fun (R : L.Relations 1) => R.formula₁ τ) (nm.preds₁ v)
• Semantics.Composition.compilePred nm τ x✝ = none

def Semantics.Composition.compileFO {L : FirstOrder.Language} (fw : FOWords) (nm : LexNaming L) : Syntax.Tree Unit String → Option (L.Formula ℕ)

Compile the FO fragment of a tree to a first-order formula with trace indices as free variables. Partial: none outside the fragment.

Equations

• One or more equations did not get rendered due to their size.
• Semantics.Composition.compileFO fw nm (Syntax.Tree.node a [Syntax.Tree.trace k a_1, r]) = Semantics.Composition.compilePred nm (FirstOrder.Language.var k) r
• Semantics.Composition.compileFO fw nm x✝ = none

Lookup lemmas

def Semantics.Composition.FOWords.Nodup (fw : FOWords) : Prop

The six logical word forms are pairwise distinct.

Equations

• fw.Nodup = [fw.every, fw.some_, fw.no, fw.not_, fw.and_, fw.or_].Nodup

theorem Semantics.Composition.Model.lexiconFO_names {L : FirstOrder.Language} (m : Model L) (fw : FOWords) (nm : LexNaming L) (w : m.W) {s : String} {c : L.Constants} (h : nm.names s = some c) : m.lexiconFO fw nm w s = some { ty := Intensional.Ty.e, denot := m.const c w }

theorem Semantics.Composition.Model.lexiconFO_preds₁ {L : FirstOrder.Language} (m : Model L) (fw : FOWords) (nm : LexNaming L) (w : m.W) {s : String} {R : L.Relations 1} (h : nm.preds₁ s = some R) (h₀ : nm.names s = none) : m.lexiconFO fw nm w s = some { ty := Intensional.Ty.e ⇒ Intensional.Ty.t, denot := m.pred₁ext R w }

theorem Semantics.Composition.Model.lexiconFO_preds₂ {L : FirstOrder.Language} (m : Model L) (fw : FOWords) (nm : LexNaming L) (w : m.W) {s : String} {R : L.Relations 2} (h : nm.preds₂ s = some R) (h₀ : nm.names s = none) (h₁ : nm.preds₁ s = none) : m.lexiconFO fw nm w s = some { ty := Intensional.Ty.e ⇒ Intensional.Ty.e ⇒ Intensional.Ty.t, denot := m.pred₂ext R w }

theorem Semantics.Composition.Model.lexiconFO_fresh {L : FirstOrder.Language} (m : Model L) (fw : FOWords) (nm : LexNaming L) (w : m.W) {s : String} (h₀ : nm.names s = none) (h₁ : nm.preds₁ s = none) (h₂ : nm.preds₂ s = none) : m.lexiconFO fw nm w s = fw.lexicon m.E m.W s

At a word fresh for the naming maps, lookup falls through to the logical vocabulary.

theorem Semantics.Composition.FOWords.lexicon_every {fw : FOWords} (E W : Type) : fw.lexicon E W fw.every = some { ty := (Intensional.Ty.e ⇒ Intensional.Ty.t) ⇒ (Intensional.Ty.e ⇒ Intensional.Ty.t) ⇒ Intensional.Ty.t, denot := Quantification.every_sem }

theorem Semantics.Composition.FOWords.lexicon_some {fw : FOWords} (E W : Type) (hnd : fw.Nodup) : fw.lexicon E W fw.some_ = some { ty := (Intensional.Ty.e ⇒ Intensional.Ty.t) ⇒ (Intensional.Ty.e ⇒ Intensional.Ty.t) ⇒ Intensional.Ty.t, denot := Quantification.some_sem }

theorem Semantics.Composition.FOWords.lexicon_no {fw : FOWords} (E W : Type) (hnd : fw.Nodup) : fw.lexicon E W fw.no = some { ty := (Intensional.Ty.e ⇒ Intensional.Ty.t) ⇒ (Intensional.Ty.e ⇒ Intensional.Ty.t) ⇒ Intensional.Ty.t, denot := Quantification.no_sem }

theorem Semantics.Composition.FOWords.lexicon_not {fw : FOWords} (E W : Type) (hnd : fw.Nodup) : fw.lexicon E W fw.not_ = some { ty := Intensional.Ty.t ⇒ Intensional.Ty.t, denot := Intensional.neg }

theorem Semantics.Composition.FOWords.lexicon_and {fw : FOWords} (E W : Type) (hnd : fw.Nodup) : fw.lexicon E W fw.and_ = some { ty := Intensional.Ty.t ⇒ Intensional.Ty.t ⇒ Intensional.Ty.t, denot := fun (q p : Intensional.Denot E W Intensional.Ty.t) => Intensional.conj p q }

theorem Semantics.Composition.FOWords.lexicon_or {fw : FOWords} (E W : Type) (hnd : fw.Nodup) : fw.lexicon E W fw.or_ = some { ty := Intensional.Ty.t ⇒ Intensional.Ty.t ⇒ Intensional.Ty.t, denot := fun (q p : Intensional.Denot E W Intensional.Ty.t) => Intensional.disj p q }

theorem Semantics.Composition.FOWords.FreshFor.at {L : FirstOrder.Language} {fw : FOWords} {nm : LexNaming L} (h : fw.FreshFor nm) {s : String} (hs : s ∈ [fw.every, fw.some_, fw.no, fw.not_, fw.and_, fw.or_]) : nm.names s = none ∧ nm.preds₁ s = none ∧ nm.preds₂ s = none

Extract the naming-map-freshness triple for a logical word.

Realization at a model's world

Model carries structures as terms, so Realize needs the instance fixed per world; realizeAt/termAt package that.

def Semantics.Composition.Model.realizeAt {L : FirstOrder.Language} (m : Model L) (w : m.W) (φ : L.Formula ℕ) (g : Core.Assignment m.E) : Prop

Realize a formula over the model's structure at world w.

Equations

• m.realizeAt w φ g = φ.Realize g

def Semantics.Composition.Model.termAt {L : FirstOrder.Language} (m : Model L) (w : m.W) (τ : L.Term ℕ) (g : Core.Assignment m.E) : m.E

Realize a term over the model's structure at world w.

Equations

• m.termAt w τ g = FirstOrder.Language.Term.realize g τ

theorem Semantics.Composition.Model.termAt_var {L : FirstOrder.Language} (m : Model L) (w : m.W) (g : Core.Assignment m.E) (k : ℕ) : m.termAt w (FirstOrder.Language.var k) g = g k

theorem Semantics.Composition.Model.termAt_const {L : FirstOrder.Language} (m : Model L) (w : m.W) (g : Core.Assignment m.E) (c : L.Constants) : m.termAt w c.term g = m.const c w

theorem Semantics.Composition.Model.realizeAt_not {L : FirstOrder.Language} (m : Model L) (w : m.W) (g : Core.Assignment m.E) (φ : L.Formula ℕ) : m.realizeAt w φ.not g ↔ ¬m.realizeAt w φ g

theorem Semantics.Composition.Model.realizeAt_inf {L : FirstOrder.Language} (m : Model L) (w : m.W) (g : Core.Assignment m.E) (φ ψ : L.Formula ℕ) : m.realizeAt w (φ ⊓ ψ) g ↔ m.realizeAt w φ g ∧ m.realizeAt w ψ g

theorem Semantics.Composition.Model.realizeAt_sup {L : FirstOrder.Language} (m : Model L) (w : m.W) (g : Core.Assignment m.E) (φ ψ : L.Formula ℕ) : m.realizeAt w (φ ⊔ ψ) g ↔ m.realizeAt w φ g ∨ m.realizeAt w ψ g

theorem Semantics.Composition.Model.realizeAt_imp {L : FirstOrder.Language} (m : Model L) (w : m.W) (g : Core.Assignment m.E) (φ ψ : L.Formula ℕ) : m.realizeAt w (φ.imp ψ) g ↔ m.realizeAt w φ g → m.realizeAt w ψ g

theorem Semantics.Composition.Model.realizeAt_all₁ {L : FirstOrder.Language} (m : Model L) (w : m.W) (g : Core.Assignment m.E) (k : ℕ) (φ : L.Formula ℕ) : m.realizeAt w (FirstOrder.Language.Formula.all₁ k φ) g ↔ ∀ (x : m.E), m.realizeAt w φ (Function.update g k x)

theorem Semantics.Composition.Model.realizeAt_ex₁ {L : FirstOrder.Language} (m : Model L) (w : m.W) (g : Core.Assignment m.E) (k : ℕ) (φ : L.Formula ℕ) : m.realizeAt w (FirstOrder.Language.Formula.ex₁ k φ) g ↔ ∃ (x : m.E), m.realizeAt w φ (Function.update g k x)

theorem Semantics.Composition.Model.realizeAt_formula₁ {L : FirstOrder.Language} (m : Model L) (w : m.W) (g : Core.Assignment m.E) (R : L.Relations 1) (τ : L.Term ℕ) : m.realizeAt w (R.formula₁ τ) g ↔ m.pred₁ext R w (m.termAt w τ g)

Atomic agreement, unary: realization of R(τ) is the model-sourced extensional predicate at the term's value.

theorem Semantics.Composition.Model.realizeAt_formula₂ {L : FirstOrder.Language} (m : Model L) (w : m.W) (g : Core.Assignment m.E) (R : L.Relations 2) (τ₁ τ₂ : L.Term ℕ) : m.realizeAt w (R.formula₂ τ₁ τ₂) g ↔ m.pred₂ext R w (m.termAt w τ₂ g) (m.termAt w τ₁ g)

Atomic agreement, binary: realization of R(τ₁, τ₂) is the model-sourced object-first relation at the terms' values (subject first in the vector).

Engine reduction helpers (at M = Id)

Agreement

theorem Semantics.Composition.interp_compileTerm {L : FirstOrder.Language} (m : Model L) (fw : FOWords) (nm : LexNaming L) (w : m.W) (g : Core.Assignment m.E) {t : Syntax.Tree Unit String} {τ : L.Term ℕ} : compileTerm nm t = some τ → Tree.interp m.E m.W (m.lexiconFO fw nm w) g t = some { ty := Intensional.Ty.e, val := m.termAt w τ g }

Entity-subtree agreement: a compiled term's engine value is its realization over the model.

theorem Semantics.Composition.interp_compilePred {L : FirstOrder.Language} (m : Model L) (fw : FOWords) (nm : LexNaming L) (w : m.W) (hdj : nm.Disjoint) (g : Core.Assignment m.E) {subj : Syntax.Tree Unit String} {τ : L.Term ℕ} (hsubj : compileTerm nm subj = some τ) {r : Syntax.Tree Unit String} {φ : L.Formula ℕ} : compilePred nm τ r = some φ → ∀ (c : Unit), Tree.interp m.E m.W (m.lexiconFO fw nm w) g (Syntax.Tree.node c [subj, r]) = some { ty := Intensional.Ty.t, val := m.realizeAt w φ g }

Predication agreement: subject term + predicate subtree compose to the compiled atom's realization.

theorem Semantics.Composition.interp_compileFO {L : FirstOrder.Language} (m : Model L) (fw : FOWords) (nm : LexNaming L) (w : m.W) (hnd : fw.Nodup) (hfr : fw.FreshFor nm) (hdj : nm.Disjoint) (t : Syntax.Tree Unit String) {φ : L.Formula ℕ} (g : Core.Assignment m.E) : compileFO fw nm t = some φ → Tree.interp m.E m.W (m.lexiconFO fw nm w) g t = some { ty := Intensional.Ty.t, val := m.realizeAt w φ g }

The agreement theorem: whenever the compiler succeeds, the engine's composed denotation is the realization of the compiled formula over the model at w — the DRT triangle for type-driven composition.

Truth and consequence transfer

def Semantics.Composition.HoldsAt {L : FirstOrder.Language} (m : Model L) (lex : Montague.Lexicon m.E m.W) (g : Core.Assignment m.E) (t : Syntax.Tree Unit String) : Prop

Truth of a tree at a model's world under an assignment: it composes to a true truth value.

Equations

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

theorem Semantics.Composition.holdsAt_iff_realize {L : FirstOrder.Language} (m : Model L) (fw : FOWords) (nm : LexNaming L) (w : m.W) (hnd : fw.Nodup) (hfr : fw.FreshFor nm) (hdj : nm.Disjoint) {t : Syntax.Tree Unit String} {φ : L.Formula ℕ} (h : compileFO fw nm t = some φ) (g : Core.Assignment m.E) : HoldsAt m (m.lexiconFO fw nm w) g t ↔ m.realizeAt w φ g

theorem Semantics.Composition.holdsAt_of_models {L : FirstOrder.Language} (m : Model L) (fw : FOWords) (nm : LexNaming L) (w : m.W) (hnd : fw.Nodup) (hfr : fw.FreshFor nm) (hdj : nm.Disjoint) {t₁ t₂ : Syntax.Tree Unit String} {φ₁ φ₂ : L.Formula ℕ} (h₁ : compileFO fw nm t₁ = some φ₁) (h₂ : compileFO fw nm t₂ = some φ₂) (hmod : ∀ (M : Type) (S : L.Structure M) (v : ℕ → M), φ₁.Realize v → φ₂.Realize v) (g : Core.Assignment m.E) : HoldsAt m (m.lexiconFO fw nm w) g t₁ → HoldsAt m (m.lexiconFO fw nm w) g t₂

Consequence transfer: first-order consequence between compiled formulas yields cross-model entailment between the trees — for every composition model, world, and assignment.

theorem Semantics.Composition.FOWords.nodup_default : { }.Nodup

The default logical vocabulary is pairwise distinct.

Bridge to mathlib Theory consequence

For universe-0 languages, composition models and mathlib's bundled models coincide: tree entailment over nonempty-domain composition models is first-order consequence over the empty theory, and compactness transfers to families of trees. (ModelType requires nonempty carriers, hence the nonempty-domain restriction — standard in the GQ literature.)

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

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

Equations

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

theorem Semantics.Composition.models_imp_iff_entails {L₀ : FirstOrder.Language} (fw : FOWords) (nm : LexNaming L₀) (hnd : fw.Nodup) (hfr : fw.FreshFor nm) (hdj : nm.Disjoint) {t₁ t₂ : Syntax.Tree Unit String} {φ₁ φ₂ : L₀.Formula ℕ} (h₁ : compileFO fw nm t₁ = some φ₁) (h₂ : compileFO fw nm t₂ = some φ₂) : ∅ ⊨ᵇ φ₁.imp φ₂ ↔ ∀ (m : Model L₀), Nonempty m.E → ∀ (w : m.W) (g : Core.Assignment m.E), HoldsAt m (m.lexiconFO fw nm w) g t₁ → HoldsAt m (m.lexiconFO fw nm w) g t₂

Tree entailment is first-order consequence: mathlib's ⊨ᵇ over the empty theory coincides with cross-model entailment between compiled trees, over nonempty-domain composition models.

Closed trees as sentences, and compactness

theorem Semantics.Composition.holdsAt_compactness {L₀ : FirstOrder.Language} (fw : FOWords) (nm : LexNaming L₀) (hnd : fw.Nodup) (hfr : fw.FreshFor nm) (hdj : nm.Disjoint) {ι : Type} (trees : ι → Syntax.Tree Unit String) (φs : ι → L₀.Formula ℕ) (hc : ∀ (i : ι), compileFO fw nm (trees i) = some (φs i)) (hcl : ∀ (i : ι), FirstOrder.Language.BoundedFormula.freeVarFinset (φs i) = ∅) : (∃ (m : Model L₀) (_ : Nonempty m.E) (w : m.W) (g : Core.Assignment m.E), ∀ (i : ι), HoldsAt m (m.lexiconFO fw nm w) g (trees i)) ↔ ∀ (s : Finset ι), ∃ (m : Model L₀) (_ : Nonempty m.E) (w : m.W) (g : Core.Assignment m.E), ∀ i ∈ s, HoldsAt m (m.lexiconFO fw nm w) g (trees i)

Compactness at the tree level: a family of closed fragment trees is jointly satisfiable in a nonempty-domain composition model iff every finite subfamily is. The nontrivial direction is mathlib's compactness theorem (Theory.isSatisfiable_iff_isFinitelySatisfiable, via ultraproducts).