Realizers of basic DRSs

A basic DRS over a context is true under an assignment of the context's referents when each of its literals holds, and the assignments that make it true are its realizers. Restriction along a context morphism precomposes assignments, so realizers restrict with the theories they realize, and the realizers of a theory are the verifying embeddings of its DRS. Gluing becomes a limit: an assignment realizes the least gluing of a family along a cover exactly when its restrictions realize the local theories, so the realizers of the gluing are the compatible families of local realizers.

Main definitions

• DRT.Literal.Holds, DRT.Theory.realizers: truth of a literal under an assignment, and the realizers of a theory.
• DRT.Cover.Compatible: local assignments that agree wherever the cover identifies referents.

Main statements

• DRT.Theory.verifies_toDRS_iff: the realizers of a theory are the verifying embeddings of its DRS.
• DRT.Cover.mem_realizers_iff: an assignment realizes the least gluing iff its restrictions realize the local theories.
• DRT.Cover.realizersEquiv: the realizers of the least gluing are the compatible families of local realizers.

Implementation notes

Abramsky and Sadrzadeh leave a sheaf-theoretic semantics of DRSs to future work; this file only shows that truth is compatible with their gluing.

References

• [AS14]
• [KR93]

def DRT.Literal.Holds {L : FirstOrder.Language} {V : Type w} {M : Type x} {c : Context L V} [L.Structure M] (l : Literal c) (g : ↥c.vars → M) : Prop

l.Holds g says that the assignment g makes l true, its atom holding when l is positive and failing when it is negative.

Equations

• l.Holds g = (FirstOrder.Language.Structure.RelMap (↑l.rel).snd (g ∘ l.args) ↔ l.pos = true)

@[simp]

theorem DRT.Literal.holds_map {L : FirstOrder.Language} {V : Type w} {M : Type x} {c c' : Context L V} [L.Structure M] (f : c ⟶ c') (l : Literal c) (g : ↥c'.vars → M) : (map f l).Holds g ↔ l.Holds (g ∘ f.map)

theorem DRT.Literal.holds_comp_val_iff {L : FirstOrder.Language} {V : Type w} {M : Type x} {c : Context L V} [L.Structure M] (l : Literal c) (g : V → M) : l.Holds (g ∘ Subtype.val) ↔ (l.atom.Realize g ↔ l.pos = true)

def DRT.Theory.realizers {L : FirstOrder.Language} {V : Type w} (M : Type x) {c : Context L V} [L.Structure M] (s : Theory c) : Set (↥c.vars → M)

The realizers of a theory are the assignments of the context's referents that make each of its literals true.

Equations

• DRT.Theory.realizers M s = {g : ↥c.vars → M | ∀ l ∈ s.lits, l.Holds g}

theorem DRT.Theory.mem_realizers {L : FirstOrder.Language} {V : Type w} {M : Type x} {c : Context L V} [L.Structure M] {s : Theory c} {g : ↥c.vars → M} : g ∈ realizers M s ↔ ∀ l ∈ s.lits, l.Holds g

theorem DRT.Theory.verifies_toDRS_iff {L : FirstOrder.Language} {V : Type w} {M : Type x} {c : Context L V} [L.Structure M] {s : Theory c} {g : V → M} : Verifies g s.toDRS ↔ g ∘ Subtype.val ∈ realizers M s

An embedding verifies the DRS of a theory exactly when its restriction to the context's referents realizes the theory.

theorem DRT.Theory.comp_val_mem_realizers_iff {L : FirstOrder.Language} {V : Type w} {M : Type x} {c : Context L V} [L.Structure M] {s : Theory c} (hpos : ∀ l ∈ s.lits, l.pos = true) {g : V → M} : g ∘ Subtype.val ∈ realizers M s ↔ g ∈ FirstOrder.Language.Atom.realizers M (Literal.atom '' ↑s.lits)

For a theory of positive literals, an embedding realizes the theory on the context's referents exactly when it realizes the atoms of the theory.

theorem DRT.Theory.comp_mem_realizers_restrict {L : FirstOrder.Language} {V : Type w} {M : Type x} {c c' : Context L V} [L.Structure M] [DecidableEq V] [(n : ℕ) → DecidableEq (L.Relations n)] {f : c ⟶ c'} {s : Theory c'} {g : ↥c'.vars → M} (h : g ∈ realizers M s) : g ∘ f.map ∈ realizers M (restrict f s)

Restricting a theory along a context morphism keeps the restrictions of its realizers.

def DRT.Cover.Compatible {L : FirstOrder.Language} {V : Type w} {M : Type x} {c : Context L V} {ι : Type u_1} (C : Cover c ι) (g : (i : ι) → ↥(C.part i).vars → M) : Prop

Local assignments are compatible when they agree wherever the cover identifies referents.

Equations

• C.Compatible g = ∀ (i j : ι) (a : ↥(C.part i).vars) (b : ↥(C.part j).vars), (C.map i).map a = (C.map j).map b → g i a = g j b

noncomputable def DRT.Cover.glueAssignment {L : FirstOrder.Language} {V : Type w} {M : Type x} {c : Context L V} {ι : Type u_1} {C : Cover c ι} (g : (i : ι) → ↥(C.part i).vars → M) (t : ↥c.vars) : M

glueAssignment g assigns each referent the value a local assignment gives one of its preimages.

Equations

• DRT.Cover.glueAssignment g t = g ⋯.choose ⋯.choose

theorem DRT.Cover.glueAssignment_comp {L : FirstOrder.Language} {V : Type w} {M : Type x} {c : Context L V} {ι : Type u_1} {C : Cover c ι} {g : (i : ι) → ↥(C.part i).vars → M} (hg : C.Compatible g) (i : ι) : glueAssignment g ∘ (C.map i).map = g i

theorem DRT.Cover.mem_realizers_iff {L : FirstOrder.Language} {V : Type w} {M : Type x} {c : Context L V} {ι : Type u_1} {C : Cover c ι} [L.Structure M] [Fintype ι] [DecidableEq V] [(n : ℕ) → DecidableEq (L.Relations n)] {x : (i : ι) → Theory (C.part i)} {s : Theory c} (hs : s.lits = C.pushforward x) {g : ↥c.vars → M} : g ∈ Theory.realizers M s ↔ ∀ (i : ι), g ∘ (C.map i).map ∈ Theory.realizers M (x i)

An assignment realizes the least gluing of a family exactly when its restriction along every cover morphism realizes the local theory.

noncomputable def DRT.Cover.realizersEquiv {L : FirstOrder.Language} {V : Type w} {M : Type x} {c : Context L V} {ι : Type u_1} {C : Cover c ι} [L.Structure M] [Fintype ι] [DecidableEq V] [(n : ℕ) → DecidableEq (L.Relations n)] {x : (i : ι) → Theory (C.part i)} {s : Theory c} (hs : s.lits = C.pushforward x) : ↑(Theory.realizers M s) ≃ { g : (i : ι) → ↑(Theory.realizers M (x i)) // C.Compatible fun (i : ι) => ↑(g i) }

The realizers of the least gluing of a family are the compatible families of local realizers.

Equations

• One or more equations did not get rendered due to their size.