Alsop (2024): The Pragmatics of Free Choice any

You may read any book does not entail that each book may be read on its own, the exclusiveness reading that Menéndez-Benito observes and Dayal's Viability Constraint builds in. Symmetric predicates (3) and world knowledge (22) block it and (23) cancels it, so on Szabolcsi's Revised Viability Constraint semantics it is a robust implicature. The two constraints are the two licit exhaustified parses (34a)–(34b) of the utterance (meaning, Table 2), and a Global Intentions listener resolves which parse a speaker intended: the speaker chooses an utterance–parse pair (speaker), and the listener recovers state and parse from the utterance alone (listener).

The strong parse (34b) is the speaker's choice at the exclusiveness states for every rationality (speaker_prefers_strong_parse), and at a uniform prior the listener hearing may any prefers each of Only 1 and Any # to each of Only 2, S or 2, and P or 2, again for every rationality (exclusiveness_derived, Table 3), while inferring the strong parse at the paper's α = 100 (listener_infers_strong_parse). May S communicates Only S (literal_s_communicates_onlyS), and the parse (35b) of may every, true at Any # but not at Only 1, makes Only 1 the strictly likelier of the two (only1_over_anyNum), the asymmetry behind the not every implicature, which Table 3 rounds to 0.50/0.50. The model takes the state prior as an argument, which enters the literal listener too; the numerical results of the prior manipulations of Tables 5–9 are not re-derived here.

References

• [Als24]
• [MB10]
• [Day13]
• [Sza19]
• [Chi13]
• [CAG19]
• [FB20b]
• [Xia20]

States, utterances, parses (Tables 1–2)

inductive Alsop2024.State : Type

A permission state (Table 1) is the set of accessible worlds among taking nothing, only Semantics, only Phonology, or both. There are seven, since taking nothing is always accessible.

• onlyS : State
• onlyP : State
• only1 : State
• anyNum : State
• only2 : State
• sOr2 : State
• pOr2 : State

@[instance_reducible]

instance Alsop2024.instDecidableEqState : DecidableEq State

Equations

• Alsop2024.instDecidableEqState x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Alsop2024.instReprState.repr : State → ℕ → Std.Format

Equations

• Alsop2024.instReprState.repr Alsop2024.State.onlyS prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Alsop2024.State.onlyS")).group prec✝
• Alsop2024.instReprState.repr Alsop2024.State.onlyP prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Alsop2024.State.onlyP")).group prec✝
• Alsop2024.instReprState.repr Alsop2024.State.only1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Alsop2024.State.only1")).group prec✝
• Alsop2024.instReprState.repr Alsop2024.State.anyNum prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Alsop2024.State.anyNum")).group prec✝
• Alsop2024.instReprState.repr Alsop2024.State.only2 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Alsop2024.State.only2")).group prec✝
• Alsop2024.instReprState.repr Alsop2024.State.sOr2 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Alsop2024.State.sOr2")).group prec✝
• Alsop2024.instReprState.repr Alsop2024.State.pOr2 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Alsop2024.State.pOr2")).group prec✝

@[instance_reducible]

instance Alsop2024.instReprState : Repr State

Equations

• Alsop2024.instReprState = { reprPrec := Alsop2024.instReprState.repr }

@[instance_reducible]

instance Alsop2024.instFintypeState : Fintype State

Equations

• Alsop2024.instFintypeState = { elems := { val := ↑Alsop2024.State.enumList, nodup := Alsop2024.State.enumList_nodup }, complete := Alsop2024.instFintypeState._proof_1 }

@[instance_reducible]

instance Alsop2024.instInhabitedState : Inhabited State

Equations

• Alsop2024.instInhabitedState = { default := Alsop2024.instInhabitedState.default }

@[instance_reducible]

instance Alsop2024.instMeasurableSpaceState : MeasurableSpace State

Equations

• Alsop2024.instMeasurableSpaceState = ⊤

instance Alsop2024.instDiscreteMeasurableSpaceState : DiscreteMeasurableSpace State

inductive Alsop2024.Utterance : Type

The four utterances (31).

• mayS : Utterance
• mayP : Utterance
• mayAny : Utterance
• mayEvery : Utterance

@[instance_reducible]

instance Alsop2024.instDecidableEqUtterance : DecidableEq Utterance

Equations

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

@[instance_reducible]

instance Alsop2024.instReprUtterance : Repr Utterance

Equations

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

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

Equations

• One or more equations did not get rendered due to their size.
• Alsop2024.instReprUtterance.repr Alsop2024.Utterance.mayS prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Alsop2024.Utterance.mayS")).group prec✝
• Alsop2024.instReprUtterance.repr Alsop2024.Utterance.mayP prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Alsop2024.Utterance.mayP")).group prec✝
• Alsop2024.instReprUtterance.repr Alsop2024.Utterance.mayAny prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Alsop2024.Utterance.mayAny")).group prec✝

@[instance_reducible]

instance Alsop2024.instFintypeUtterance : Fintype Utterance

Equations

• Alsop2024.instFintypeUtterance = { elems := { val := ↑Alsop2024.Utterance.enumList, nodup := Alsop2024.Utterance.enumList_nodup }, complete := Alsop2024.instFintypeUtterance._proof_1 }

@[instance_reducible]

instance Alsop2024.instMeasurableSpaceUtterance : MeasurableSpace Utterance

Equations

• Alsop2024.instMeasurableSpaceUtterance = ⊤

instance Alsop2024.instDiscreteMeasurableSpaceUtterance : DiscreteMeasurableSpace Utterance

inductive Alsop2024.Parse : Type

The twelve utterance–parse pairs are those of (32)–(35), with a the weakest parse of each utterance. May any has two, the weak parse (34a) giving Szabolcsi's meaning and the strong parse (34b) Dayal's.

• sA : Parse
• sB : Parse
• sC : Parse
• pA : Parse
• pB : Parse
• pC : Parse
• anyA : Parse
• anyB : Parse
• evA : Parse
• evB : Parse
• evC : Parse
• evD : Parse

@[instance_reducible]

instance Alsop2024.instDecidableEqParse : DecidableEq Parse

Equations

• Alsop2024.instDecidableEqParse x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Alsop2024.instReprParse : Repr Parse

Equations

• Alsop2024.instReprParse = { reprPrec := Alsop2024.instReprParse.repr }

def Alsop2024.instReprParse.repr : Parse → ℕ → Std.Format

Equations

• Alsop2024.instReprParse.repr Alsop2024.Parse.sA prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Alsop2024.Parse.sA")).group prec✝
• Alsop2024.instReprParse.repr Alsop2024.Parse.sB prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Alsop2024.Parse.sB")).group prec✝
• Alsop2024.instReprParse.repr Alsop2024.Parse.sC prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Alsop2024.Parse.sC")).group prec✝
• Alsop2024.instReprParse.repr Alsop2024.Parse.pA prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Alsop2024.Parse.pA")).group prec✝
• Alsop2024.instReprParse.repr Alsop2024.Parse.pB prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Alsop2024.Parse.pB")).group prec✝
• Alsop2024.instReprParse.repr Alsop2024.Parse.pC prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Alsop2024.Parse.pC")).group prec✝
• Alsop2024.instReprParse.repr Alsop2024.Parse.anyA prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Alsop2024.Parse.anyA")).group prec✝
• Alsop2024.instReprParse.repr Alsop2024.Parse.anyB prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Alsop2024.Parse.anyB")).group prec✝
• Alsop2024.instReprParse.repr Alsop2024.Parse.evA prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Alsop2024.Parse.evA")).group prec✝
• Alsop2024.instReprParse.repr Alsop2024.Parse.evB prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Alsop2024.Parse.evB")).group prec✝
• Alsop2024.instReprParse.repr Alsop2024.Parse.evC prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Alsop2024.Parse.evC")).group prec✝
• Alsop2024.instReprParse.repr Alsop2024.Parse.evD prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Alsop2024.Parse.evD")).group prec✝

@[instance_reducible]

instance Alsop2024.instFintypeParse : Fintype Parse

Equations

• Alsop2024.instFintypeParse = { elems := { val := ↑Alsop2024.Parse.enumList, nodup := Alsop2024.Parse.enumList_nodup }, complete := Alsop2024.instFintypeParse._proof_1 }

@[instance_reducible]

instance Alsop2024.instInhabitedParse : Inhabited Parse

Equations

• Alsop2024.instInhabitedParse = { default := Alsop2024.instInhabitedParse.default }

@[instance_reducible]

instance Alsop2024.instMeasurableSpaceParse : MeasurableSpace Parse

Equations

• Alsop2024.instMeasurableSpaceParse = ⊤

instance Alsop2024.instDiscreteMeasurableSpaceParse : DiscreteMeasurableSpace Parse

def Alsop2024.Parse.utt : Parse → Utterance

The utterance a parse belongs to.

Equations

• Alsop2024.Parse.sA.utt = Alsop2024.Utterance.mayS
• Alsop2024.Parse.sB.utt = Alsop2024.Utterance.mayS
• Alsop2024.Parse.sC.utt = Alsop2024.Utterance.mayS
• Alsop2024.Parse.pA.utt = Alsop2024.Utterance.mayP
• Alsop2024.Parse.pB.utt = Alsop2024.Utterance.mayP
• Alsop2024.Parse.pC.utt = Alsop2024.Utterance.mayP
• Alsop2024.Parse.anyA.utt = Alsop2024.Utterance.mayAny
• Alsop2024.Parse.anyB.utt = Alsop2024.Utterance.mayAny
• Alsop2024.Parse.evA.utt = Alsop2024.Utterance.mayEvery
• Alsop2024.Parse.evB.utt = Alsop2024.Utterance.mayEvery
• Alsop2024.Parse.evC.utt = Alsop2024.Utterance.mayEvery
• Alsop2024.Parse.evD.utt = Alsop2024.Utterance.mayEvery

def Alsop2024.meaning : Parse → State → Prop

The states at which each parse is true (Table 2).

Equations

• Alsop2024.meaning Alsop2024.Parse.sA x✝ = (x✝ ≠ Alsop2024.State.onlyP)
• Alsop2024.meaning Alsop2024.Parse.sB x✝ = (x✝ = Alsop2024.State.onlyS ∨ x✝ = Alsop2024.State.only1 ∨ x✝ = Alsop2024.State.anyNum ∨ x✝ = Alsop2024.State.sOr2)
• Alsop2024.meaning Alsop2024.Parse.sC x✝ = (x✝ = Alsop2024.State.onlyS)
• Alsop2024.meaning Alsop2024.Parse.pA x✝ = (x✝ ≠ Alsop2024.State.onlyS)
• Alsop2024.meaning Alsop2024.Parse.pB x✝ = (x✝ = Alsop2024.State.onlyP ∨ x✝ = Alsop2024.State.only1 ∨ x✝ = Alsop2024.State.anyNum ∨ x✝ = Alsop2024.State.pOr2)
• Alsop2024.meaning Alsop2024.Parse.pC x✝ = (x✝ = Alsop2024.State.onlyP)
• Alsop2024.meaning Alsop2024.Parse.anyA x✝ = (x✝ ≠ Alsop2024.State.onlyS ∧ x✝ ≠ Alsop2024.State.onlyP)
• Alsop2024.meaning Alsop2024.Parse.anyB x✝ = (x✝ = Alsop2024.State.only1 ∨ x✝ = Alsop2024.State.anyNum)
• Alsop2024.meaning Alsop2024.Parse.evA x✝ = (x✝ ≠ Alsop2024.State.onlyS ∧ x✝ ≠ Alsop2024.State.onlyP)
• Alsop2024.meaning Alsop2024.Parse.evB x✝ = (x✝ = Alsop2024.State.anyNum ∨ x✝ = Alsop2024.State.only2 ∨ x✝ = Alsop2024.State.sOr2 ∨ x✝ = Alsop2024.State.pOr2)
• Alsop2024.meaning Alsop2024.Parse.evC x✝ = (x✝ = Alsop2024.State.only1 ∨ x✝ = Alsop2024.State.anyNum)
• Alsop2024.meaning Alsop2024.Parse.evD x✝ = (x✝ = Alsop2024.State.only2)

@[instance_reducible]

instance Alsop2024.instDecidablePredStateMeaning (p : Parse) : DecidablePred (meaning p)

Equations

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

def Alsop2024.sem (p : Parse) : Finset State

The extension of each parse.

Equations

• Alsop2024.sem p = Finset.filter (Alsop2024.meaning p) Finset.univ

@[simp]

theorem Alsop2024.mem_sem {p : Parse} {s : State} : s ∈ sem p ↔ meaning p s

def Alsop2024.LiterallyTrue (s : State) : Prop

May any is literally true at a state when some parse of it is.

Equations

• Alsop2024.LiterallyTrue s = ∃ (p : Alsop2024.Parse), p.utt = Alsop2024.Utterance.mayAny ∧ Alsop2024.meaning p s

@[instance_reducible]

instance Alsop2024.instDecidablePredStateLiterallyTrue : DecidablePred LiterallyTrue

Equations

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

theorem Alsop2024.literallyTrue_iff (s : State) : LiterallyTrue s ↔ meaning Parse.anyA s

The strong parse (34b) entails the weak parse (34a), so may any is literally true exactly where Szabolcsi's meaning holds.

The Global Intentions model (36)–(41)

@[reducible, inline]

noncomputable abbrev Alsop2024.literal (μ : MeasureTheory.Measure State) : ProbabilityTheory.Kernel Parse State

The literal listener (36) conditions the state prior on the meaning of the parse.

Equations

• Alsop2024.literal μ = RSA.listener μ (RSA.truthful fun (p : Alsop2024.Parse) => ↑(Alsop2024.sem p))

@[reducible, inline]

noncomputable abbrev Alsop2024.speaker (μ : MeasureTheory.Measure State) (α : ℝ) : ProbabilityTheory.Kernel State Parse

The speaker (37)–(38) knows the state and chooses an utterance together with a parse, at equal costs.

Equations

• Alsop2024.speaker μ α = RSA.speaker α 0 (⇑(Alsop2024.literal μ)) MeasureTheory.Measure.dirac

@[reducible, inline]

noncomputable abbrev Alsop2024.listener (μ : MeasureTheory.Measure State) (α : ℝ) : ProbabilityTheory.Kernel Utterance (State × Parse)

The pragmatic listener (40) hears the utterance of the speaker's choice and infers the state and the parse; her first marginal is her belief about the state (41). The state prior enters the literal listener too, the setting of Tables 5–9.

Equations

• Alsop2024.listener μ α = RSA.listener (μ.compProd (Alsop2024.speaker μ α)) fun (p : Alsop2024.State × Alsop2024.Parse) => MeasureTheory.Measure.dirac p.2.utt

The findings at a uniform prior (Table 3)

theorem Alsop2024.speaker_prefers_strong_parse {α : ℝ} (hα : 0 < α) {s : State} (hs : meaning Parse.anyB s) : ((speaker (ProbabilityTheory.uniformOn Set.univ) α) s).real {Parse.anyA} < ((speaker (ProbabilityTheory.uniformOn Set.univ) α) s).real {Parse.anyB}

At an exclusiveness state the speaker prefers the strong parse (34b) of may any to the weak parse (34a) at every rationality, since the weak parse is true in five states and the strong in two. At α = 100 the ratio is (5/2)^100, the paper's "almost 100% of the time".

theorem Alsop2024.mayAny_rules_out_onlyS {α : ℝ} (hα : 0 < α) (p : Parse) : ((listener (ProbabilityTheory.uniformOn Set.univ) α) Utterance.mayAny) {(State.onlyS, p)} = 0

Hearing may any, the listener assigns no posterior to Only S under any parse.

theorem Alsop2024.mayEvery_rules_out_onlyS {α : ℝ} (hα : 0 < α) (p : Parse) : ((listener (ProbabilityTheory.uniformOn Set.univ) α) Utterance.mayEvery) {(State.onlyS, p)} = 0

Hearing may every, the listener assigns no posterior to Only S under any parse.

theorem Alsop2024.exclusiveness_derived {α : ℝ} (hα : 0 < α) (s : State) : s ∈ {State.only2, State.sOr2, State.pOr2} → ∀ s' ∈ {State.only1, State.anyNum}, ((listener (ProbabilityTheory.uniformOn Set.univ) α) Utterance.mayAny).fst.real {s} < ((listener (ProbabilityTheory.uniformOn Set.univ) α) Utterance.mayAny).fst.real {s'}

Hearing may any, the listener prefers each exclusiveness state, Only 1 and Any #, where each class may be taken on its own (the paper's 0.50 + 0.50), to each of Only 2, S or 2, and P or 2 (each ≈ 0), at every rationality. This is the exclusiveness implicature of Table 3.

theorem Alsop2024.listener_infers_strong_parse : ((listener (ProbabilityTheory.uniformOn Set.univ) 100) Utterance.mayAny).snd.real {Parse.anyA} < ((listener (ProbabilityTheory.uniformOn Set.univ) 100) Utterance.mayAny).snd.real {Parse.anyB}

Hearing may any at the paper's α = 100, the listener infers the strong parse (34b) over the weak parse (34a), the speaker's near-categorical parse preference pooled over states.

theorem Alsop2024.literal_s_communicates_onlyS {α : ℝ} (hα : 0 < α) : ((listener (ProbabilityTheory.uniformOn Set.univ) α) Utterance.mayS).fst.real {State.sOr2} < ((listener (ProbabilityTheory.uniformOn Set.univ) α) Utterance.mayS).fst.real {State.onlyS}

Hearing may S, the listener prefers Only S to S or 2 at every rationality (0.67 against 0.33 in Table 3), since the doubly exhaustified parse (32c) is available only at Only S.

theorem Alsop2024.only1_over_anyNum {α : ℝ} (hα : 0 < α) : ((listener (ProbabilityTheory.uniformOn Set.univ) α) Utterance.mayAny).fst.real {State.anyNum} < ((listener (ProbabilityTheory.uniformOn Set.univ) α) Utterance.mayAny).fst.real {State.only1}

Hearing may any, Only 1 is strictly likelier than Any # at every rationality. Both parses of may any weigh the same at the two states, but the parse (35b) of may every is true at Any # and not at Only 1, inflating the speaker's partition there. Table 3 reports 0.50/0.50 (at α = 100 the difference is ≈ 2·10⁻³¹); the same asymmetry drives the not every implicature under an Only-1-favouring prior (Table 6).

The paper's scenarios

def Alsop2024.rowState (row : Datum) : Option State

The state a scenario fixes, where the paper says which.

Equations

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

def Alsop2024.observedLiteral (row : Datum) : Bool

A row's literal truth is judged by its explicit literal reading if it has one, and otherwise by the row's own judgment.

Equations

• Alsop2024.observedLiteral row = match List.lookup "literal" row.readings with | some j => j == Judgment.acceptable | none => row.judgment == Judgment.acceptable

theorem Alsop2024.rows_agree (row : Datum) : row ∈ Examples.all → ∀ s ∈ rowState row, (LiterallyTrue s ↔ observedLiteral row = true) ∧ ∀ j ∈ List.lookup "exclusiveness" row.readings, meaning Parse.anyB s ↔ j = Judgment.acceptable

At every scenario with a fixed state, may any is literally true exactly where the paper judges it so, and the exclusiveness reading holds exactly where Dayal's parse (34b) is true, so the all-or-nothing scenarios are true but not exclusive.