Personae and grounded fields

This file defines the personae and grounded indexical fields of Burnett's social meaning games and the Eckert–Montague lift of a field to persona compatibility. A property space is a graph of incompatibility on social properties, a persona is a maximal independent set of it, and a grounded field indexes each variant to an independent set of properties. The lift sends a variant to the personae compatible with it, those with every property it indexes, or on the Montagovian-individual reading those sharing some property with it, as an entity lifts to the generalized quantifier of the properties it has. An association field over the dimensions of social evaluation grounds as the poles whose polarity is the sign of the association. A social meaning game runs the RSA pipeline on the personae, its literal listener conditioning a prior on the personae a variant meets; Burnett's 2023 book keeps these definitions, and her 2026 review takes the game as the current formalization of social meaning as reasoning.

Main definitions

• GroundedField: an indexical field whose values are independent sets of an incompatibility graph.
• GroundedField.Compatible, GroundedField.Meets: a persona has every property a variant indexes, or shares one with it.
• GroundedField.lift, GroundedField.liftMI: the personae compatible with a variant on each reading.
• Persona: a maximal independent set of the incompatibility graph, and GroundedField.personae, the personae that meet a variant.
• AssociationField.ground: the grounded field of an association field over the dimensions.

Main results

• GroundedField.lift_subset_lift, GroundedField.liftMI_subset_liftMI: the lift is antitone and the Montagovian-individual lift monotone in the indexed properties.
• GroundedField.lift_eq_singleton: a variant that indexes a whole persona lifts to it alone.
• AssociationField.Antipodal.ground_indexes: of an antipodal pair, the second grounds as the opposites of the poles the first grounds as.

References

• [Bur19]
• [Bur23]
• [Bur26]
• [Eck08]

structure SocialMeaning.GroundedField (Variant : Type u_1) {P : Type u_2} (G : SimpleGraph P) : Type (max u_1 u_2)

A grounded field indexes each variant to an independent set of the incompatibility graph on properties.

• indexes : Variant → Finset P

  The properties each variant indexes.

• isIndepSet (v : Variant) : G.IsIndepSet ↑(self.indexes v)

def SocialMeaning.GroundedField.Compatible {Variant : Type u_1} {P : Type u_2} {G : SimpleGraph P} (F : GroundedField Variant G) (v : Variant) (π : Finset P) : Prop

A persona is compatible with a variant when it has every property the variant indexes.

Equations

• F.Compatible v π = (F.indexes v ⊆ π)

def SocialMeaning.GroundedField.Meets {Variant : Type u_1} {P : Type u_2} {G : SimpleGraph P} (F : GroundedField Variant G) (v : Variant) (π : Finset P) : Prop

On the Montagovian-individual reading, a persona meets a variant when it shares a property with it.

Equations

• F.Meets v π = ¬Disjoint (F.indexes v) π

@[instance_reducible]

instance SocialMeaning.GroundedField.instDecidableCompatibleOfDecidableEq {Variant : Type u_1} {P : Type u_2} {G : SimpleGraph P} (F : GroundedField Variant G) (v : Variant) (π : Finset P) [DecidableEq P] : Decidable (F.Compatible v π)

Equations

• F.instDecidableCompatibleOfDecidableEq v π = { decide := decide (∀ a ∈ (F.indexes v).val.attach, (fun (x : P) (a : x ∈ F.indexes v) => x ∈ π) ↑a ⋯), reflects_decide := ⋯ }

@[instance_reducible]

instance SocialMeaning.GroundedField.instDecidableMeetsOfDecidableEq {Variant : Type u_1} {P : Type u_2} {G : SimpleGraph P} (F : GroundedField Variant G) (v : Variant) (π : Finset P) [DecidableEq P] : Decidable (F.Meets v π)

Equations

• F.instDecidableMeetsOfDecidableEq v π = { decide := !decide (Disjoint (F.indexes v) π), reflects_decide := ⋯ }

def SocialMeaning.GroundedField.lift {Variant : Type u_1} {P : Type u_2} {G : SimpleGraph P} (F : GroundedField Variant G) (v : Variant) [Fintype P] [DecidableEq P] [DecidableRel G.Adj] : Finset (Finset P)

The Eckert–Montague lift sends a variant to the personae compatible with it.

Equations

• F.lift v = Finset.filter (F.Compatible v) G.maximalIndepSets

def SocialMeaning.GroundedField.liftMI {Variant : Type u_1} {P : Type u_2} {G : SimpleGraph P} (F : GroundedField Variant G) (v : Variant) [Fintype P] [DecidableEq P] [DecidableRel G.Adj] : Finset (Finset P)

The Montagovian-individual lift sends a variant to the personae that meet it.

Equations

• F.liftMI v = Finset.filter (F.Meets v) G.maximalIndepSets

theorem SocialMeaning.GroundedField.lift_subset_lift {Variant : Type u_1} {P : Type u_2} {G : SimpleGraph P} (F : GroundedField Variant G) {v₁ v₂ : Variant} [Fintype P] [DecidableEq P] [DecidableRel G.Adj] (h : F.indexes v₁ ⊆ F.indexes v₂) : F.lift v₂ ⊆ F.lift v₁

The more a variant indexes, the fewer personae are compatible with it.

theorem SocialMeaning.GroundedField.liftMI_subset_liftMI {Variant : Type u_1} {P : Type u_2} {G : SimpleGraph P} (F : GroundedField Variant G) {v₁ v₂ : Variant} [Fintype P] [DecidableEq P] [DecidableRel G.Adj] (h : F.indexes v₁ ⊆ F.indexes v₂) : F.liftMI v₁ ⊆ F.liftMI v₂

The more a variant indexes, the more personae meet it.

theorem SocialMeaning.GroundedField.lift_eq_singleton {Variant : Type u_1} {P : Type u_2} {G : SimpleGraph P} (F : GroundedField Variant G) (v : Variant) [Fintype P] [DecidableEq P] [DecidableRel G.Adj] (h : F.indexes v ∈ G.maximalIndepSets) : F.lift v = {F.indexes v}

A variant that indexes a whole persona is compatible with that persona alone.

@[reducible, inline]

abbrev SocialMeaning.Persona {P : Type u_1} (G : SimpleGraph P) [Fintype P] [DecidableEq P] [DecidableRel G.Adj] : Type u_1

A persona is a maximal independent set of the incompatibility graph, a maximal consistent set of properties.

Equations

• SocialMeaning.Persona G = ↥G.maximalIndepSets

def SocialMeaning.GroundedField.personae {Variant : Type u_1} {P : Type u_2} {G : SimpleGraph P} [Fintype P] [DecidableEq P] [DecidableRel G.Adj] (F : GroundedField Variant G) (v : Variant) : Finset (Persona G)

The personae that meet a variant.

Equations

• F.personae v = {π : SocialMeaning.Persona G | F.Meets v ↑π}

@[simp]

theorem SocialMeaning.GroundedField.mem_personae {Variant : Type u_1} {P : Type u_2} {G : SimpleGraph P} [Fintype P] [DecidableEq P] [DecidableRel G.Adj] {F : GroundedField Variant G} {v : Variant} {π : Persona G} : π ∈ F.personae v ↔ F.Meets v ↑π

def SocialMeaning.AssociationField.ground {Variant : Type u_1} {R : Type u_2} [Zero R] [Preorder R] [DecidableLT R] (M : AssociationField Variant Dimension R) : GroundedField Variant (dimensionalIncompatibility Pole.dimension)

An association field over the dimensions grounds as the poles whose polarity is the sign of the variant's association with their dimension.

Equations

• M.ground = { indexes := fun (v : Variant) => {p : SocialMeaning.Pole | SignType.sign (M v p.dimension) = p.polarity}, isIndepSet := ⋯ }

@[simp]

theorem SocialMeaning.AssociationField.mem_ground_indexes {Variant : Type u_1} {R : Type u_2} [Zero R] [Preorder R] [DecidableLT R] {M : AssociationField Variant Dimension R} {v : Variant} {p : Pole} : p ∈ M.ground.indexes v ↔ SignType.sign (M v p.dimension) = p.polarity

theorem SocialMeaning.AssociationField.ground_indexes_mem_maximalIndepSets_iff {Variant : Type u_1} {R : Type u_2} {v : Variant} [Zero R] [LinearOrder R] {M : AssociationField Variant Dimension R} : M.ground.indexes v ∈ (dimensionalIncompatibility Pole.dimension).maximalIndepSets ↔ ∀ (d : Dimension), M v d ≠ 0

A variant grounds as a persona exactly when it indexes every dimension one way or the other.

theorem SocialMeaning.AssociationField.Antipodal.ground_indexes {Variant : Type u_1} {v₁ v₂ : Variant} {M : AssociationField Variant Dimension SignType} (h : M.Antipodal v₁ v₂) : M.ground.indexes v₂ = Finset.map (Equiv.toEmbedding Pole.oppositeEquiv) (M.ground.indexes v₁)

Of an antipodal pair of sign fields, the second grounds as the opposites of the poles the first grounds as.