The box relation: dynamic face of DRS verification

This file gives DRS verification (DRS/Verification.lean) its relational, input–output face. The box relation K.toRel a a' holds when the output a' extends the input a across K and verifies K; a DRS is true under an input iff some output is related to it (the spine's anaphoric closure). This is [Mus96]'s SEM3 format, in the style of [GS91a]; his SEM1/2 clauses — complex conditions as the spine connectives on box relations — are derived characterizations, connecting DRS verification to the connective algebra shared across the dynamic-semantics spine.

Main declarations

• DRS.toRel: the box relation; DRS.trueRel: relational truth, its closure.
• Embedding.verifies_neg_toRel (_imp_, _dis_): complex conditions are the spine connectives on box relations (SEM1/2).
• DRS.trueRel_iff_realize_toFormula: dynamic truth equals the first-order translation's Realize (DRS/Reduction.lean).
• DRS.trueRel_congr: truth reads the input only at the occurring referents.
• DRS.toRel_merge: the Merging Lemma — under freshness, merge denotes the spine sequencing Update.seq of the two box relations.
• DRS.trueRel_map: alphabetic variants have the same truth conditions.

Implementation notes

• Muskens scopes the equivalence of the relational and standard interpretations to constant-free constructs, both sides in the total-assignment rendering (fn. 3–4; see the deviation note in DRS/Verification.lean).
• The relational face (toRel, trueRel) follows the spine's lowerCamel operation names (neg, seq, closure); verification uses the field's own verb, and the first-order reduction speaks mathlib's Formula.Realize.

The box relation

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

The box relation (SEM3), relating an input a to the outputs that extend it across K and verify K.

Equations

• K.toRel a a' = (DRT.Box.Extends K a a' ∧ DRT.Embedding.Verifies a' K)

@[simp]

theorem DRT.DRS.toRel_iff {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] (K : DRS L V) (a a' : Embedding V M) : K.toRel a a' ↔ Box.Extends K a a' ∧ a'.Verifies K

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 — the spine's anaphoric closure.

Equations

• K.trueRel a = K.toRel.closure a

theorem DRT.DRS.trueRel_iff {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] (K : DRS L V) (a : V → M) : K.trueRel a ↔ ∃ (a' : V → M), K.toRel a a'

trueRel unfolded: some output embedding is related to the input.

The spine connectives (SEM1/2)

theorem DRT.Embedding.verifies_neg_toRel {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] (K : DRS L V) (f : Embedding V M) : f.VerifiesCondition (Condition.neg K) ↔ K.toRel.neg f

A negated sub-DRS is the spine's neg of its box relation.

theorem DRT.Embedding.verifies_imp_toRel {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] (a c : DRS L V) (f : Embedding V M) : f.VerifiesCondition (Condition.imp a c) ↔ a.toRel.impl c.toRel f

A conditional is the spine's impl of the boxes' relations.

theorem DRT.Embedding.verifies_dis_toRel {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] (l r : DRS L V) (f : Embedding V M) : f.VerifiesCondition (Condition.dis l r) ↔ l.toRel.disj r.toRel f

A disjunction is the spine's disj of the boxes' relations.

Truth: the triangle, coincidence, and alphabetic variants

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 — the third edge of the Verifies/toFormula/toRel triangle.

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.varFinset) : K.trueRel a₁ ↔ K.trueRel a₂

Coincidence: truth reads the input embedding only at the occurring referents.

theorem DRT.DRS.trueRel_map {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] {W : Type u_1} [DecidableEq W] (e : V ≃ W) (K : DRS L V) (a : Embedding W M) : (map (⇑e) K).trueRel a ↔ K.trueRel (a ∘ ⇑e)

Renaming along a bijection transports dynamic truth: alphabetic variants have the same truth conditions.

The merging lemma: sequencing is merge, under freshness

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 : Disjoint K₂.referents (Condition.varFinsetL K₁.conditions)) : (K₁.merge K₂).toRel = K₁.toRel.seq K₂.toRel

Merging Lemma (§II.2): when K₂'s universe is fresh for K₁'s conditions, the merge K₁ ⊕ K₂ denotes the spine sequencing (relational composition) of the two box relations — ‖K₁ ⊕ K₂‖ = seq ‖K₁‖ ‖K₂‖. This is what gives merge its dynamic meaning.