Relational (dynamic) semantics of DRSs, and its equivalence with verifying embeddings

[Mus96]

Muskens's reformulation of DRT. Conditions denote sets of embeddings (SEM1/2); boxes denote binary relations between embeddings (SEM3, input → output); a box is true under an input embedding a iff some output a' is related to it (p. 148). This is the dynamic / CCP face of DRT, dual to the static verifying-embedding semantics DRS.Realize ([KR93], Def. 1.4.4).

The two semantics are defined independently and proved equivalent — Muskens's remark that the relational interpretation "is in fact equivalent" to Kamp & Reyle's. The equivalence is a theorem, not a definitional identification:

• DRS.toRel_iff_realize — the relation toRel K a a' holds iff a' extends a over K's universe and verifies K (the keystone bridge).
• DRS.trueRel_iff_realize_toFormula — the dynamic truth of a DRS equals its first-order translation's Realize, closing the triangle with Reduction (Realize — toFormula — toRel, each pair related by a proven theorem).

Main declarations

• DRS.toRel / Condition.holds — the relational (SEM3) and set (SEM1/2) denotations.
• DRS.trueRel — relational truth: some output embedding is related to the input.
• DRS.toRel_iff_realize / Condition.holds_iff_realize — equivalence with the static DRS.Realize semantics.
• DRS.occ / DRS.trueRel_congr — occurring referents and the coincidence lemma (denotation depends only on them).
• DRS.toRel_merge — the Merging Lemma: under freshness, merge denotes the sequencing (relational composition) of the two box relations.

Reindexing concrete atomic arguments

A concrete DRS atom .rel R ![k₁, …] interprets (via holds/Realize) to RelMap R (fun i => v (![k₁, …] i)). These @[simp] lemmas reindex that to ![v k₁, …], so truth-condition proofs over concrete DRSs work with the atom's assigned values directly. (No general mathlib form exists — Loogle finds only a buried comp_fin3 in the elliptic-curve files.)

@[simp]

theorem DRT.vecArg₁ {α : Type u_1} {β : Type u_2} (v : α → β) (k : α) : (fun (i : Fin (Nat.succ 0)) => v (![k] i)) = ![v k]

@[simp]

theorem DRT.vecArg₂ {α : Type u_1} {β : Type u_2} (v : α → β) (j k : α) : (fun (i : Fin (Nat.succ 0).succ) => v (![j, k] i)) = ![v j, v k]

@[simp]

theorem DRT.vecArg₃ {α : Type u_1} {β : Type u_2} (v : α → β) (j k l : α) : (fun (i : Fin (Nat.succ 0).succ.succ) => v (![j, k, l] i)) = ![v j, v k, v l]

The relational denotation

def DRT.DRS.toRel {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] : DRS L V → (V → M) → (V → M) → Prop

The relational (dynamic) denotation of a DRS ([Mus96], SEM3): the input-output relation ⟨a, a'⟩ where a' differs from a at most on the universe and verifies every condition.

Equations

• (DRT.DRS.mk U conds).toRel = fun (a a' : V → M) => (∀ x ∉ U, a' x = a x) ∧ DRT.Condition.holdsAll conds a'

def DRT.Condition.holds {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] : Condition L V → (V → M) → Prop

The set denotation of a condition ([Mus96], SEM1/2): the set of embeddings at which it holds. Complex conditions reference the box relation DRS.toRel of their sub-DRSs.

Equations

• (DRT.Condition.rel R args).holds = fun (a : V → M) => FirstOrder.Language.Structure.RelMap R fun (i : Fin n) => a (args i)
• (DRT.Condition.eq u v).holds = fun (a : V → M) => a u = a v
• (DRT.Condition.neg K).holds = fun (a : V → M) => ¬∃ (a' : V → M), K.toRel a a'
• (DRT.Condition.imp ante cons).holds = fun (a : V → M) => ∀ (a' : V → M), ante.toRel a a' → ∃ (a'' : V → M), cons.toRel a' a''
• (DRT.Condition.dis l r).holds = fun (a : V → M) => ∃ (a' : V → M), l.toRel a a' ∨ r.toRel a a'

def DRT.Condition.holdsAll {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] : List (Condition L V) → (V → M) → Prop

Every condition in the list holds at a. A List helper — the higher-order form fails the nested-inductive structural-recursion checker.

Equations

• DRT.Condition.holdsAll [] = fun (x : V → M) => True
• DRT.Condition.holdsAll (c :: cs) = fun (a : V → M) => c.holds a ∧ DRT.Condition.holdsAll cs a

def DRT.DRS.trueRel {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] (K : DRS L V) (a : V → M) : Prop

A DRS is true under an input embedding a iff some output embedding is related to it ([Mus96], p. 148).

Equations

• K.trueRel a = ∃ (a' : V → M), K.toRel a a'

Equivalence with the verifying-embedding semantics

theorem DRT.DRS.toRel_iff_realize {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] (K : DRS L V) (a a' : V → M) : K.toRel a a' ↔ (∀ x ∉ K.referents, a' x = a x) ∧ Realize a' K

Muskens ≡ Kamp & Reyle ([Mus96]): the relational denotation agrees with the static verifying-embedding semantics — toRel K a a' holds iff the output a' extends the input a over K's universe and verifies K.

theorem DRT.Condition.holds_iff_realize {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] (c : Condition L V) (a : V → M) : c.holds a ↔ Realize a c

A condition's set denotation agrees with its static Realize.

theorem DRT.Condition.holdsAll_iff_realizeAll {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] (cs : List (Condition L V)) (a : V → M) : holdsAll cs a ↔ RealizeAll a cs

The list analogue of Condition.holds_iff_realize.

theorem DRT.DRS.trueRel_iff_realize_toFormula {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] (K : DRS L V) (a : V → M) : K.trueRel a ↔ K.toFormula.Realize a

The dynamic truth of a DRS equals its first-order translation's Realize ([Mus96]; [KR93] §1.5) — the third edge of the Realize/toFormula/toRel triangle.

The coincidence lemma

theorem DRT.DRS.trueRel_congr {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] (K : DRS L V) (a₁ a₂ : V → M) (h : Set.EqOn a₁ a₂ ↑K.occ) : K.trueRel a₁ ↔ K.trueRel a₂

Coincidence: a DRS's relational truth depends only on the input embedding's values at its occurring referents. Proved by surgery on the output witness, the load-bearing case being the imp clause of Condition.holds_congr.

theorem DRT.Condition.holds_congr {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] (c : Condition L V) (a₁ a₂ : V → M) (h : Set.EqOn a₁ a₂ ↑c.occ) : c.holds a₁ ↔ c.holds a₂

A condition's set denotation depends only on its occurring referents.

theorem DRT.Condition.holdsAll_congr {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] (cs : List (Condition L V)) (a₁ a₂ : V → M) (h : Set.EqOn a₁ a₂ ↑(occL cs)) : holdsAll cs a₁ ↔ holdsAll cs a₂

The list analogue of Condition.holds_congr.

The merging lemma: sequencing is merge, under freshness

theorem DRT.Condition.holdsAll_append {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] (cs ds : List (Condition L V)) (a : V → M) : holdsAll (cs ++ ds) a ↔ holdsAll cs a ∧ holdsAll ds a

The conjunction of conditions distributes over list append.

theorem DRT.DRS.toRel_merge {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] (K₁ K₂ : DRS L V) (hfresh : ∀ x ∈ K₂.referents, x ∉ Condition.occL K₁.conditions) (a a' : V → M) : (K₁.merge K₂).toRel a a' ↔ ∃ (a'' : V → M), K₁.toRel a a'' ∧ K₂.toRel a'' a'

Merging Lemma ([Mus96], §II.2): when K₂'s universe is fresh for K₁'s conditions, the relation denoted by the merge K₁ ⊕ K₂ is the relational composition (sequencing K₁ ; K₂) of the two box relations — ‖K₁ ⊕ K₂‖ = ‖K₁‖ ∘ ‖K₂‖. This is what gives merge its dynamic meaning.