Chatzikyriakidis, Cooper, Gregoromichelaki and Sutton (2025): Types and the Structure of Meaning

Ranta models an agent's beliefs as a context, a sequence of hypotheses about variables, and Cooper recasts the context as a record type whose labels play the role of the variables. An agent believes a type when its belief type is a subtype of some relabelling of it, so the labels of a complement make no difference to the truth of a belief report. They make a difference to anaphora. In Geach's Hob thinks a witch has blighted Bob's mare, and Nob wonders whether she (the same witch) killed Cob's sow, the two belief contexts overlap in the label of the witch, so that Nob's question is about Hob's witch although no witch need exist. Ranta separates the actual beliefs, the hypotheses in an agent's context, from those that follow from it; on record types, what an agent believes in every modal system is exactly its actual beliefs up to relabelling. The datum is Data/Examples/ChatzikyriakidisEtAl2025.json.

Main statements

• forall_subtypeRelabel_recTypes_iff: a belief type believes a type in every modal system exactly when it contains the fields of some relabelling of it.
• Kim.believes: a belief type with the fields of (32) believes (34) under every labelling of (34), in every modal system.
• HobNob.believes_witch, HobNob.extension_witch_actual: Hob believes that there is a witch, and there is none.
• HobNob.atom_image_sameGlue, HobNob.same_witch: gluing Hob's belief context and that of Nob's question along a cover that identifies their witches gives the merge of their record types, whose witnesses are the compatible pairs of local witnesses, so it is not true when different witches did the deeds; along a cover that keeps the witches apart it is (HobNob.other_witch).

Implementation notes

• A field ℓ : P(ℓ₁, …, ℓₙ) is the atom P(ℓ, ℓ₁, …, ℓₙ), its witness first, and a record type is a set of such atoms. A possibility is a structure for the predicates, every record type occurs in every possibility, and labels are flat, so a path such as idᵢ.x is one label.
• A relabelling is a permutation of the labels, extending a one-one relabelling of a record type's finitely many labels, so the relabellings of a record type are its orbit.
• The free model behind the actual-belief theorems is the structure a record type presents on its labels.
• The alignment of §2.3.2, and the alignment of discourse referents the Element compares it with in §2.3.3, is gluing of basic DRSs along a cover of contexts in the sense of Abramsky and Sadrzadeh.

TODO

• Manifest fields (31), and the point of view by which a Roman reports Alexander's belief about Zeus with the name Jupiter.
• Nested record types, whose relabellings preserve the prefix order of paths, so that a belief in some boy who runs, (21), stays apart from a belief in the type of boys who run, (23).
• Section 3 of the Element, on polysemy, copredication and counting.

References

• [CCGS25]
• [Ran94]
• [Coo23]
• [Gea67]
• [AS14]

Record types over a modal system

def ChatzikyriakidisEtAl2025.recTypes {L : FirstOrder.Language} {M α E : Type} (S : M → L.Structure E) : Cooper2023.ModalSystem M (Set (L.Atom α)) (α → E)

The modal system of record types over a family of structures, one for each possibility. A record type occurs in every possibility, and a record witnesses it there when it realizes each of its fields.

Equations

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

theorem ChatzikyriakidisEtAl2025.mem_extension_recTypes {L : FirstOrder.Language} {M α E : Type} {S : M → L.Structure E} {T : Set (L.Atom α)} {p : M} {r : α → E} : r ∈ (recTypes S).extension T p ↔ ∀ a ∈ T, a.Realize r

theorem ChatzikyriakidisEtAl2025.extension_recTypes_union {L : FirstOrder.Language} {M α E : Type} {S : M → L.Structure E} {T₁ T₂ : Set (L.Atom α)} {p : M} : (recTypes S).extension (T₁ ∪ T₂) p = (recTypes S).extension T₁ p ∩ (recTypes S).extension T₂ p

Merging record types intersects their witnesses.

theorem ChatzikyriakidisEtAl2025.mem_extension_recTypes_smul {L : FirstOrder.Language} {M α E : Type} {S : M → L.Structure E} {T : Set (L.Atom α)} {p : M} {r : α → E} (σ : Equiv.Perm α) : r ∈ (recTypes S).extension (σ • T) p ↔ r ∘ ⇑σ ∈ (recTypes S).extension T p

theorem ChatzikyriakidisEtAl2025.subtypeR_recTypes_of_subset {L : FirstOrder.Language} {M α E : Type} {S : M → L.Structure E} {T₁ T₂ : Set (L.Atom α)} (h : T₂ ⊆ T₁) : (recTypes S).SubtypeR T₁ T₂

A record type with more fields is a subtype, since its witnesses realize the fields of the other.

theorem ChatzikyriakidisEtAl2025.subtypeRelabel_of_smul_subset {L : FirstOrder.Language} {M α E : Type} {S : M → L.Structure E} {T B : Set (L.Atom α)} (σ : Equiv.Perm α) (h : σ • T ⊆ B) : (recTypes S).SubtypeRelabel (MulAction.orbitRel (Equiv.Perm α) (Set (L.Atom α))) B T

A belief type that contains the fields of a relabelling of a type believes it.

theorem ChatzikyriakidisEtAl2025.subtypeRelabel_smul {L : FirstOrder.Language} {M α E : Type} {S : M → L.Structure E} {T B : Set (L.Atom α)} (σ : Equiv.Perm α) : (recTypes S).SubtypeRelabel (MulAction.orbitRel (Equiv.Perm α) (Set (L.Atom α))) B (σ • T) ↔ (recTypes S).SubtypeRelabel (MulAction.orbitRel (Equiv.Perm α) (Set (L.Atom α))) B T

Belief is blind to the labels of the believed type.

Actual beliefs (§2.3.1)

A record type presents a structure on its labels, in which a map of labels is a witness of another record type exactly when it carries its fields into those of the first. So the beliefs that hold in every modal system are the ones the belief type contains, up to relabelling.

theorem ChatzikyriakidisEtAl2025.forall_subtypeR_recTypes_iff {L : FirstOrder.Language} [L.IsRelational] {α : Type} {T₁ T₂ : Set (L.Atom α)} : (∀ (M E : Type) (S : M → L.Structure E), (recTypes S).SubtypeR T₁ T₂) ↔ T₂ ⊆ T₁

A record type is a subtype of another in every modal system exactly when it has all of its fields.

theorem ChatzikyriakidisEtAl2025.forall_subtypeRelabel_recTypes_iff {L : FirstOrder.Language} [L.IsRelational] {α : Type} {T B : Set (L.Atom α)} : (∀ (M E : Type) (S : M → L.Structure E), (recTypes S).SubtypeRelabel (MulAction.orbitRel (Equiv.Perm α) (Set (L.Atom α))) B T) ↔ ∃ (σ : Equiv.Perm α), σ • T ⊆ B

A belief type believes a type in every modal system exactly when it contains the fields of some relabelling of it, as an actual belief.

Kim believes that some woman is a conductor, (32)–(35)

inductive ChatzikyriakidisEtAl2025.Kim.Rel : ℕ → Type

The predicates of (32)–(35), each taking its witness as first argument.

• ind : Rel 1
• woman : Rel 2
• conductor : Rel 2

@[reducible, inline]

abbrev ChatzikyriakidisEtAl2025.Kim.lang : FirstOrder.Language

The language of the predicates of (32)–(35).

Equations

• ChatzikyriakidisEtAl2025.Kim.lang = { Functions := fun (x : ℕ) => Empty, Relations := ChatzikyriakidisEtAl2025.Kim.Rel }

instance ChatzikyriakidisEtAl2025.Kim.instIsRelationalLang : lang.IsRelational

inductive ChatzikyriakidisEtAl2025.Kim.Label : Type

The labels of (32) and (34). The path idᵢ.x of (32) is the label «idᵢ.x».

• x : Label
• c : Label
• e : Label
• «idᵢ.x» : Label
• «idᵢ.e» : Label
• «idⱼ.e» : Label

@[instance_reducible]

instance ChatzikyriakidisEtAl2025.Kim.instDecidableEqLabel : DecidableEq Label

Equations

• ChatzikyriakidisEtAl2025.Kim.instDecidableEqLabel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def ChatzikyriakidisEtAl2025.Kim.belief : Set (lang.Atom Label)

The fields of Kim's belief type (32).

Equations

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

def ChatzikyriakidisEtAl2025.Kim.complement : Set (lang.Atom Label)

The complement (34) of the report.

Equations

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

def ChatzikyriakidisEtAl2025.Kim.relabelling : Equiv.Perm Label

The relabelling (35a).

Equations

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

theorem ChatzikyriakidisEtAl2025.Kim.relabelling_smul_complement : relabelling • complement = belief

Relabelling (34) by (35a) gives the fields of (32), the type (35b).

theorem ChatzikyriakidisEtAl2025.Kim.believes {M E : Type} (S : M → lang.Structure E) {B : Set (lang.Atom Label)} (hB : belief ⊆ B) (τ : Equiv.Perm Label) : (recTypes S).SubtypeRelabel (MulAction.orbitRel (Equiv.Perm Label) (Set (lang.Atom Label))) B (τ • complement)

Whatever its labelling, (34) is believed by any belief type with the fields of (32), in every modal system.

Intentional identity

Hob believes that a witch blighted Bob's mare, and Nob, who believes only that there is a witch, wonders whether she killed Cob's sow. In the actual possibility there are no witches; in the other, one witch blighted the mare and another killed the sow.

inductive ChatzikyriakidisEtAl2025.HobNob.Rel : ℕ → Type

The predicates of the Hob–Nob sentence, each taking its witness as first argument.

• ind : Rel 1
• witch : Rel 2
• blightedBobsMare : Rel 2
• killedCobsSow : Rel 2

def ChatzikyriakidisEtAl2025.HobNob.instDecidableEqRel.decEq {a✝ : ℕ} (x✝ x✝¹ : Rel a✝) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance ChatzikyriakidisEtAl2025.HobNob.instDecidableEqRel {a✝ : ℕ} : DecidableEq (Rel a✝)

Equations

• ChatzikyriakidisEtAl2025.HobNob.instDecidableEqRel = ChatzikyriakidisEtAl2025.HobNob.instDecidableEqRel.decEq

@[reducible, inline]

abbrev ChatzikyriakidisEtAl2025.HobNob.lang : FirstOrder.Language

The language of the predicates of the Hob–Nob sentence.

Equations

• ChatzikyriakidisEtAl2025.HobNob.lang = { Functions := fun (x : ℕ) => Empty, Relations := ChatzikyriakidisEtAl2025.HobNob.Rel }

inductive ChatzikyriakidisEtAl2025.HobNob.Label : Type

The witch x, her being one c, the blighting b and the killing k, and another label y.

• x : Label
• y : Label
• c : Label
• b : Label
• k : Label

@[instance_reducible]

instance ChatzikyriakidisEtAl2025.HobNob.instDecidableEqLabel : DecidableEq Label

Equations

• ChatzikyriakidisEtAl2025.HobNob.instDecidableEqLabel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def ChatzikyriakidisEtAl2025.HobNob.witch : Set (lang.Atom Label)

The context Hob and Nob share, that there is a witch.

Equations

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

def ChatzikyriakidisEtAl2025.HobNob.hob : Set (lang.Atom Label)

Hob's belief that a witch blighted Bob's mare.

Equations

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

def ChatzikyriakidisEtAl2025.HobNob.nob : Set (lang.Atom Label)

The content of Nob's question, that she killed Cob's sow, with she the witch of the shared context.

Equations

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

inductive ChatzikyriakidisEtAl2025.HobNob.Possib : Type

• actual : Possib
• twoWitches : Possib

@[instance_reducible]

instance ChatzikyriakidisEtAl2025.HobNob.instDecidableEqPossib : DecidableEq Possib

Equations

• ChatzikyriakidisEtAl2025.HobNob.instDecidableEqPossib x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive ChatzikyriakidisEtAl2025.HobNob.Obj : Type

Two women and a situation.

• w₁ : Obj
• w₂ : Obj
• s : Obj

@[instance_reducible]

instance ChatzikyriakidisEtAl2025.HobNob.instDecidableEqObj : DecidableEq Obj

Equations

• ChatzikyriakidisEtAl2025.HobNob.instDecidableEqObj x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def ChatzikyriakidisEtAl2025.HobNob.holds (p : Possib) {n : ℕ} : Rel n → (Fin n → Obj) → Prop

The ptypes that hold in each possibility. Both women are individuals in both, and in twoWitches both are witches, w₁ blighted Bob's mare and w₂ killed Cob's sow, in the situation s.

Equations

• One or more equations did not get rendered due to their size.
• ChatzikyriakidisEtAl2025.HobNob.holds p ChatzikyriakidisEtAl2025.HobNob.Rel.ind xs = (xs 0 ≠ ChatzikyriakidisEtAl2025.HobNob.Obj.s)

@[reducible, inline]

abbrev ChatzikyriakidisEtAl2025.HobNob.system (p : Possib) : lang.Structure Obj

The possibilities as structures.

Equations

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

@[simp]

theorem ChatzikyriakidisEtAl2025.HobNob.relMap_system {p : Possib} {n : ℕ} (R : Rel n) (xs : Fin n → Obj) : FirstOrder.Language.Structure.RelMap R xs ↔ holds p R xs

theorem ChatzikyriakidisEtAl2025.HobNob.extension_witch_actual : (recTypes system).extension witch Possib.actual = ∅

No witch exists.

theorem ChatzikyriakidisEtAl2025.HobNob.believes_witch : (recTypes system).SubtypeRelabel (MulAction.orbitRel (Equiv.Perm Label) (Set (lang.Atom Label))) hob witch

Hob believes that there is a witch.

theorem ChatzikyriakidisEtAl2025.HobNob.not_believes_blighted : ¬(recTypes system).SubtypeRelabel (MulAction.orbitRel (Equiv.Perm Label) (Set (lang.Atom Label))) witch hob

Nob, whose belief type is that there is a witch, does not believe that she blighted Bob's mare.

Aligning the two contexts

Hob's belief context and the content of Nob's question each have their own referents, Nob's witch being y. Aligning them on the witch is a cover of the discourse that sends both witches to one referent, and gluing along it gives the merge of their record types; a cover that keeps the witches apart gives the merge with Nob's witch relabelled.

def ChatzikyriakidisEtAl2025.HobNob.lit {γ : DRT.Context lang Label} {n : ℕ} (r : Rel n) (args : Fin n → Label) (hr : ⟨n, r⟩ ∈ γ.vocab := by decide +kernel) (h : ∀ (i : Fin n), args i ∈ γ.vars := by decide +kernel) : DRT.Literal γ

lit A x̄ is the positive literal A(x̄) over a context.

Equations

• ChatzikyriakidisEtAl2025.HobNob.lit r args hr h = { rel := ⟨⟨n, r⟩, hr⟩, args := fun (i : Fin (↑⟨⟨n, r⟩, hr⟩).fst) => ⟨args i, ⋯⟩, pos := true }

@[simp]

theorem ChatzikyriakidisEtAl2025.HobNob.atom_lit {γ : DRT.Context lang Label} {n : ℕ} (r : Rel n) (args : Fin n → Label) (hr : ⟨n, r⟩ ∈ γ.vocab) (h : ∀ (i : Fin n), args i ∈ γ.vars) : (lit r args hr h).atom = { arity := n, rel := r, args := args }

def ChatzikyriakidisEtAl2025.HobNob.hom {γ γ' : DRT.Context lang Label} (f : Label → Label) (hf : ∀ t ∈ γ.vars, f t ∈ γ'.vars := by decide +kernel) (hL : γ.vocab ⊆ γ'.vocab := by decide +kernel) : γ ⟶ γ'

hom f is the context morphism acting as f on referents.

Equations

• ChatzikyriakidisEtAl2025.HobNob.hom f hf hL = { incl := hL, map := fun (t : ↥γ.vars) => ⟨f ↑t, ⋯⟩ }

@[reducible, inline]

abbrev ChatzikyriakidisEtAl2025.HobNob.hobCtx : DRT.Context lang Label

Hob's belief context, with the witch x.

Equations

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

@[reducible, inline]

abbrev ChatzikyriakidisEtAl2025.HobNob.nobCtx : DRT.Context lang Label

The context of Nob's question, with the witch y.

Equations

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

def ChatzikyriakidisEtAl2025.HobNob.sections (i : Fin (Nat.succ 0).succ) : DRT.Theory (![hobCtx, nobCtx] i)

Hob's belief over Hob's context, and the content of Nob's question over Nob's.

Equations

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

@[reducible, inline]

abbrev ChatzikyriakidisEtAl2025.HobNob.vocab : Finset ((n : ℕ) × lang.Relations n)

The vocabulary of the discourse.

Equations

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

@[reducible, inline]

abbrev ChatzikyriakidisEtAl2025.HobNob.sameCtx : DRT.Context lang Label

The discourse with one witch.

Equations

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

@[reducible, inline]

abbrev ChatzikyriakidisEtAl2025.HobNob.apartCtx : DRT.Context lang Label

The discourse with two witches.

Equations

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

def ChatzikyriakidisEtAl2025.HobNob.sameCover : DRT.Cover sameCtx (Fin 2)

The cover of the discourse that sends Nob's witch to Hob's.

Equations

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

def ChatzikyriakidisEtAl2025.HobNob.apartCover : DRT.Cover apartCtx (Fin 2)

The cover of the discourse that keeps the witches apart.

Equations

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

def ChatzikyriakidisEtAl2025.HobNob.sameGlue : DRT.Theory sameCtx

The gluing of the two contexts along the aligning cover.

Equations

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

def ChatzikyriakidisEtAl2025.HobNob.apartGlue : DRT.Theory apartCtx

The gluing of the two contexts along the cover that keeps the witches apart.

Equations

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

theorem ChatzikyriakidisEtAl2025.HobNob.isGluing_sameGlue : sameCover.IsGluing (DRT.presheaf lang Label) sections sameGlue

theorem ChatzikyriakidisEtAl2025.HobNob.isGluing_apartGlue : apartCover.IsGluing (DRT.presheaf lang Label) sections apartGlue

theorem ChatzikyriakidisEtAl2025.HobNob.atom_image_sameGlue : DRT.Literal.atom '' ↑sameGlue.lits = hob ∪ nob

Gluing along the aligning cover merges Hob's belief and the content of Nob's question as record types.

theorem ChatzikyriakidisEtAl2025.HobNob.atom_image_apartGlue : DRT.Literal.atom '' ↑apartGlue.lits = hob ∪ Equiv.swap Label.x Label.y • nob

Gluing along the other cover merges them with Nob's witch relabelled.

theorem ChatzikyriakidisEtAl2025.HobNob.same_witch : (recTypes system).extension (hob ∪ nob) Possib.twoWitches = ∅

She (the same witch). Aligned on the witch, Hob's belief and the content of Nob's question are not both true where different witches blighted the mare and killed the sow, since their witnesses are the compatible pairs of local witnesses and compatibility gives both one witch.

theorem ChatzikyriakidisEtAl2025.HobNob.other_witch : ((recTypes system).extension (hob ∪ Equiv.swap Label.x Label.y • nob) Possib.twoWitches).Nonempty

Keeping the witches apart, which leaves Nob's beliefs as they are, makes Hob's belief and the content of Nob's question true together.