Verifying embeddings for DRSs

This file defines verification of DRSs by embeddings into a model, following [KR93]'s Def. 1.4.4 over a mathlib FirstOrder.Language.Structure. An embedding f : Embedding V M assigns discourse referents to individuals; f.Verifies 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 (the ⇒ clause is Def. 2.1.4; the ∨ clause is the Chapter 2 disjunction semantics). Truth (Def. 1.4.5) is the existential closure of verification over the outer universe, delivered downstream as DRS.trueRel (DRS/Dynamics.lean) and as the first-order translation's realization (DRS/Reduction.lean).

Main declarations

• Embedding.Verifies, Embedding.VerifiesCondition: f verifies the DRS K, resp. a single DRS-condition.
• Embedding.verifies_perm: verification reads the condition list as a set.
• Embedding.verifies_map: renaming along a bijection transports verification, so alphabetic variants (Def. 1.4.8) have the same semantics.

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 ([Mus96], 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 quantifies over the condition list (∀ c ∈ K.conditions, the Theory.Model idiom), avoiding mutual recursion. VerifiesCondition descends into sub-DRSs by well-founded recursion on sizeOf, so its clause characterizations (verifies_neg, …) are equation-lemma rewrites rather than Iff.rfl.

@[irreducible]

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

f.VerifiesCondition 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 and verifying each of its conditions.

Equations

• One or more equations did not get rendered due to their size.
• x✝.VerifiesCondition (DRT.Condition.rel R args) = FirstOrder.Language.Structure.RelMap R fun (i : Fin n) => x✝ (args i)
• x✝.VerifiesCondition (DRT.Condition.eq a b) = (x✝ a = x✝ b)
• x✝.VerifiesCondition (DRT.Condition.neg K) = ¬∃ (g : DRT.Embedding V M), K.Extends x✝ g ∧ ∀ c ∈ K.conditions, g.VerifiesCondition c

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

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

Equations

• f.Verifies K = ∀ c ∈ K.conditions, f.VerifiesCondition c

Structural simp API

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

theorem DRT.Embedding.verifies_rel {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] {f : Embedding V M} {n : ℕ} (R : L.Relations n) (args : Fin n → V) : f.VerifiesCondition (Condition.rel R args) ↔ FirstOrder.Language.Structure.RelMap R fun (i : Fin n) => f (args i)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem DRT.Embedding.verifies_perm {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] {f : Embedding V M} {U : Finset V} {cs ds : List (Condition L V)} (h : cs.Perm ds) : f.Verifies { referents := U, conditions := cs } ↔ f.Verifies { 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.Embedding.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 : Embedding W M) (c : Condition L V) : f.VerifiesCondition (Condition.map (⇑e) c) ↔ VerifiesCondition (f ∘ ⇑e) c

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

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

Renaming along a bijection transports verification: f verifies K.map e iff f ∘ e verifies K — alphabetic variants have the same semantics.

theorem DRT.Embedding.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 : Embedding W M) (K : DRS L V) : (∃ (g : Embedding W M), Box.Extends (DRS.map (⇑e) K) f g ∧ g.Verifies (DRS.map (⇑e) K)) ↔ ∃ (g : Embedding V M), Box.Extends K (f ∘ ⇑e) g ∧ g.Verifies K

"Some extension verifies", transported along renaming: f has a verifying K.map e-extension iff f ∘ e has a verifying K-extension.

Coincidence

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

Verification of a condition reads the embedding only at its occurring referents.

theorem DRT.Embedding.verifies_congr {L : FirstOrder.Language} {V : Type w} {M : Type x} [L.Structure M] [DecidableEq V] {K : DRS L V} {f₁ f₂ : Embedding V M} (h : Set.EqOn f₁ f₂ ↑K.varFinset) : f₁.Verifies K ↔ f₂.Verifies K

Verification reads the embedding only at the DRS's occurring referents.

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

"Some extension verifies" reads the input embedding only at the occurring referents.