Spector (2017): The pragmatics of plural predication: Homogeneity and non-maximality within the Rational Speech Act model

Spector reconstructs Križ and Spector's pragmatics of plural predication in the Rational Speech Act model. A plural definite is ambiguous between an existential and a universal reading, and the first speaker, unsure which reading the literal listener uses, weighs a message by its expected utility across the readings (S1_apply_singleton). A message false on some reading throughout the speaker's answer has utility minus infinity there, which derives Križ and Spector's truth on all interpretations (S1_apply_singleton_eq_zero_iff). The utility is the literal listener's probability of the speaker's answer to the question under discussion together with the question. When the question is what is the case, the students came and the students didn't come are used only where all or where none of the students came (homogeneity); when it is whether some of them came, both are existential (nonMaximality), and the listener who hears the students came entertains that only some came only under that question (L1_the_justSome_ne_zero_iff).

Implementation notes

• Priors are arguments, with positive mass on every world, question and interpretation, of which the paper's flat priors and its two priors over questions are instances.
• A question maps a world to its answer, yes or no for the polar questions and the world itself for what is the case; the speaker's answer is that answer together with the question.
• The literal listeners of the two interpretations are one measure on pairs of an interpretation and an answer, and the speaker's belief is the interpretation prior times a point mass at her answer, so RSA.speaker takes the expected utility across interpretations.

TODO

• The higher levels of the recursion and the interpretations of the level-five listener reported in the tables of §3.3 to §3.5.

References

• [Spe17]
• [KS21b]
• [GS13]

inductive Spector2017.World : Type

No student came, some but not all did, or all did.

• none : World
• justSome : World
• all : World

@[instance_reducible]

instance Spector2017.instDecidableEqWorld : DecidableEq World

Equations

• Spector2017.instDecidableEqWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Spector2017.instReprWorld : Repr World

Equations

• Spector2017.instReprWorld = { reprPrec := Spector2017.instReprWorld.repr }

def Spector2017.instReprWorld.repr : World → ℕ → Std.Format

Equations

• Spector2017.instReprWorld.repr Spector2017.World.none prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Spector2017.World.none")).group prec✝
• Spector2017.instReprWorld.repr Spector2017.World.justSome prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Spector2017.World.justSome")).group prec✝
• Spector2017.instReprWorld.repr Spector2017.World.all prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Spector2017.World.all")).group prec✝

@[instance_reducible]

instance Spector2017.instFintypeWorld : Fintype World

Equations

• Spector2017.instFintypeWorld = { elems := { val := ↑Spector2017.World.enumList, nodup := Spector2017.World.enumList_nodup }, complete := Spector2017.instFintypeWorld._proof_1 }

@[instance_reducible]

instance Spector2017.instMeasurableSpaceWorld : MeasurableSpace World

Equations

• Spector2017.instMeasurableSpaceWorld = ⊤

instance Spector2017.instDiscreteMeasurableSpaceWorld : DiscreteMeasurableSpace World

inductive Spector2017.Message : Type

The messages of the model.

• no : Message
• some : Message
• all : Message
• notAll : Message
• the : Message
• notThe : Message

@[instance_reducible]

instance Spector2017.instDecidableEqMessage : DecidableEq Message

Equations

• Spector2017.instDecidableEqMessage x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Spector2017.instReprMessage : Repr Message

Equations

• Spector2017.instReprMessage = { reprPrec := Spector2017.instReprMessage.repr }

def Spector2017.instReprMessage.repr : Message → ℕ → Std.Format

Equations

• Spector2017.instReprMessage.repr Spector2017.Message.no prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Spector2017.Message.no")).group prec✝
• Spector2017.instReprMessage.repr Spector2017.Message.some prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Spector2017.Message.some")).group prec✝
• Spector2017.instReprMessage.repr Spector2017.Message.all prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Spector2017.Message.all")).group prec✝
• Spector2017.instReprMessage.repr Spector2017.Message.notAll prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Spector2017.Message.notAll")).group prec✝
• Spector2017.instReprMessage.repr Spector2017.Message.the prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Spector2017.Message.the")).group prec✝
• Spector2017.instReprMessage.repr Spector2017.Message.notThe prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Spector2017.Message.notThe")).group prec✝

@[instance_reducible]

instance Spector2017.instFintypeMessage : Fintype Message

Equations

• Spector2017.instFintypeMessage = { elems := { val := ↑Spector2017.Message.enumList, nodup := Spector2017.Message.enumList_nodup }, complete := Spector2017.instFintypeMessage._proof_1 }

@[instance_reducible]

instance Spector2017.instMeasurableSpaceMessage : MeasurableSpace Message

Equations

• Spector2017.instMeasurableSpaceMessage = ⊤

instance Spector2017.instDiscreteMeasurableSpaceMessage : DiscreteMeasurableSpace Message

inductive Spector2017.Interp : Type

The plural definite is read existentially or universally.

• exist : Interp
• univ : Interp

@[instance_reducible]

instance Spector2017.instDecidableEqInterp : DecidableEq Interp

Equations

• Spector2017.instDecidableEqInterp x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Spector2017.instReprInterp.repr : Interp → ℕ → Std.Format

Equations

• Spector2017.instReprInterp.repr Spector2017.Interp.exist prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Spector2017.Interp.exist")).group prec✝
• Spector2017.instReprInterp.repr Spector2017.Interp.univ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Spector2017.Interp.univ")).group prec✝

@[instance_reducible]

instance Spector2017.instReprInterp : Repr Interp

Equations

• Spector2017.instReprInterp = { reprPrec := Spector2017.instReprInterp.repr }

@[instance_reducible]

instance Spector2017.instFintypeInterp : Fintype Interp

Equations

• Spector2017.instFintypeInterp = { elems := { val := ↑Spector2017.Interp.enumList, nodup := Spector2017.Interp.enumList_nodup }, complete := Spector2017.instFintypeInterp._proof_1 }

@[instance_reducible]

instance Spector2017.instMeasurableSpaceInterp : MeasurableSpace Interp

Equations

• Spector2017.instMeasurableSpaceInterp = ⊤

instance Spector2017.instDiscreteMeasurableSpaceInterp : DiscreteMeasurableSpace Interp

inductive Spector2017.QUD : Type

Did some of the students come, did all of them, and what is the case.

• isSome : QUD
• isAll : QUD
• whatsTheCase : QUD

@[instance_reducible]

instance Spector2017.instDecidableEqQUD : DecidableEq QUD

Equations

• Spector2017.instDecidableEqQUD x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Spector2017.instReprQUD.repr : QUD → ℕ → Std.Format

Equations

• Spector2017.instReprQUD.repr Spector2017.QUD.isSome prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Spector2017.QUD.isSome")).group prec✝
• Spector2017.instReprQUD.repr Spector2017.QUD.isAll prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Spector2017.QUD.isAll")).group prec✝
• Spector2017.instReprQUD.repr Spector2017.QUD.whatsTheCase prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Spector2017.QUD.whatsTheCase")).group prec✝

@[instance_reducible]

instance Spector2017.instReprQUD : Repr QUD

Equations

• Spector2017.instReprQUD = { reprPrec := Spector2017.instReprQUD.repr }

@[instance_reducible]

instance Spector2017.instFintypeQUD : Fintype QUD

Equations

• Spector2017.instFintypeQUD = { elems := { val := ↑Spector2017.QUD.enumList, nodup := Spector2017.QUD.enumList_nodup }, complete := Spector2017.instFintypeQUD._proof_1 }

@[instance_reducible]

instance Spector2017.instMeasurableSpaceQUD : MeasurableSpace QUD

Equations

• Spector2017.instMeasurableSpaceQUD = ⊤

instance Spector2017.instDiscreteMeasurableSpaceQUD : DiscreteMeasurableSpace QUD

def Spector2017.QUD.answer : QUD → World → Bool ⊕ World

The answer to a question at a world: yes or no to a polar question, the world itself to what is the case.

Equations

• Spector2017.QUD.isSome.answer x✝ = Sum.inl (decide (x✝ ≠ Spector2017.World.none))
• Spector2017.QUD.isAll.answer x✝ = Sum.inl (decide (x✝ = Spector2017.World.all))
• Spector2017.QUD.whatsTheCase.answer x✝ = Sum.inr x✝

def Spector2017.meaning : Interp → Message → Set World

The meaning of a message under an interpretation of the plural definite.

Equations

• Spector2017.meaning x✝ Spector2017.Message.no = {w : Spector2017.World | w = Spector2017.World.none}
• Spector2017.meaning x✝ Spector2017.Message.some = {w : Spector2017.World | w ≠ Spector2017.World.none}
• Spector2017.meaning x✝ Spector2017.Message.all = {w : Spector2017.World | w = Spector2017.World.all}
• Spector2017.meaning x✝ Spector2017.Message.notAll = {w : Spector2017.World | w ≠ Spector2017.World.all}
• Spector2017.meaning Spector2017.Interp.exist Spector2017.Message.the = {w : Spector2017.World | w ≠ Spector2017.World.none}
• Spector2017.meaning Spector2017.Interp.univ Spector2017.Message.the = {w : Spector2017.World | w = Spector2017.World.all}
• Spector2017.meaning Spector2017.Interp.exist Spector2017.Message.notThe = {w : Spector2017.World | w = Spector2017.World.none}
• Spector2017.meaning Spector2017.Interp.univ Spector2017.Message.notThe = {w : Spector2017.World | w ≠ Spector2017.World.all}

@[instance_reducible]

instance Spector2017.instDecidablePredWorldMemSetMeaning (i : Interp) (u : Message) : DecidablePred fun (x : World) => x ∈ meaning i u

Equations

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

noncomputable def Spector2017.cost : Message → ℝ

The costs of the messages.

Equations

• Spector2017.cost Spector2017.Message.the = 0
• Spector2017.cost Spector2017.Message.notThe = 1
• Spector2017.cost Spector2017.Message.some = 1
• Spector2017.cost Spector2017.Message.all = 1
• Spector2017.cost Spector2017.Message.no = 3 / 2
• Spector2017.cost Spector2017.Message.notAll = 2

def Spector2017.answer (p : World × QUD) : (Bool ⊕ World) × QUD

The answer at a world and a question, together with the question.

Equations

• Spector2017.answer p = (p.2.answer p.1, p.2)

noncomputable def Spector2017.L0 (μ : MeasureTheory.Measure World) (ρ : MeasureTheory.Measure QUD) (i : Interp) : ProbabilityTheory.Kernel Message (World × QUD)

The literal listener of an interpretation conditions the prior over worlds and questions on the message.

Equations

• Spector2017.L0 μ ρ i = RSA.listener (μ.prod ρ) (RSA.truthful fun (u : Spector2017.Message) => Prod.fst ⁻¹' Spector2017.meaning i u)

instance Spector2017.instIsFiniteKernelMessageProdWorldQUDL0 (μ : MeasureTheory.Measure World) (ρ : MeasureTheory.Measure QUD) (i : Interp) : ProbabilityTheory.IsFiniteKernel (L0 μ ρ i)

noncomputable def Spector2017.answerL0 (μ : MeasureTheory.Measure World) (ρ : MeasureTheory.Measure QUD) (u : Message) : MeasureTheory.Measure (Interp × (Bool ⊕ World) × QUD)

The literal listeners' probabilities of the answers, one for each interpretation.

Equations

• Spector2017.answerL0 μ ρ u = MeasureTheory.Measure.sum fun (i : Spector2017.Interp) => MeasureTheory.Measure.map (Prod.mk i) (((Spector2017.L0 μ ρ i).map Spector2017.answer) u)

instance Spector2017.instIsFiniteMeasureProdInterpSumBoolWorldQUDAnswerL0 (μ : MeasureTheory.Measure World) (ρ : MeasureTheory.Measure QUD) (u : Message) : MeasureTheory.IsFiniteMeasure (answerL0 μ ρ u)

noncomputable def Spector2017.S1 (μ : MeasureTheory.Measure World) (ρ : MeasureTheory.Measure QUD) (ν : MeasureTheory.Measure Interp) (α : ℝ) : ProbabilityTheory.Kernel (World × QUD) Message

The first speaker is uncertain about the interpretation of the literal listener and weighs a message by its expected utility across interpretations.

Equations

• Spector2017.S1 μ ρ ν α = RSA.speaker α Spector2017.cost (Spector2017.answerL0 μ ρ) fun (p : Spector2017.World × Spector2017.QUD) => ν.prod (MeasureTheory.Measure.dirac (Spector2017.answer p))

instance Spector2017.instIsFiniteKernelProdWorldQUDMessageS1 (μ : MeasureTheory.Measure World) (ρ : MeasureTheory.Measure QUD) (ν : MeasureTheory.Measure Interp) (α : ℝ) : ProbabilityTheory.IsFiniteKernel (S1 μ ρ ν α)

noncomputable def Spector2017.L1 (μ : MeasureTheory.Measure World) (ρ : MeasureTheory.Measure QUD) (ν : MeasureTheory.Measure Interp) (α : ℝ) : ProbabilityTheory.Kernel Message (World × QUD)

The pragmatic listener inverts the first speaker against the prior over worlds and questions.

Equations

• Spector2017.L1 μ ρ ν α = RSA.listener (μ.prod ρ) ⇑(Spector2017.S1 μ ρ ν α)

theorem Spector2017.answerL0_apply_singleton (μ : MeasureTheory.Measure World) (ρ : MeasureTheory.Measure QUD) (u : Message) (i : Interp) (x : (Bool ⊕ World) × QUD) : (answerL0 μ ρ u) {(i, x)} = (((L0 μ ρ i).map answer) u) {x}

theorem Spector2017.S1_apply_singleton (μ : MeasureTheory.Measure World) (ρ : MeasureTheory.Measure QUD) (ν : MeasureTheory.Measure Interp) (α : ℝ) (p : World × QUD) (u : Message) : ((S1 μ ρ ν α) p) {u} = (ν.geomMean fun (i : Interp) => (((L0 μ ρ i).map answer) u) {answer p}) ^ α * ENNReal.ofReal (Real.exp (-(α * cost u))) / ∑ u' : Message, (ν.geomMean fun (i : Interp) => (((L0 μ ρ i).map answer) u') {answer p}) ^ α * ENNReal.ofReal (Real.exp (-(α * cost u')))

The first speaker weighs a message by the geometric mean over interpretations of the literal listener's probability of her answer, to the power of the rationality, times the cost weight: the exponential of the rationality times the expected utility across interpretations.

theorem Spector2017.answerL0_answer_eq_zero_iff {μ : MeasureTheory.Measure World} {ρ : MeasureTheory.Measure QUD} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ρ] (hμ : ∀ (w : World), μ {w} ≠ 0) (hρ : ∀ (Q : QUD), ρ {Q} ≠ 0) (u : Message) (i : Interp) (w : World) (Q : QUD) : (answerL0 μ ρ u) {(i, answer (w, Q))} = 0 ↔ ∀ (v : World), Q.answer v = Q.answer w → v ∉ meaning i u

Under an interpretation, the literal listener gives no probability to an answer exactly when the message is false at every world with that answer.

theorem Spector2017.S1_apply_singleton_eq_zero_iff {μ : MeasureTheory.Measure World} {ρ : MeasureTheory.Measure QUD} {ν : MeasureTheory.Measure Interp} {α : ℝ} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ρ] (hμ : ∀ (w : World), μ {w} ≠ 0) (hρ : ∀ (Q : QUD), ρ {Q} ≠ 0) [MeasureTheory.IsFiniteMeasure ν] (hα : 0 < α) (w : World) (Q : QUD) (u : Message) : ((S1 μ ρ ν α) (w, Q)) {u} = 0 ↔ ∃ (i : Interp), ν {i} ≠ 0 ∧ ∀ (v : World), Q.answer v = Q.answer w → v ∉ meaning i u

The first speaker never uses a message at a world when, under some interpretation, it is false at every world with her answer, the principle of truth on all interpretations.

theorem Spector2017.S1_apply_singleton_ne_zero_iff {μ : MeasureTheory.Measure World} {ρ : MeasureTheory.Measure QUD} {ν : MeasureTheory.Measure Interp} {α : ℝ} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ρ] (hμ : ∀ (w : World), μ {w} ≠ 0) (hρ : ∀ (Q : QUD), ρ {Q} ≠ 0) [MeasureTheory.IsFiniteMeasure ν] (hα : 0 < α) (hν : ∀ (i : Interp), ν {i} ≠ 0) (w : World) (Q : QUD) (u : Message) : ((S1 μ ρ ν α) (w, Q)) {u} ≠ 0 ↔ ∀ (i : Interp), ∃ (v : World), Q.answer v = Q.answer w ∧ v ∈ meaning i u

With every interpretation possible, the first speaker uses a message exactly when, under each interpretation, it is true at some world with her answer.

theorem Spector2017.homogeneity {μ : MeasureTheory.Measure World} {ρ : MeasureTheory.Measure QUD} {ν : MeasureTheory.Measure Interp} {α : ℝ} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ρ] (hμ : ∀ (w : World), μ {w} ≠ 0) (hρ : ∀ (Q : QUD), ρ {Q} ≠ 0) [MeasureTheory.IsFiniteMeasure ν] (hα : 0 < α) (hν : ∀ (i : Interp), ν {i} ≠ 0) (w : World) : (((S1 μ ρ ν α) (w, QUD.whatsTheCase)) {Message.the} ≠ 0 ↔ w = World.all) ∧ (((S1 μ ρ ν α) (w, QUD.whatsTheCase)) {Message.notThe} ≠ 0 ↔ w = World.none)

When the question is what is the case, the first speaker uses the only where all of the students came and not the only where none did, so neither where only some did.

theorem Spector2017.nonMaximality {μ : MeasureTheory.Measure World} {ρ : MeasureTheory.Measure QUD} {ν : MeasureTheory.Measure Interp} {α : ℝ} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ρ] (hμ : ∀ (w : World), μ {w} ≠ 0) (hρ : ∀ (Q : QUD), ρ {Q} ≠ 0) [MeasureTheory.IsFiniteMeasure ν] (hα : 0 < α) (hν : ∀ (i : Interp), ν {i} ≠ 0) (w : World) : (((S1 μ ρ ν α) (w, QUD.isSome)) {Message.the} ≠ 0 ↔ w ≠ World.none) ∧ (((S1 μ ρ ν α) (w, QUD.isSome)) {Message.notThe} ≠ 0 ↔ w = World.none)

When the question is whether some of the students came, the first speaker uses the wherever some did and not the only where none did, as existential quantifiers.

theorem Spector2017.L1_the_justSome_ne_zero_iff {μ : MeasureTheory.Measure World} {ρ : MeasureTheory.Measure QUD} {ν : MeasureTheory.Measure Interp} {α : ℝ} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ρ] (hμ : ∀ (w : World), μ {w} ≠ 0) (hρ : ∀ (Q : QUD), ρ {Q} ≠ 0) [MeasureTheory.IsFiniteMeasure ν] (hα : 0 < α) (hν : ∀ (i : Interp), ν {i} ≠ 0) (Q : QUD) : ((L1 μ ρ ν α) Message.the) {(World.justSome, Q)} ≠ 0 ↔ Q = QUD.isSome

Hearing the, the pragmatic listener takes it to be possible that only some of the students came exactly as an answer to whether some of them did.