[AS14]: Semantic Unification, sheaf-theoretically

[AS14] present a presheaf of basic DRSs over vocabulary–variable contexts and cast anaphora resolution as sheaf gluing: local literal-theories over parts of a discourse unify into a global theory when a cover — the choice of which referents to merge — admits a section restricting onto each part. The paper's Proposition 1 asserts that gluings are unique when they exist.

The formalization confirms the framework and sharpens the proposition. Uniqueness holds for covers in which every literal of the glued context factors through a single cover map (isGluing_unique_of_factors) — as in all the paper's examples, where one map carries each semantic unit. Without that hypothesis it fails: a binary literal whose arguments are hit by different cover maps is invisible to every restriction, so two theories differing by such a mixed literal glue the same family (exists_isGluing_ne — a two-singleton cover of a two-variable context). Existence can also fail, as the paper's negative-literal example shows: merging it with John forces Man and ¬Man on one referent (noGluing_merged).

The closing section reads the substrate's information states (Semantics/Dynamic/State.lean) through the paper's contextuality frame: three pairwise-compatible anticorrelation states on a triangle of bases admit no gluing at all (no_gluing_triangle) — local consistency without a global section, in the model-theoretic fibers. Together with the substrate's exists_ne_of_restrict_eq (non-uniqueness from correlation), this locates the two sheaf-condition failures that separate model-theoretic information from the paper's syntactic theories.

Main results

• Theory.restrict_restrict: functoriality of the paper's F.
• subset_of_isGluing: the pushforward union is the least gluing.
• isGluing_unique_of_factors: Proposition 1, under the factorization hypothesis its proof uses.
• exists_isGluing_ne: uniqueness fails without it.
• noGluing_merged: the paper's consistency-violation example.
• no_gluing_triangle: contextuality in the State fibers.

Literals and theories

structure AbramskySadrzadeh2014.Signature : Type 1

A relational signature: symbols with arities.

• Rel : Type

  The relation symbols.

• ar : self.Rel → ℕ

  The arity of each symbol.

structure AbramskySadrzadeh2014.Literal (σ : Signature) : Type

A literal: a signed atomic formula, variables drawn from ℕ.

• rel : σ.Rel

  The relation symbol.

• args : Fin (σ.ar self.rel) → ℕ

  The argument variables.

• pos : Bool

  The sign.

def AbramskySadrzadeh2014.Literal.map {σ : Signature} (f : ℕ → ℕ) (l : Literal σ) : Literal σ

Substitution along a variable map.

Equations

• AbramskySadrzadeh2014.Literal.map f l = { rel := l.rel, args := f ∘ l.args, pos := l.pos }

@[simp]

theorem AbramskySadrzadeh2014.Literal.map_id {σ : Signature} (l : Literal σ) : map id l = l

theorem AbramskySadrzadeh2014.Literal.map_map {σ : Signature} (f g : ℕ → ℕ) (l : Literal σ) : map g (map f l) = map (g ∘ f) l

def AbramskySadrzadeh2014.Literal.neg {σ : Signature} (l : Literal σ) : Literal σ

The complementary literal.

Equations

• l.neg = { rel := l.rel, args := l.args, pos := !l.pos }

@[simp]

theorem AbramskySadrzadeh2014.Literal.neg_map {σ : Signature} (f : ℕ → ℕ) (l : Literal σ) : (map f l).neg = map f l.neg

def AbramskySadrzadeh2014.Literal.Over {σ : Signature} (L : Finset σ.Rel) (X : Finset ℕ) (l : Literal σ) : Prop

The literal draws its symbol from L and its variables from X.

Equations

• AbramskySadrzadeh2014.Literal.Over L X l = (l.rel ∈ L ∧ ∀ (i : Fin (σ.ar l.rel)), l.args i ∈ X)

structure AbramskySadrzadeh2014.Theory (σ : Signature) (L : Finset σ.Rel) (X : Finset ℕ) : Type

The paper's fibers F(L, X): consistent theories of literals over the context. The paper takes deductive closures of consistent finite sets; for literal-only theories closure adds nothing and finiteness is not load-bearing — the paper's own "could be finessed if necessary".

• lits : Set (Literal σ)

  The literals held true.

• over (l : Literal σ) : l ∈ self.lits → Literal.Over L X l

  Every literal is over the context.

• consistent (l : Literal σ) : l ∈ self.lits → l.neg ∉ self.lits

  No literal occurs with both signs.

theorem AbramskySadrzadeh2014.Theory.ext_iff {σ : Signature} {L : Finset σ.Rel} {X : Finset ℕ} {x y : Theory σ L X} : x = y ↔ x.lits = y.lits

theorem AbramskySadrzadeh2014.Theory.ext {σ : Signature} {L : Finset σ.Rel} {X : Finset ℕ} {x y : Theory σ L X} (lits : x.lits = y.lits) : x = y

@[implicit_reducible]

instance AbramskySadrzadeh2014.instMembershipLiteralTheory {σ : Signature} {L : Finset σ.Rel} {X : Finset ℕ} : Membership (Literal σ) (Theory σ L X)

Equations

• AbramskySadrzadeh2014.instMembershipLiteralTheory = { mem := fun (s : AbramskySadrzadeh2014.Theory σ L X) (l : AbramskySadrzadeh2014.Literal σ) => l ∈ s.lits }

def AbramskySadrzadeh2014.Theory.restrict {σ : Signature} {L' : Finset σ.Rel} {X' : Finset ℕ} (f : ℕ → ℕ) (s : Theory σ L' X') (L : Finset σ.Rel) (X : Finset ℕ) : Theory σ L X

Restriction along a context morphism (the paper's F(ι, f)), by substitution-preimage: F(f)(s) ⊨ ±A(x̄) ⟺ s ⊨ ±A(f(x̄)).

Equations

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

@[simp]

theorem AbramskySadrzadeh2014.Theory.mem_restrict {σ : Signature} {L L' : Finset σ.Rel} {X X' : Finset ℕ} {f : ℕ → ℕ} {s : Theory σ L' X'} {l : Literal σ} : l ∈ restrict f s L X ↔ Literal.Over L X l ∧ Literal.map f l ∈ s.lits

theorem AbramskySadrzadeh2014.Theory.restrict_restrict {σ : Signature} {L L' : Finset σ.Rel} {X X' : Finset ℕ} {L'' : Finset σ.Rel} {X'' : Finset ℕ} {f g : ℕ → ℕ} (hL : L ⊆ L') (hf : ∀ x ∈ X, f x ∈ X') (s : Theory σ L'' X'') : restrict f (restrict g s L' X') L X = restrict (g ∘ f) s L X

Functoriality of restriction, along composable context morphisms.

Covers and gluing

structure AbramskySadrzadeh2014.Cover (σ : Signature) (L : Finset σ.Rel) (X : Finset ℕ) (ι : Type u_2) : Type u_2

The paper's covers: jointly surjective families of context morphisms into (L, X).

• Lpart : ι → Finset σ.Rel

  The component vocabularies.

• Xpart : ι → Finset ℕ

  The component variable contexts.

• map : ι → ℕ → ℕ

  The component variable maps.

• jointlySurj (x : ℕ) : x ∈ X → ∃ (i : ι), ∃ y ∈ self.Xpart i, self.map i y = x

  Joint surjectivity on variables.

def AbramskySadrzadeh2014.IsGluing {σ : Signature} {L : Finset σ.Rel} {X : Finset ℕ} {ι : Type u_1} (c : Cover σ L X ι) (F : (i : ι) → Theory σ (c.Lpart i) (c.Xpart i)) (s : Theory σ L X) : Prop

s glues the family F over the cover: it restricts onto every member (F(fᵢ)(s) = sᵢ).

Equations

• AbramskySadrzadeh2014.IsGluing c F s = ∀ (i : ι), AbramskySadrzadeh2014.Theory.restrict (c.map i) s (c.Lpart i) (c.Xpart i) = F i

theorem AbramskySadrzadeh2014.subset_of_isGluing {σ : Signature} {L : Finset σ.Rel} {X : Finset ℕ} {ι : Type u_1} {c : Cover σ L X ι} {F : (i : ι) → Theory σ (c.Lpart i) (c.Xpart i)} {s : Theory σ L X} (hs : IsGluing c F s) (i : ι) {l : Literal σ} (hl : l ∈ F i) : Literal.map (c.map i) l ∈ s.lits

Any gluing contains every pushed-forward literal: the union of pushforwards is the least gluing — the candidate of the paper's Proposition 1.

theorem AbramskySadrzadeh2014.isGluing_unique_of_factors {σ : Signature} {L : Finset σ.Rel} {X : Finset ℕ} {ι : Type u_1} {c : Cover σ L X ι} {F : (i : ι) → Theory σ (c.Lpart i) (c.Xpart i)} {s s' : Theory σ L X} (hFac : ∀ (m : Literal σ), Literal.Over L X m → ∃ (i : ι) (l : Literal σ), Literal.Over (c.Lpart i) (c.Xpart i) l ∧ Literal.map (c.map i) l = m) (hs : IsGluing c F s) (hs' : IsGluing c F s') : s = s'

Proposition 1, with its implicit hypothesis: gluings are unique provided every literal over the glued context factors through a single cover map — as in all the paper's examples. Membership of a factoring literal is decided by the restriction it factors through.

Uniqueness fails without factorization

theorem AbramskySadrzadeh2014.exists_isGluing_ne : ∃ (s : Theory AbramskySadrzadeh2014.sigB✝ {()} {0, 1}) (s' : Theory AbramskySadrzadeh2014.sigB✝ {()} {0, 1}), IsGluing AbramskySadrzadeh2014.twoCover✝ (fun (x : Bool) => AbramskySadrzadeh2014.emptyTheory✝ {()} {0}) s ∧ IsGluing AbramskySadrzadeh2014.twoCover✝ (fun (x : Bool) => AbramskySadrzadeh2014.emptyTheory✝ {()} {0}) s' ∧ s ≠ s'

Uniqueness fails without factorization: the empty theories on the two-singleton cover are glued both by the empty theory and by the mixed-literal theory. Proposition 1's uniqueness claim needs the factorization hypothesis.

Existence fails on inconsistency: the paper's example 3

@[implicit_reducible]

instance AbramskySadrzadeh2014.instDecidableEqR3 : DecidableEq AbramskySadrzadeh2014.R3✝

Equations

• AbramskySadrzadeh2014.instDecidableEqR3 x✝ y✝ = if h : AbramskySadrzadeh2014.R3.ctorIdx✝ x✝ = AbramskySadrzadeh2014.R3.ctorIdx✝ y✝ then isTrue ⋯ else isFalse ⋯

theorem AbramskySadrzadeh2014.noGluing_merged : ¬∃ (s : Theory AbramskySadrzadeh2014.sigU✝ {AbramskySadrzadeh2014.R3.john✝, AbramskySadrzadeh2014.R3.man✝, AbramskySadrzadeh2014.R3.donkey✝} {5}), IsGluing AbramskySadrzadeh2014.mergedCover✝ AbramskySadrzadeh2014.mergedFamily✝ s

Existence fails on inconsistency (the paper's example 3): the cover merging it with John has no gluing — it would hold both Man and ¬Man of the merged referent. "A cover which merged x and y would not have a gluing, since the consistency condition would be violated."

Contextuality in the model-theoretic fibers

theorem AbramskySadrzadeh2014.no_gluing_triangle : ¬∃ (S : DynamicSemantics.State Unit (Fin 3) Bool), DynamicSemantics.State.restrict {0, 1} S = AbramskySadrzadeh2014.anti✝ 0 1 ∧ DynamicSemantics.State.restrict {1, 2} S = AbramskySadrzadeh2014.anti✝ 1 2 ∧ DynamicSemantics.State.restrict {0, 2} S = AbramskySadrzadeh2014.anti✝ 0 2

Contextuality in the states ([AS14]'s frame, model-theoretically): the three anticorrelation constraints are pairwise consistent — each pair merges (merge_anti_nonempty) — but no state restricts onto all three: Boolean anticorrelation cannot hold on three referents at once. Local consistency without a global section.