Verifying embeddings for DRSs

This file defines verification of DRSs by embeddings into a FirstOrder.Language.Structure, following Kamp and Reyle's Def. 1.4.4. An embedding f : V → M assigns discourse referents to individuals; Verifies f K says f verifies every condition of K, and a sub-DRS is entered by existentially (re)assigning along its extension relation Box.Extends. For imp, the consequent witness extends the antecedent embedding, so antecedent referents stay visible in the consequent (Def. 2.1.4); the ∨ clause is Def. 2.4.2(ii)(h). Verification reads an embedding only at the free referents, so whether some extension of an input verifies a proper DRS does not depend on the input: it is truth in the model (Def. 1.4.5).

Main definitions

• DRT.VerifiesCondition, DRT.Verifies: f verifies a DRS-condition, resp. the DRS K.

Main statements

• DRT.verifies_map: alphabetic variants (Def. 1.4.8) have the same semantics.
• DRT.verifiesCondition_congr, DRT.exists_extends_verifies_congr: verification reads an embedding only at the free referents.
• DRT.exists_extends_verifies_iff_of_isProper: a proper DRS is verified by some extension of any input iff some embedding verifies it.

Implementation notes

• Embeddings here are total, and a re-declared referent is freely reassigned; the book's are partial functions that sub-DRSs strictly extend, so a re-declared referent keeps its value (Muskens, fn. 4). The two agree on DRSs that declare each referent once — the construction algorithm never re-declares — but diverge on re-declaration: [ | [x | man x] ⇒ [x | mortal x]] says "every man is mortal" there, "if there is a man there is a mortal" here.
• Verifies, VerifiesCondition and VerifiesAll are defined by structural recursion through the nested conditions, so the clause characterizations (verifies_neg, …) hold by Iff.rfl; verifies_iff recovers the ∀ c ∈ K.conditions form.

References

• [KR93]
• [Mus96]

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

Verifies f K says the embedding f verifies the DRS K, that is, every condition of K (Def. 1.4.4).

Equations

• DRT.Verifies x✝ { referents := referents, conditions := cs } = DRT.VerifiesAll x✝ cs

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

VerifiesCondition f c says the embedding f verifies the DRS-condition c (Def. 1.4.4(ii)); a sub-DRS is entered by existentially (re)assigning along its extension relation.

Equations

• DRT.VerifiesCondition x✝ (DRT.Condition.atom a) = a.Realize x✝
• DRT.VerifiesCondition x✝ (DRT.Condition.eq a b) = (x✝ a = x✝ b)
• DRT.VerifiesCondition x✝ (DRT.Condition.neg K) = ¬∃ (g : V → M), K.Extends x✝ g ∧ DRT.Verifies g K
• DRT.VerifiesCondition x✝ (DRT.Condition.imp a c) = ∀ (g : V → M), a.Extends x✝ g → DRT.Verifies g a → ∃ (h : V → M), c.Extends g h ∧ DRT.Verifies h c
• DRT.VerifiesCondition x✝ (DRT.Condition.dis l r) = ((∃ (g : V → M), l.Extends x✝ g ∧ DRT.Verifies g l) ∨ ∃ (g : V → M), r.Extends x✝ g ∧ DRT.Verifies g r)

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

VerifiesAll f cs says f verifies every condition of cs.

Equations

• DRT.VerifiesAll x✝ [] = True
• DRT.VerifiesAll x✝ (c :: cs) = (DRT.VerifiesCondition x✝ c ∧ DRT.VerifiesAll x✝ cs)

Structural simp API

theorem DRT.verifiesAll_iff {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] {f : V → M} {cs : List (Condition L V)} : VerifiesAll f cs ↔ ∀ c ∈ cs, VerifiesCondition f c

@[simp]

theorem DRT.verifies_mk {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] {f : V → M} (U : Finset V) (conds : List (Condition L V)) : Verifies f { referents := U, conditions := conds } ↔ ∀ c ∈ conds, VerifiesCondition f c

theorem DRT.verifies_iff {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] {f : V → M} {K : DRS L V} : Verifies f K ↔ ∀ c ∈ K.conditions, VerifiesCondition f c

@[simp]

theorem DRT.verifies_empty {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] {f : V → M} : Verifies f DRS.empty

@[simp]

theorem DRT.verifies_merge {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] {f : V → M} [DecidableEq V] (K₁ K₂ : DRS L V) : Verifies f (K₁.merge K₂) ↔ Verifies f K₁ ∧ Verifies f K₂

@[simp]

theorem DRT.verifies_atom {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] {f : V → M} (a : L.Atom V) : VerifiesCondition f (Condition.atom a) ↔ a.Realize f

@[simp]

theorem DRT.verifies_eq {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] {f : V → M} (a b : V) : VerifiesCondition f (Condition.eq a b) ↔ f a = f b

@[simp]

theorem DRT.verifies_neg {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] {f : V → M} (K : DRS L V) : VerifiesCondition f (Condition.neg K) ↔ ¬∃ (g : V → M), Box.Extends K f g ∧ Verifies g K

@[simp]

theorem DRT.verifies_imp {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] {f : V → M} (a c : DRS L V) : VerifiesCondition f (Condition.imp a c) ↔ ∀ (g : V → M), Box.Extends a f g → Verifies g a → ∃ (h : V → M), Box.Extends c g h ∧ Verifies h c

@[simp]

theorem DRT.verifies_dis {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] {f : V → M} (l r : DRS L V) : VerifiesCondition f (Condition.dis l r) ↔ (∃ (g : V → M), Box.Extends l f g ∧ Verifies g l) ∨ ∃ (g : V → M), Box.Extends r f g ∧ Verifies g r

theorem DRT.verifies_perm {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] {f : V → M} {U : Finset V} {cs ds : List (Condition L V)} (h : cs.Perm ds) : Verifies f { referents := U, conditions := cs } ↔ Verifies f { referents := U, conditions := ds }

Verification is invariant under permutation of the conditions — the set semantics the List-valued conditions field promises (DRS/Defs.lean).

Alphabetic variants

theorem DRT.verifies_map_condition {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] {W : Type u_1} [DecidableEq W] (e : V ≃ W) (f : W → M) (c : Condition L V) : VerifiesCondition f (Condition.map (⇑e) c) ↔ VerifiesCondition (f ∘ ⇑e) c

Renaming along a bijection transports verification (the condition form of verifies_map).

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

f verifies K.map e iff f ∘ e verifies K, so alphabetic variants have the same semantics.

theorem DRT.exists_extends_verifies_map {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] {W : Type u_1} [DecidableEq W] (e : V ≃ W) (f : W → M) (K : DRS L V) : (∃ (g : W → M), Box.Extends (DRS.map (⇑e) K) f g ∧ Verifies g (DRS.map (⇑e) K)) ↔ ∃ (g : V → M), Box.Extends K (f ∘ ⇑e) g ∧ Verifies g K

f has a verifying K.map e-extension iff f ∘ e has a verifying K-extension.

Coincidence

theorem DRT.verifiesCondition_congr {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] (c : Condition L V) {f₁ f₂ : V → M} (h : Set.EqOn f₁ f₂ ↑c.freeVarFinset) : VerifiesCondition f₁ c ↔ VerifiesCondition f₂ c

Verification of a condition reads the embedding only at its free referents (Def. 1.4.2).

theorem DRT.exists_extends_verifies_congr {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] {K : DRS L V} {f₁ f₂ : V → M} (h : Set.EqOn f₁ f₂ ↑K.freeVarFinset) : (∃ (g : V → M), Box.Extends K f₁ g ∧ Verifies g K) ↔ ∃ (g : V → M), Box.Extends K f₂ g ∧ Verifies g K

"Some extension verifies K" reads the input embedding only at K's free referents.

theorem DRT.exists_extends_verifies_iff_of_isProper {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] {K : DRS L V} (hK : K.IsProper) (f : V → M) : (∃ (g : V → M), Box.Extends K f g ∧ Verifies g K) ↔ ∃ (g : V → M), Verifies g K

A proper DRS is verified by some extension of any input iff some embedding verifies it, which is its truth in the model (Def. 1.4.5).