Warstadt (2022): Presupposition Triggering Reflects Pragmatic Reasoning About Utterance Utility

Warstadt derives soft presupposition triggers from a listener's inference about the common ground the speaker assumed. The model is Qing, Goodman and Lassiter's. Within a context set the literal listener conditions the prior on the utterance and answers the question under discussion (L0), the speaker is informative about the answer at her world and says nothing false there (speaker), and the pragmatic listener inverts the speaker jointly over worlds and context sets (listener).

Main results

• needVisa_nonUS_lt: asked whether Tom needs a visa, a listener who hears Tom doesn't have a green card favours the world where Tom is a non-US citizen over the one where he is a US citizen, at every rationality.
• freeDrink_exhaustive, freeDrink_nonUS_lt: asked whether Tom gets a free drink, the utterance settles the question in every context set, and the listener still favours the non-US world.
• notSprinter_exhaustive_iff: not an Olympic sprinter settles which kind of athlete Tom is, at the world where he is another runner, exactly within context sets that exclude the athlete and the non-athlete worlds.
• other_share_lt: at the non-athlete world not an Olympic sprinter is produced more often than silence and less often than not a runner.

Implementation notes

• Utterances carry no cost.
• The paper gives a false utterance a utility of minus infinity. Here the speaker who addresses the question is conditioned on the utterances true at her world, which is the same distribution wherever some true utterance has positive weight.
• Shares are evaluated cell by cell from tables of natural-number weights (weight), certified by decide, and the listener comparisons are prior-weighted sums over the eight context sets.

TODO

• The paper reports the free-drink posteriors of its second figure as nearly equal. Under the model as written the non-US world is favoured under both questions.
• The family-genus-species listener of the paper's third figure is not formalized.

References

• [War22]
• [QGL16]
• [Abu02]
• [FG12]
• [Sta78]

The model (3)

def Warstadt2022.weight {W U Q : Type} [DecidableEq W] (P : W → ℕ) (cell : Q → W → Finset W) (sem : U → Set W) [(u : U) → DecidablePred fun (x : W) => x ∈ sem u] (C : Finset W) (q : Q) (u : U) (w : W) : ℕ × ℕ

The speaker's weight on an utterance at a world before the rationality exponent (3c), as a numerator and a denominator. Where the utterance is true it is the literal listener's probability of the world's answer, the prior weight of the context-set worlds that make the utterance true and share the answer over that of those that make it true. Where it is false it is 0 over 1.

Equations

• Warstadt2022.weight P cell sem C q u w = if w ∈ sem u then (∑ v ∈ {x ∈ C | x ∈ sem u} with cell q v = cell q w, P v, ∑ v ∈ C with v ∈ sem u, P v) else (0, 1)

noncomputable def Warstadt2022.pairPrior {W : Type} [DecidableEq W] [MeasurableSpace W] (P : W → ℕ) : MeasureTheory.Measure (W × Finset W)

In the prior over pairs of a world and a context set (3d), a world's weight within a context set is its prior share of the set, and context sets are equally likely.

Equations

• Warstadt2022.pairPrior P = MeasureTheory.Measure.count.withDensity fun (p : W × Finset W) => if p.1 ∈ p.2 then ↑(P p.1) / ∑ v ∈ p.2, ↑(P v) else 0

theorem Warstadt2022.pairPrior_singleton {W : Type} [DecidableEq W] [Fintype W] [MeasurableSpace W] [MeasurableSingletonClass W] (P : W → ℕ) (w : W) (C : Finset W) : (pairPrior P) {(w, C)} = if w ∈ C then ↑(P w) / ∑ v ∈ C, ↑(P v) else 0

theorem Warstadt2022.pairPrior_singleton_le_one {W : Type} [DecidableEq W] [Fintype W] [MeasurableSpace W] [MeasurableSingletonClass W] (P : W → ℕ) (w : W) (C : Finset W) : (pairPrior P) {(w, C)} ≤ 1

theorem Warstadt2022.pairPrior_real {W : Type} [DecidableEq W] [Fintype W] [MeasurableSpace W] [MeasurableSingletonClass W] (P : W → ℕ) (w : W) (C : Finset W) : (pairPrior P).real {(w, C)} = if w ∈ C then ↑(P w) / ∑ v ∈ C, ↑(P v) else 0

instance Warstadt2022.instIsFiniteMeasureProdFinsetPairPrior {W : Type} [DecidableEq W] [Fintype W] [MeasurableSpace W] [MeasurableSingletonClass W] (P : W → ℕ) : MeasureTheory.IsFiniteMeasure (pairPrior P)

noncomputable def Warstadt2022.L0 {W U Q : Type} [Fintype W] [MeasurableSpace W] [Fintype U] [MeasurableSpace U] [MeasurableSingletonClass U] (P : W → ℕ) (cell : Q → W → Finset W) (sem : U → Set W) (C : Finset W) (q : Q) : ProbabilityTheory.Kernel U (Finset W)

The literal listener within a context set (3a) conditions the prior on the context set and on the utterance, and answers the question.

Equations

• Warstadt2022.L0 P cell sem C q = (RSA.listener ((MeasureTheory.Measure.ofWeights fun (x : W) => ↑(P x)).restrict ↑C) (RSA.truthful sem)).map (cell q)

instance Warstadt2022.instIsFiniteKernelFinsetL0 {W U Q : Type} [Fintype W] [MeasurableSpace W] [Fintype U] [MeasurableSpace U] [MeasurableSingletonClass U] (P : W → ℕ) (cell : Q → W → Finset W) (sem : U → Set W) (C : Finset W) (q : Q) : ProbabilityTheory.IsFiniteKernel (L0 P cell sem C q)

noncomputable def Warstadt2022.speaker {W U Q : Type} [Fintype W] [MeasurableSpace W] [Fintype U] [MeasurableSpace U] [MeasurableSingletonClass U] (P : W → ℕ) (cell : Q → W → Finset W) (sem : U → Set W) (C : Finset W) (q : Q) (α : ℝ) (w : W) : MeasureTheory.Measure U

The speaker within a context set (3b) is informative about the answer at her world, with no cost, and says nothing false there (3c).

Equations

• Warstadt2022.speaker P cell sem C q α w = ((RSA.speaker α 0 (⇑(Warstadt2022.L0 P cell sem C q)) MeasureTheory.Measure.dirac) (cell q w))[|{u : U | w ∈ sem u}]

instance Warstadt2022.instIsFiniteMeasureSpeaker {W U Q : Type} [Fintype W] [MeasurableSpace W] [Fintype U] [MeasurableSpace U] [MeasurableSingletonClass U] (P : W → ℕ) (cell : Q → W → Finset W) (sem : U → Set W) (C : Finset W) (q : Q) (α : ℝ) (w : W) : MeasureTheory.IsFiniteMeasure (speaker P cell sem C q α w)

noncomputable def Warstadt2022.share {W U Q : Type} [Fintype W] [MeasurableSpace W] [Fintype U] [MeasurableSpace U] [MeasurableSingletonClass U] (P : W → ℕ) (cell : Q → W → Finset W) (sem : U → Set W) (C : Finset W) (q : Q) (u : U) (w : W) (α : ℝ) : ℝ

The share of an utterance at a world within a context set, on reals.

Equations

• Warstadt2022.share P cell sem C q u w α = (Warstadt2022.speaker P cell sem C q α w).real {u}

noncomputable def Warstadt2022.listener {W U Q : Type} [DecidableEq W] [Fintype W] [MeasurableSpace W] [Fintype U] [MeasurableSpace U] [MeasurableSingletonClass U] (P : W → ℕ) (cell : Q → W → Finset W) (sem : U → Set W) (q : Q) (α : ℝ) : ProbabilityTheory.Kernel U (W × Finset W)

The pragmatic listener (3d) inverts the speaker jointly over worlds and context sets, given the question.

Equations

• Warstadt2022.listener P cell sem q α = RSA.listener (Warstadt2022.pairPrior P) fun (p : W × Finset W) => Warstadt2022.speaker P cell sem p.2 q α p.1

def Warstadt2022.worldEvent {W : Type} [DecidableEq W] [Fintype W] (w : W) : Finset (W × Finset W)

The pairs whose world is w.

Equations

• Warstadt2022.worldEvent w = Finset.image (fun (C : Finset W) => (w, C)) Finset.univ

theorem Warstadt2022.listener_worldEvent_lt_iff {W U Q : Type} [DecidableEq W] [Fintype W] [MeasurableSpace W] [MeasurableSingletonClass W] [Fintype U] [MeasurableSpace U] [MeasurableSingletonClass U] (P : W → ℕ) (cell : Q → W → Finset W) (sem : U → Set W) (q : Q) {α : ℝ} {u : U} (w₁ w₂ : W) : ((listener P cell sem q α) u).real ↑(worldEvent w₁) < ((listener P cell sem q α) u).real ↑(worldEvent w₂) ↔ ∑ C : Finset W, (pairPrior P).real {(w₁, C)} * share P cell sem C q u w₁ α < ∑ C : Finset W, (pairPrior P).real {(w₂, C)} * share P cell sem C q u w₂ α

The listener's preference between two worlds, marginalizing the context set, is the comparison of prior-weighted speaker shares summed over context sets.

theorem Warstadt2022.L0_apply {W U Q : Type} [DecidableEq W] [Fintype W] [MeasurableSpace W] [MeasurableSingletonClass W] [Fintype U] [MeasurableSpace U] [MeasurableSingletonClass U] {P : W → ℕ} {cell : Q → W → Finset W} {sem : U → Set W} {C : Finset W} {q : Q} [(u : U) → DecidablePred fun (x : W) => x ∈ sem u] [DiscreteMeasurableSpace W] {u : U} {w : W} (h : w ∈ sem u) : ((L0 P cell sem C q) u) {cell q w} = ↑(weight P cell sem C q u w).1 / ↑(weight P cell sem C q u w).2

theorem Warstadt2022.L0_apply_eq_one_iff {W U Q : Type} [DecidableEq W] [Fintype W] [MeasurableSpace W] [MeasurableSingletonClass W] [Fintype U] [MeasurableSpace U] [MeasurableSingletonClass U] {P : W → ℕ} {cell : Q → W → Finset W} {sem : U → Set W} {C : Finset W} {q : Q} [(u : U) → DecidablePred fun (x : W) => x ∈ sem u] [DiscreteMeasurableSpace W] {u : U} {w : W} (h : w ∈ sem u) (hC : w ∈ C) (hP : P w ≠ 0) : ((L0 P cell sem C q) u) {cell q w} = 1 ↔ (weight P cell sem C q u w).1 = (weight P cell sem C q u w).2

At a context-set world of positive prior where the utterance is true, the literal listener is certain of the answer exactly when the two components of the weight agree.

theorem Warstadt2022.share_eq {W U Q : Type} [DecidableEq W] [Fintype W] [MeasurableSpace W] [MeasurableSingletonClass W] [Fintype U] [MeasurableSpace U] [MeasurableSingletonClass U] {P : W → ℕ} {cell : Q → W → Finset W} {sem : U → Set W} {C : Finset W} {q : Q} [(u : U) → DecidablePred fun (x : W) => x ∈ sem u] [DiscreteMeasurableSpace W] {u : U} {w : W} {α : ℝ} (hα : 0 < α) : share P cell sem C q u w α = (↑(weight P cell sem C q u w).1 / ↑(weight P cell sem C q u w).2) ^ α / ∑ u' : U, (↑(weight P cell sem C q u' w).1 / ↑(weight P cell sem C q u' w).2) ^ α

The share of an utterance is its weight, raised to the rationality, among those of all utterances.

The green card scenario (Table 1)

inductive Warstadt2022.World : Type

Tom is a US citizen, a green card holder, or a non-US citizen without a green card.

• usCitizen : World
• gcHolder : World
• nonUS : World

@[instance_reducible]

instance Warstadt2022.instDecidableEqWorld : DecidableEq World

Equations

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

@[instance_reducible]

instance Warstadt2022.instFintypeWorld : Fintype World

Equations

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

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

Equations

• One or more equations did not get rendered due to their size.
• Warstadt2022.instReprWorld.repr Warstadt2022.World.nonUS prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Warstadt2022.World.nonUS")).group prec✝

@[instance_reducible]

instance Warstadt2022.instReprWorld : Repr World

Equations

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

@[instance_reducible]

instance Warstadt2022.instInhabitedWorld : Inhabited World

Equations

• Warstadt2022.instInhabitedWorld = { default := Warstadt2022.instInhabitedWorld.default }

@[instance_reducible]

instance Warstadt2022.instMeasurableSpaceWorld : MeasurableSpace World

Equations

• Warstadt2022.instMeasurableSpaceWorld = ⊤

instance Warstadt2022.instDiscreteMeasurableSpaceWorld : DiscreteMeasurableSpace World

instance Warstadt2022.instMeasurableSingletonClassWorld : MeasurableSingletonClass World

inductive Warstadt2022.Utterance : Type

Silence, US citizen, not US citizen, green card, not green card.

• silence : Utterance
• us : Utterance
• notUS : Utterance
• gc : Utterance
• notGC : Utterance

@[instance_reducible]

instance Warstadt2022.instDecidableEqUtterance : DecidableEq Utterance

Equations

• Warstadt2022.instDecidableEqUtterance x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Warstadt2022.instFintypeUtterance : Fintype Utterance

Equations

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

@[instance_reducible]

instance Warstadt2022.instReprUtterance : Repr Utterance

Equations

• Warstadt2022.instReprUtterance = { reprPrec := Warstadt2022.instReprUtterance.repr }

def Warstadt2022.instReprUtterance.repr : Utterance → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Warstadt2022.instInhabitedUtterance : Inhabited Utterance

Equations

• Warstadt2022.instInhabitedUtterance = { default := Warstadt2022.instInhabitedUtterance.default }

@[instance_reducible]

instance Warstadt2022.instMeasurableSpaceUtterance : MeasurableSpace Utterance

Equations

• Warstadt2022.instMeasurableSpaceUtterance = ⊤

instance Warstadt2022.instDiscreteMeasurableSpaceUtterance : DiscreteMeasurableSpace Utterance

instance Warstadt2022.instMeasurableSingletonClassUtterance : MeasurableSingletonClass Utterance

def Warstadt2022.Utterance.sem : Utterance → Set World

The truth conditions follow Table 1, and a negation is the complement.

Equations

• Warstadt2022.Utterance.silence.sem = Set.univ
• Warstadt2022.Utterance.us.sem = {w : Warstadt2022.World | w = Warstadt2022.World.usCitizen}
• Warstadt2022.Utterance.notUS.sem = {w : Warstadt2022.World | w ≠ Warstadt2022.World.usCitizen}
• Warstadt2022.Utterance.gc.sem = {w : Warstadt2022.World | w = Warstadt2022.World.gcHolder}
• Warstadt2022.Utterance.notGC.sem = {w : Warstadt2022.World | w ≠ Warstadt2022.World.gcHolder}

@[instance_reducible]

instance Warstadt2022.instDecidablePredWorldMemSetSem (u : Utterance) : DecidablePred fun (x : World) => x ∈ u.sem

Equations

• Warstadt2022.instDecidablePredWorldMemSetSem Warstadt2022.Utterance.silence x✝ = { decide := true, reflects_decide := ⋯ }
• Warstadt2022.instDecidablePredWorldMemSetSem Warstadt2022.Utterance.us x✝ = Warstadt2022.instDecidablePredWorldMemSetSem._aux_2 x✝
• Warstadt2022.instDecidablePredWorldMemSetSem Warstadt2022.Utterance.notUS x✝ = { decide := !decide (x✝ = Warstadt2022.World.usCitizen), reflects_decide := ⋯ }
• Warstadt2022.instDecidablePredWorldMemSetSem Warstadt2022.Utterance.gc x✝ = Warstadt2022.instDecidablePredWorldMemSetSem._aux_5 x✝
• Warstadt2022.instDecidablePredWorldMemSetSem Warstadt2022.Utterance.notGC x✝ = { decide := !decide (x✝ = Warstadt2022.World.gcHolder), reflects_decide := ⋯ }

inductive Warstadt2022.QUD : Type

Does Tom need a visa? Can Tom get a free drink?

• needVisa : QUD
• freeDrink : QUD

@[instance_reducible]

instance Warstadt2022.instDecidableEqQUD : DecidableEq QUD

Equations

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

@[instance_reducible]

instance Warstadt2022.instReprQUD : Repr QUD

Equations

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

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

Equations

• Warstadt2022.instReprQUD.repr Warstadt2022.QUD.needVisa prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Warstadt2022.QUD.needVisa")).group prec✝
• Warstadt2022.instReprQUD.repr Warstadt2022.QUD.freeDrink prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Warstadt2022.QUD.freeDrink")).group prec✝

def Warstadt2022.QUD.answer : QUD → World → Bool

The answer of a world to a question.

Equations

• Warstadt2022.QUD.needVisa.answer x✝ = decide (x✝ = Warstadt2022.World.nonUS)
• Warstadt2022.QUD.freeDrink.answer x✝ = decide (x✝ = Warstadt2022.World.gcHolder)

def Warstadt2022.QUD.cell (q : QUD) (w : World) : Finset World

The cell of a world holds the worlds with the same answer.

Equations

• q.cell w = {x : Warstadt2022.World | q.answer x = q.answer w}

def Warstadt2022.nonUSSets : List (Finset World)

The context sets containing the non-US world, and those containing the US-citizen world.

Equations

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

def Warstadt2022.usSets : List (Finset World)

Equations

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

def Warstadt2022.uniform : World → ℕ

The uniform world prior.

Equations

• Warstadt2022.uniform x✝ = 1

theorem Warstadt2022.freeDrink_exhaustive {C : Finset World} {w : World} (hC : w ∈ C) (h : w ∈ Utterance.notGC.sem) : ((L0 uniform QUD.cell Utterance.sem C QUD.freeDrink) Utterance.notGC) {QUD.freeDrink.cell w} = 1

Not green card settles the free-drink question in every context set, since at a world where it is true the literal listener is certain of the answer.

theorem Warstadt2022.needVisa_not_exhaustive : ((L0 uniform QUD.cell Utterance.sem {World.usCitizen, World.gcHolder, World.nonUS} QUD.needVisa) Utterance.notGC) {QUD.needVisa.cell World.usCitizen} = 1 / 2 ∧ ((L0 uniform QUD.cell Utterance.sem {World.gcHolder, World.nonUS} QUD.needVisa) Utterance.notGC) {QUD.needVisa.cell World.nonUS} = 1

It does not settle the visa question. In the universe the literal listener gives the US-citizen world's answer probability one half, while within the context set that Tom is not a US citizen he is certain of the non-US world's answer.

Shares

The listener over worlds

noncomputable def Warstadt2022.gcListener (q : QUD) (α : ℝ) : ProbabilityTheory.Kernel Utterance (World × Finset World)

The joint listener of the green card scenario.

Equations

• Warstadt2022.gcListener q α = Warstadt2022.listener Warstadt2022.uniform Warstadt2022.QUD.cell Warstadt2022.Utterance.sem q α

theorem Warstadt2022.needVisa_nonUS_lt {α : ℝ} (hα : 0 < α) : ((gcListener QUD.needVisa α) Utterance.notGC).real ↑(worldEvent World.usCitizen) < ((gcListener QUD.needVisa α) Utterance.notGC).real ↑(worldEvent World.nonUS)

With the question whether Tom needs a visa, not green card makes the listener favour the non-US world over the US-citizen world at every rationality. Within the context set that Tom is not a US citizen the utterance answers the question, whereas at the US-citizen world US citizen always answers it at least as well (Figure 1).

theorem Warstadt2022.freeDrink_nonUS_lt {α : ℝ} (hα : 0 < α) : ((gcListener QUD.freeDrink α) Utterance.notGC).real ↑(worldEvent World.usCitizen) < ((gcListener QUD.freeDrink α) Utterance.notGC).real ↑(worldEvent World.nonUS)

With the question whether Tom gets a free drink, not green card is an exhaustive answer in every context set, yet the listener still favours the non-US world. At the US-citizen world US citizen is an equally good answer, so the utterance's share there never exceeds a half (Figure 2 reports the two posteriors as nearly equal).

The family-genus-species scenario (Table 2)

inductive Warstadt2022.Hobby : Type

Tom is an Olympic sprinter, another runner, another athlete, or none of these.

• sprinter : Hobby
• runner : Hobby
• athlete : Hobby
• other : Hobby

@[instance_reducible]

instance Warstadt2022.instDecidableEqHobby : DecidableEq Hobby

Equations

• Warstadt2022.instDecidableEqHobby x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Warstadt2022.instFintypeHobby : Fintype Hobby

Equations

• Warstadt2022.instFintypeHobby = { elems := { val := ↑Warstadt2022.Hobby.enumList, nodup := Warstadt2022.Hobby.enumList_nodup }, complete := Warstadt2022.instFintypeHobby._proof_1 }

@[instance_reducible]

instance Warstadt2022.instReprHobby : Repr Hobby

Equations

• Warstadt2022.instReprHobby = { reprPrec := Warstadt2022.instReprHobby.repr }

def Warstadt2022.instReprHobby.repr : Hobby → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Warstadt2022.instReprHobby.repr Warstadt2022.Hobby.runner prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Warstadt2022.Hobby.runner")).group prec✝
• Warstadt2022.instReprHobby.repr Warstadt2022.Hobby.athlete prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Warstadt2022.Hobby.athlete")).group prec✝
• Warstadt2022.instReprHobby.repr Warstadt2022.Hobby.other prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Warstadt2022.Hobby.other")).group prec✝

@[instance_reducible]

instance Warstadt2022.instInhabitedHobby : Inhabited Hobby

Equations

• Warstadt2022.instInhabitedHobby = { default := Warstadt2022.instInhabitedHobby.default }

@[instance_reducible]

instance Warstadt2022.instMeasurableSpaceHobby : MeasurableSpace Hobby

Equations

• Warstadt2022.instMeasurableSpaceHobby = ⊤

instance Warstadt2022.instDiscreteMeasurableSpaceHobby : DiscreteMeasurableSpace Hobby

instance Warstadt2022.instMeasurableSingletonClassHobby : MeasurableSingletonClass Hobby

inductive Warstadt2022.HobbyUtterance : Type

The three predicates, affirmed or negated, and silence.

• silence : HobbyUtterance
• sprinter : HobbyUtterance
• notSprinter : HobbyUtterance
• runner : HobbyUtterance
• notRunner : HobbyUtterance
• athlete : HobbyUtterance
• notAthlete : HobbyUtterance

@[instance_reducible]

instance Warstadt2022.instDecidableEqHobbyUtterance : DecidableEq HobbyUtterance

Equations

• Warstadt2022.instDecidableEqHobbyUtterance x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Warstadt2022.instFintypeHobbyUtterance : Fintype HobbyUtterance

Equations

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

@[instance_reducible]

instance Warstadt2022.instReprHobbyUtterance : Repr HobbyUtterance

Equations

• Warstadt2022.instReprHobbyUtterance = { reprPrec := Warstadt2022.instReprHobbyUtterance.repr }

def Warstadt2022.instReprHobbyUtterance.repr : HobbyUtterance → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Warstadt2022.instInhabitedHobbyUtterance : Inhabited HobbyUtterance

Equations

• Warstadt2022.instInhabitedHobbyUtterance = { default := Warstadt2022.instInhabitedHobbyUtterance.default }

@[instance_reducible]

instance Warstadt2022.instMeasurableSpaceHobbyUtterance : MeasurableSpace HobbyUtterance

Equations

• Warstadt2022.instMeasurableSpaceHobbyUtterance = ⊤

instance Warstadt2022.instDiscreteMeasurableSpaceHobbyUtterance : DiscreteMeasurableSpace HobbyUtterance

instance Warstadt2022.instMeasurableSingletonClassHobbyUtterance : MeasurableSingletonClass HobbyUtterance

def Warstadt2022.HobbyUtterance.sem : HobbyUtterance → Set Hobby

The truth conditions of Table 2, respecting the hierarchy of the predicates.

Equations

• Warstadt2022.HobbyUtterance.silence.sem = Set.univ
• Warstadt2022.HobbyUtterance.sprinter.sem = {w : Warstadt2022.Hobby | w = Warstadt2022.Hobby.sprinter}
• Warstadt2022.HobbyUtterance.notSprinter.sem = {w : Warstadt2022.Hobby | w ≠ Warstadt2022.Hobby.sprinter}
• Warstadt2022.HobbyUtterance.runner.sem = {w : Warstadt2022.Hobby | w = Warstadt2022.Hobby.sprinter ∨ w = Warstadt2022.Hobby.runner}
• Warstadt2022.HobbyUtterance.notRunner.sem = {w : Warstadt2022.Hobby | ¬(w = Warstadt2022.Hobby.sprinter ∨ w = Warstadt2022.Hobby.runner)}
• Warstadt2022.HobbyUtterance.athlete.sem = {w : Warstadt2022.Hobby | w ≠ Warstadt2022.Hobby.other}
• Warstadt2022.HobbyUtterance.notAthlete.sem = {w : Warstadt2022.Hobby | w = Warstadt2022.Hobby.other}

@[instance_reducible]

instance Warstadt2022.instDecidablePredHobbyMemSetSem (u : HobbyUtterance) : DecidablePred fun (x : Hobby) => x ∈ u.sem

Equations

• One or more equations did not get rendered due to their size.
• Warstadt2022.instDecidablePredHobbyMemSetSem Warstadt2022.HobbyUtterance.silence x✝ = { decide := true, reflects_decide := ⋯ }
• Warstadt2022.instDecidablePredHobbyMemSetSem Warstadt2022.HobbyUtterance.sprinter x✝ = Warstadt2022.instDecidablePredHobbyMemSetSem._aux_2 x✝
• Warstadt2022.instDecidablePredHobbyMemSetSem Warstadt2022.HobbyUtterance.notSprinter x✝ = { decide := !decide (x✝ = Warstadt2022.Hobby.sprinter), reflects_decide := ⋯ }
• Warstadt2022.instDecidablePredHobbyMemSetSem Warstadt2022.HobbyUtterance.athlete x✝ = { decide := !decide (x✝ = Warstadt2022.Hobby.other), reflects_decide := ⋯ }
• Warstadt2022.instDecidablePredHobbyMemSetSem Warstadt2022.HobbyUtterance.notAthlete x✝ = Warstadt2022.instDecidablePredHobbyMemSetSem._aux_8 x✝

def Warstadt2022.hobbyWeight : Hobby → ℕ

The prior of Table 2, in percent.

Equations

• Warstadt2022.hobbyWeight Warstadt2022.Hobby.sprinter = 1
• Warstadt2022.hobbyWeight Warstadt2022.Hobby.runner = 5
• Warstadt2022.hobbyWeight Warstadt2022.Hobby.athlete = 10
• Warstadt2022.hobbyWeight Warstadt2022.Hobby.other = 84

def Warstadt2022.which : Unit → (w : Hobby) → Finset Hobby

Under the question which world it is, every cell is a singleton.

Equations

• Warstadt2022.which x✝ w = {w}

def Warstadt2022.hobbies : Finset Hobby

The universe of hobbies.

Equations

• Warstadt2022.hobbies = {Warstadt2022.Hobby.sprinter, Warstadt2022.Hobby.runner, Warstadt2022.Hobby.athlete, Warstadt2022.Hobby.other}

theorem Warstadt2022.notSprinter_exhaustive_iff {C : Finset Hobby} (hC : Hobby.runner ∈ C) : ((L0 hobbyWeight which HobbyUtterance.sem C ()) HobbyUtterance.notSprinter) {which () Hobby.runner} = 1 ↔ Hobby.athlete ∉ C ∧ Hobby.other ∉ C

Not an Olympic sprinter settles the question at the runner world exactly within context sets that exclude the athlete and the non-athlete world, so the accommodation the paper describes is of a common ground in which Tom is a runner or a sprinter.

theorem Warstadt2022.notRunner_exhaustive_iff {C : Finset Hobby} (hC : Hobby.athlete ∈ C) : ((L0 hobbyWeight which HobbyUtterance.sem C ()) HobbyUtterance.notRunner) {which () Hobby.athlete} = 1 ↔ Hobby.other ∉ C

Not a runner settles the question at the athlete world exactly within context sets that exclude the non-athlete world.

theorem Warstadt2022.other_share_lt {α : ℝ} (hα : 0 < α) : share hobbyWeight which HobbyUtterance.sem hobbies () HobbyUtterance.silence Hobby.other α < share hobbyWeight which HobbyUtterance.sem hobbies () HobbyUtterance.notSprinter Hobby.other α ∧ share hobbyWeight which HobbyUtterance.sem hobbies () HobbyUtterance.notSprinter Hobby.other α < share hobbyWeight which HobbyUtterance.sem hobbies () HobbyUtterance.notRunner Hobby.other α ∧ share hobbyWeight which HobbyUtterance.sem hobbies () HobbyUtterance.notRunner Hobby.other α < share hobbyWeight which HobbyUtterance.sem hobbies () HobbyUtterance.notAthlete Hobby.other α

At the non-athlete world in the universe, not an Olympic sprinter is produced more often than silence but less often than not a runner, which loses to not an athlete. Olympic sprinters are rare, so denying that Tom is one says little (4).