The box relation: dynamic face of DRS verification

The box relation of a DRS relates an input embedding to the outputs that agree with it off the universe and verify the DRS. It is the box Update.box of Semantics/Dynamic/RegisterStructure.lean over the universe, at the register structure of embeddings, so Muskens's relational semantics of DRT is the general one of boxes. A DRS is true under an input when some output is related to it.

Main declarations

• DRS.toRel: the box relation; DRS.trueRel: truth, its domain.
• verifies_neg_toRel (_imp_, _dis_): complex conditions are the connectives of Update on box relations.
• DRS.trueRel_iff_realize_toFormula: dynamic truth is the truth of the first-order translation (DRS/Reduction.lean).
• DRS.trueRel_congr: truth reads the input only at the free referents.
• DRS.toRel_merge: under freshness, merge denotes the composition of the box relations, as an instance of the semantic Merging Lemma Update.box_comp_box.
• DRS.trueRel_map: alphabetic variants have the same truth conditions.

Implementation notes

Muskens scopes the agreement of his relational semantics with the standard one to constructs without constants, both in total-assignment form (fn. 3–4; see DRS/Verification.lean).

References

• [Mus96]
• [GS91a]

The box relation

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

The box relation of a DRS (SEM3) is the box over its universe testing its conditions.

Equations

• K.toRel = DynamicSemantics.Update.box K.referents {a : V → M | DRT.Verifies a K}

@[simp]

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

The box relation relates an input to the outputs that extend it across the universe and verify the DRS.

def DRT.DRS.trueRel {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] (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 domain of the box relation.

Equations

• K.trueRel a = (a ∈ SetRel.dom K.toRel)

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

A DRS is true under an input iff some output embedding is related to it.

theorem DRT.DRS.trueRel_iff_exists_extends {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] (K : DRS L V) (a : V → M) : K.trueRel a ↔ ∃ (a' : V → M), Box.Extends K a a' ∧ Verifies a' K

A DRS is true under an input iff some extension of the input across the universe verifies it.

The spine connectives (SEM1/2)

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

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

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

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

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

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

Truth reads the input embedding only at the free referents.

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

Renaming along a bijection transports dynamic truth, so 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 = SetRel.comp K₁.toRel K₂.toRel

When K₂'s universe is fresh for K₁'s conditions, the merge K₁ ⊕ K₂ denotes the composition of the two box relations (the Merging Lemma of §II.2). It is the semantic Merging Lemma Update.box_comp_box, since freshness puts K₂'s referents outside the dimension set of K₁'s conditions.