Indexed relational semantics of DRSs

This file defines the base-threaded verification semantics: toRelAt X K f g holds when the output g agrees with the input f on the context base X and verifies K's conditions, sub-boxes entered at the grown base. This is the total-assignment rendering of [KvGR11]'s partial-embedding semantics (Defs. 19, 22, 24): values at established referents persist, as in [KR93]'s original embeddings — in contrast to the flat DRS.toRel (DRS/Dynamics.lean), which freely reassigns re-declared referents ([muskens-1996]'s fn. 4 divergence).

Persistence types the semantics: toRelAt X K is read only at X and, given the referential presupposition K.freeVarFinset ⊆ X, written only at X ∪ U, so a well-formed DRS denotes a spine transition Transition X (X ∪ U) and a proper DRS expresses an information state by acting on ⊥ (Def. 22). The Merging Lemma here needs less than the flat freshness hypothesis — only capture by sub-box universes is fatal, re-declaration is harmless — and lifts to the spine, where the action equation is an instance of functoriality (Transition.apply_comp).

Main declarations

• DRS.toRelAt, Condition.holdsAt: the base-threaded semantics.
• DRS.toRelAt_congr_left, DRS.toRelAt_congr_right: read/write support.
• DRS.transition: a DRS as a spine transition X ⟶ X ∪ U.
• DRS.state: the information state a proper DRS expresses.
• DRS.transition_merge, DRS.state_merge: the Merging Lemma on the spine and the action equation.
• DRS.trueRel_iff_toRelAt: on reuse-free DRSs the flat and indexed semantics have the same truth conditions.

The base-threaded semantics

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

Base-threaded relational semantics (Def. 19 in total-assignment form): the output agrees with the input on the base — established referents persist — and verifies the conditions, with sub-boxes entered at the grown base.

Equations

• DRT.DRS.toRelAt X { referents := U, conditions := conds } = fun (f g : V → M) => Set.EqOn g f ↑X ∧ DRT.Condition.holdsAllAt (X ∪ U) conds g

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

A condition holds at a base under an assignment; sub-DRSs are entered as context extensions of the current base.

Equations

• DRT.Condition.holdsAt X (DRT.Condition.rel R args) = fun (g : V → M) => FirstOrder.Language.Structure.RelMap R fun (i : Fin n) => g (args i)
• DRT.Condition.holdsAt X (DRT.Condition.eq u v) = fun (g : V → M) => g u = g v
• DRT.Condition.holdsAt X (DRT.Condition.neg K) = fun (g : V → M) => ¬∃ (g' : V → M), DRT.DRS.toRelAt X K g g'
• DRT.Condition.holdsAt X (DRT.Condition.imp a c) = fun (g : V → M) => ∀ (g' : V → M), DRT.DRS.toRelAt X a g g' → ∃ (g'' : V → M), DRT.DRS.toRelAt (X ∪ a.referents) c g' g''
• DRT.Condition.holdsAt X (DRT.Condition.dis l r) = fun (g : V → M) => ∃ (g' : V → M), DRT.DRS.toRelAt X l g g' ∨ DRT.DRS.toRelAt X r g g'

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

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

Equations

• DRT.Condition.holdsAllAt X [] = fun (x : V → M) => True
• DRT.Condition.holdsAllAt X (c :: cs) = fun (g : V → M) => DRT.Condition.holdsAt X c g ∧ DRT.Condition.holdsAllAt X cs g

Structural simp API

@[simp]

theorem DRT.DRS.toRelAt_mk {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] (X U : Finset V) (conds : List (Condition L V)) (f g : V → M) : toRelAt X { referents := U, conditions := conds } f g ↔ Set.EqOn g f ↑X ∧ Condition.holdsAllAt (X ∪ U) conds g

@[simp]

theorem DRT.Condition.holdsAt_rel {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] (X : Finset V) {n : ℕ} (R : L.Relations n) (args : Fin n → V) (g : V → M) : holdsAt X (rel R args) g ↔ FirstOrder.Language.Structure.RelMap R fun (i : Fin n) => g (args i)

@[simp]

theorem DRT.Condition.holdsAt_eq {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] (X : Finset V) (u v : V) (g : V → M) : holdsAt X (eq u v) g ↔ g u = g v

@[simp]

theorem DRT.Condition.holdsAt_neg {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] (X : Finset V) (K : DRS L V) (g : V → M) : holdsAt X (neg K) g ↔ ¬∃ (g' : V → M), DRS.toRelAt X K g g'

@[simp]

theorem DRT.Condition.holdsAt_imp {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] (X : Finset V) (a c : DRS L V) (g : V → M) : holdsAt X (imp a c) g ↔ ∀ (g' : V → M), DRS.toRelAt X a g g' → ∃ (g'' : V → M), DRS.toRelAt (X ∪ a.referents) c g' g''

@[simp]

theorem DRT.Condition.holdsAt_dis {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] (X : Finset V) (l r : DRS L V) (g : V → M) : holdsAt X (dis l r) g ↔ ∃ (g' : V → M), DRS.toRelAt X l g g' ∨ DRS.toRelAt X r g g'

@[simp]

theorem DRT.Condition.holdsAllAt_nil {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] (X : Finset V) (g : V → M) : holdsAllAt X [] g

@[simp]

theorem DRT.Condition.holdsAllAt_cons {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] (X : Finset V) (c : Condition L V) (cs : List (Condition L V)) (g : V → M) : holdsAllAt X (c :: cs) g ↔ holdsAt X c g ∧ holdsAllAt X cs g

Read and write support

The indexed clauses only mention the input through the agreement conjunct, so read-support is one line — the flat semantics' piecewise witness surgery disappears. Write-support needs the referential presupposition freeVarFinset ⊆ X only at the atomic clauses.

theorem DRT.DRS.toRelAt_congr_left {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] (X : Finset V) (K : DRS L V) {f f' g : V → M} (h : Set.EqOn f f' ↑X) : toRelAt X K f g ↔ toRelAt X K f' g

toRelAt X K reads its input only at X.

theorem DRT.Condition.holdsAt_congr {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] {X : Finset V} (c : Condition L V) (hfv : c.freeVarFinset ⊆ X) {g g' : V → M} (hgg' : Set.EqOn g g' ↑X) : holdsAt X c g ↔ holdsAt X c g'

A condition with free referents in X depends on the assignment only at X.

theorem DRT.Condition.holdsAllAt_congr {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] {X : Finset V} (cs : List (Condition L V)) (hfv : freeVarFinsetL cs ⊆ X) {g g' : V → M} (hgg' : Set.EqOn g g' ↑X) : holdsAllAt X cs g ↔ holdsAllAt X cs g'

The list analogue of Condition.holdsAt_congr.

theorem DRT.DRS.toRelAt_congr_right {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] {X : Finset V} (K : DRS L V) (hfv : K.freeVarFinset ⊆ X) {f g g' : V → M} (hgg' : Set.EqOn g g' ↑(X ∪ K.referents)) : toRelAt X K f g ↔ toRelAt X K f g'

toRelAt X K writes its output only at X ∪ U, given the referential presupposition K.freeVarFinset ⊆ X.

A DRS as a spine transition

theorem DRT.DRS.readsAt_toRelAt {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] {W : Type u_1} (X : Finset V) (K : DRS L V) : DynamicSemantics.Transition.ReadsAt ↑X fun (x : W) => toRelAt X K

A well-formed DRS denotes a transition from its context base to the base grown by its universe — K.freeVarFinset ⊆ X is the referential presupposition (Def. 27(i)).

theorem DRT.DRS.writesAt_toRelAt {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] {W : Type u_1} {X : Finset V} (K : DRS L V) (hK : K.freeVarFinset ⊆ X) : DynamicSemantics.Transition.WritesAt ↑(X ∪ K.referents) fun (x : W) => toRelAt X K

def DRT.DRS.transition {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] (W : Type u_1) (K : DRS L V) (X : Finset V) (_hK : K.freeVarFinset ⊆ X) : DynamicSemantics.Transition W M ↑X ↑(X ∪ K.referents)

A well-formed DRS as a transition, via the total–typed bridge: read at X, write at X ∪ U. The referential presupposition documents Def. 24's domain condition; the congruence lemmas above are the bridge's support hypotheses.

Equations

• DRT.DRS.transition W K X _hK = DynamicSemantics.Transition.ofTotal ⋯ fun (x : W) => DRT.DRS.toRelAt X K

theorem DRT.DRS.transition_empty {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] [Nonempty M] (W : Type u_1) (X : Finset V) (h : empty.freeVarFinset ⊆ X) (he : X ∪ empty.referents = X) : (transition W empty X h).copy ⋯ ⋯ = DynamicSemantics.Transition.id ↑X

The empty DRS denotes the identity transition, repackaged to its source: interpretation sends DRT's unit to the semantic unit. Nonempty entities are needed — under extension-typing an empty domain separates the empty box from the identity.

theorem DRT.DRS.transition_isExtension {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] (W : Type u_1) (K : DRS L V) (X : Finset V) (hK : K.freeVarFinset ⊆ X) : (transition W K X hK).IsExtension

Established referents persist along a DRS transition.

theorem DRT.DRS.transition_copy {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] (W : Type u_1) {X X' : Finset V} (K : DRS L V) (hX : X = X') (hK : K.freeVarFinset ⊆ X) (hK' : K.freeVarFinset ⊆ X') : (transition W K X hK).copy ⋯ ⋯ = transition W K X' hK'

Repackaging a DRS transition along an equality of context bases is the transition at the new base.

def DRT.DRS.state {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] (W : Type u_1) (K : DRS L V) (hK : K.IsProper) : DynamicSemantics.State W V M

The information state a proper DRS expresses (Def. 22): act on the initial state.

Equations

• DRT.DRS.state W K hK = (DRT.DRS.transition W K ∅ ⋯).applyState ⊥

theorem DRT.DRS.uniformAt_state {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] (W : Type u_1) (K : DRS L V) (hK : K.IsProper) : DynamicSemantics.State.UniformAt (↑K.referents) (state W K hK)

The state a DRS expresses lives in its referents' stratum.

theorem DRT.DRS.mem_state {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] {W : Type u_1} {K : DRS L V} {hK : K.IsProper} {q : DynamicSemantics.Possibility W V (Part M)} : q ∈ state W K hK ↔ q.domain = ↑(∅ ∪ K.referents) ∧ ∃ (f : V → M) (g : V → M), toRelAt ∅ K f g ∧ ∀ (v : ↑↑(∅ ∪ K.referents)), g ↑v ∈ q.assignment ↑v

The characteristic membership form: a point survives in ⟦K⟧ˢ iff it lives on the referents and its values are reached from some input.

Base invariance

A fresh extension of the base is invisible to a well-formed condition. The only fatal interference is capture — a fresh referent colliding with a sub-box universe would freeze a previously local existential — so the hypothesis is disjointness from the occurring referents. Re-declaration of base referents needs no exclusion: persistence makes it inert.

@[simp]

theorem DRT.Condition.holdsAllAt_append {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] (X : Finset V) (cs ds : List (Condition L V)) (g : V → M) : holdsAllAt X (cs ++ ds) g ↔ holdsAllAt X cs g ∧ holdsAllAt X ds g

theorem DRT.Condition.holdsAt_union_fresh {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] {X Δ : Finset V} (c : Condition L V) (hocc : Disjoint Δ c.varFinset) (hfv : c.freeVarFinset ⊆ X) (g : V → M) : holdsAt (X ∪ Δ) c g ↔ holdsAt X c g

Base invariance: a fresh base extension is invisible to a well-formed condition.

theorem DRT.Condition.holdsAllAt_union_fresh {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] {X Δ : Finset V} (cs : List (Condition L V)) (hocc : Disjoint Δ (varFinsetL cs)) (hfv : freeVarFinsetL cs ⊆ X) (g : V → M) : holdsAllAt (X ∪ Δ) cs g ↔ holdsAllAt X cs g

The list analogue of Condition.holdsAt_union_fresh.

The Merging Lemma and the action equation

theorem DRT.DRS.toRelAt_merge {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] {X : Finset V} (K₁ K₂ : DRS L V) (h₁ : K₁.freeVarFinset ⊆ X) (hfresh : Disjoint K₂.referents (Condition.varFinsetL K₁.conditions)) : toRelAt X (K₁.merge K₂) = DynamicSemantics.Update.seq (toRelAt X K₁) (toRelAt (X ∪ K₁.referents) K₂)

Indexed Merging Lemma: merge is sequencing. The side condition asks only that K₂'s universe not occur in K₁'s conditions (no capture); re-declaration of context or K₁-universe referents is allowed — persistence makes it inert. Contrast the flat lemma (DRS.toRel_merge), whose freshness hypothesis also had to forbid re-declaration.

theorem DRT.DRS.transition_merge {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] (W : Type u_1) {X : Finset V} (K₁ K₂ : DRS L V) (h₁ : K₁.freeVarFinset ⊆ X) (h₂ : K₂.freeVarFinset ⊆ X ∪ K₁.referents) (hfresh : Disjoint K₂.referents (Condition.varFinsetL K₁.conditions)) : (transition W K₁ X h₁).comp (transition W K₂ (X ∪ K₁.referents) h₂) = (transition W (K₁.merge K₂) X ⋯).copy ⋯ ⋯

Transition-level Merging Lemma: sequencing the transitions is the merge's transition, repackaged along associativity of the grown bases.

theorem DRT.DRS.state_merge {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] (W : Type u_1) (K₁ K₂ : DRS L V) (h₁ : K₁.IsProper) (h₂ : K₂.freeVarFinset ⊆ K₁.referents) (hfresh : Disjoint K₂.referents (Condition.varFinsetL K₁.conditions)) : (transition W K₂ K₁.referents h₂).applyState (state W K₁ h₁) = state W (K₁.merge K₂) ⋯

Action equation (p. 159): applying a DRS's transition to the state a proper context DRS expresses yields the state of the merge — an instance of Transition.apply_comp through the transition-level Merging Lemma.

Reconciliation with the flat semantics

On reuse-free DRSs (DRS.ReuseFreeAt, DRS/Basic.lean) the flat agree-off-universe semantics (DRS.toRel, DRS/Dynamics.lean) and the indexed persistence semantics coincide at truth level: every flat output is a indexed output, and a indexed output repairs, off the grown base, into a flat one. Reuse-freeness is needed — on a DRS that re-declares a referent the two diverge (Muskens's fn. 4; witness in Studies/Muskens1996.lean).

theorem DRT.Condition.verifies_iff_holdsAt {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] {X : Finset V} (c : Condition L V) (hrf : ReuseFreeAt X c) (hfv : c.freeVarFinset ⊆ X) (g : V → M) : Embedding.VerifiesCondition g c ↔ holdsAt X c g

On a reuse-free condition with free referents in the base, the flat set denotation and the indexed one coincide.

theorem DRT.Condition.verifiesAll_iff_holdsAllAt {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] {X : Finset V} (cs : List (Condition L V)) (hrf : ReuseFreeAllAt X cs) (hfv : freeVarFinsetL cs ⊆ X) (g : V → M) : (∀ c ∈ cs, Embedding.VerifiesCondition g c) ↔ holdsAllAt X cs g

The list analogue of Condition.verifies_iff_holdsAt.

theorem DRT.DRS.toRelAt_of_toRel {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] {X : Finset V} {K : DRS L V} (hrf : ReuseFreeAt X K) (hfv : K.freeVarFinset ⊆ X) {g g' : V → M} (h : K.toRel g g') : toRelAt X K g g'

Flat-to-indexed: on a reuse-free DRS every flat output is a indexed output.

theorem DRT.DRS.toRel_of_toRelAt {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] {X : Finset V} {K : DRS L V} (hrf : ReuseFreeAt X K) (hfv : K.freeVarFinset ⊆ X) {g g' : V → M} (h : toRelAt X K g g') : ∃ (g'' : V → M), K.toRel g g'' ∧ Set.EqOn g'' g' ↑(X ∪ K.referents)

Indexed-to-flat: on a reuse-free DRS a indexed output repairs, off the grown base, into a flat output.

theorem DRT.DRS.trueRel_iff_toRelAt {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] {X : Finset V} {K : DRS L V} (hrf : ReuseFreeAt X K) (hfv : K.freeVarFinset ⊆ X) (g : V → M) : K.trueRel g ↔ ∃ (g' : V → M), toRelAt X K g g'

Truth-level reconciliation (Muskens's fn. 4): on a reuse-free DRS the flat total-assignment semantics and the indexed persistence semantics have the same truth conditions. Reuse-freeness is needed — a re-declaring witness separates the two (Studies/Muskens1996.lean).