Docs / Semantics / Dynamic / DRT / Verification / Total

Verification by total assignments

import Linglib.Semantics.Dynamic.DRT.Verification.Total · namespace DRT

This file defines the verification of a DRS by total assignments. An assignment verifies a DRS when it verifies each of its conditions, and a sub-DRS is entered by reassigning its universe, so a referent declared twice takes a fresh value the second time. Verification reads an assignment only at the free referents, and alphabetic variants agree.

Main definitions

DRT.DRS.Extends: the relation between assignments that differ at most on the universe of a DRS.
DRT.VerifiesTotal, DRT.VerifiesConditionTotal: verification of DRSs and conditions.

Implementation notes

The quantifier over assignments reduces to a quantifier over values for the universe (DRS.exists_extends_iff), which is Function.updateFinset; mathlib's DependsOn.updateFinset then gives coincidence.

References

Muskens 1996, Combining Montague semantics and discourse representation formalized

Assignments that differ on a universe

K.Extends f g says f and g differ at most in their values for the universe of K. This is Muskens's a[x₁, …, xₙ]a' (p. 148), the total rendering of the partial embeddings' "f ⊆ g and Dom g = Dom f ∪ U_K"; on total assignments it is symmetric.

def DRS.Extends L45–48

{L : FirstOrder.Language} {V : Type w} {M : Type x} (K : DRS L V) (f g : V → M) :

Prop

K.Extends f g = ∀ x ∉ K.referents, g x = f x

Used by DRS.Extends.refl, DRS.Extends.symm, DRS.extends_map, DRS.exists_extends_map, DRS.forall_extends_map, DRS.extends_iff_mem_range, DRS.exists_extends_iff, DRS.forall_extends_iff, DRS.dependsOn_exists_extends, DRS.dependsOn_forall_extends, VerifiesConditionTotal, verifiesTotal_neg, verifiesTotal_imp, verifiesTotal_dis, exists_extends_verifiesTotal_map, dependsOn_exists_extends_verifiesTotal, exists_extends_verifiesTotal_iff_of_isProper

Used in Semantics/Dynamic/DRT/Relational, Semantics/Dynamic/DRT/Translation, Semantics/Dynamic/DRT/Verification/Partial

Verification

VerifiesTotal f K says the total assignment f verifies every condition of K.

def VerifiesTotal L112–114

{L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] :

(V → M) → DRS L V → Prop

VerifiesTotal x✝ { referents := referents, conditions := cs } = VerifiesAllTotal x✝ cs

Built from

Used by VerifiesConditionTotal, verifiesTotal_mk, verifiesTotal_iff, verifiesTotal_empty, verifiesTotal_merge, verifiesTotal_neg, verifiesTotal_imp, verifiesTotal_dis, verifiesTotal_perm, verifiesTotal_map, exists_extends_verifiesTotal_map, dependsOn_verifiesTotal, dependsOn_exists_extends_verifiesTotal, exists_extends_verifiesTotal_iff_of_isProper

Used in Semantics/Dynamic/DRT/Relational, Semantics/Dynamic/DRT/Sheaf/Realizers, Semantics/Dynamic/DRT/Translation, Semantics/Dynamic/DRT/Verification/Partial

VerifiesConditionTotal f c says the total assignment f verifies the DRS-condition c; a sub-DRS is entered by existentially (re)assigning along its extension relation.

def VerifiesConditionTotal L115–124