[Als24] — The pragmatics of free choice any

[Als24] (Glossa 9(1)) argues that You may read any book does not entail that each book may be read on its own ([menendez-benito-2010], [dayal-2013]'s Viability Constraint) — it carries a particularly robust exclusiveness implicature, derived pragmatically from [szabolcsi-2019]'s weaker semantics. The derivation combines [CAG19]'s ambiguity-driven free choice with [FB20b]'s Global Intentions architecture: each utterance comes with its own set of licit exhaustified parses, the speaker chooses an utterance–parse pair jointly, and the listener infers state and intended parse together.

The model (the paper's §5, eqs. (36)–(41)): seven permission states over a two-class domain (their Table 1); four utterances with 12 utterance–parse pairs in total (3 for may S, 3 for may P, 2 for may any, 4 for may every; truth conditions in their Table 2); L0(s|u,p) ∝ P(s)·⟦u⟧ᵖ(s); S1(u,p|s) ∝ exp(α·log L0) over all 12 pairs; L1(s,p|u) ∝ P(s)·S1(u,p|s) with parse-marginal L1(s|u). Speaker optimality α = 100, equal costs.

Instantiated on the canonical pipeline: L0 is RSA.Canonical.L0OfBool over the Table-2 matrix, the joint speaker is RSA.Canonical.S1 with powUtility, the parse-marginal speaker is its PMF.map along Parse.utt, and the pragmatic listener is RSA.Canonical.L1.

Main statements

• exclusiveness_derived — at a uniform prior, hearing may any puts more posterior mass on the exclusiveness states {Only 1, Any #} than on the non-exclusive states {Only 2, S or 2, P or 2} (their Table 3).
• mayAny_rules_out_onlyS / mayEvery_rules_out_onlyS — may any and may every are false at single-class states under every parse.
• s1_prefers_strong_parse — the mechanism: at an exclusiveness state the speaker prefers the strong parse (their (34b)) of may any to the weak parse ((34a)), for every exponent α ≥ 1 — the weak parse is true in five states, the strong in two.
• literal_s_communicates_onlyS — hearing may S, the listener prefers the Only-S state to the S-or-2 state (their Table 3: 0.67 vs 0.33).
• exclusiveness_strict_asymmetry — a refinement the paper's Table 3 rounds away: L1(Only 1 | may any) strictly exceeds L1(Any # | may any) at every exponent, because may every's parse (35b) is true at Any # but not Only 1, inflating the speaker's partition at Any #. The paper reports 0.50/0.50 at α = 100 (the difference is ≈ 2·10⁻³¹).

Context manipulation (verified prose)

The paper's Tables 5–9 manipulate the state prior, which enters L0 (eq. (36)); independently recomputed, every reported cell reproduces exactly. The not every implicature is absent at a uniform prior (the 50/50 split above), derived under a 70%-Only-1 prior (L1(Only 1) ≈ 1, robust for all scanned α ≥ 1), and the Any-#-biased prior shifts L1 to 0.93 while S1 stays 50/50 — a prior-driven shift, not an implicature (the paper's eq. (1)). Robustness of exclusiveness to a 70%-S-or-2 prior (Table 5: 0.49/0.49/0.02) genuinely needs α ≥ 45, so the paper's α = 100 does real work there. These prior-in-L0 results are recorded as prose rather than theorems per the parameter-dependence policy.

Implementation notes

Theorems are at the paper's α = 100 (the parse preference at every α ≥ 1) with a uniform prior, by ℕ-certificate dominance bounds — no numeric reflection. The previous version of this file modelled two global interpretation functions with an interpretation prior at α = 2 — the [CAG19] architecture that the paper explicitly replaces with [FB20b]'s — and included a negation finding with no counterpart in the paper's model (its utterance set has no negation; NPI any is set aside in the paper's §2.1).

States, utterances, parses (the paper's Tables 1–2)

inductive Alsop2024.FCIState : Type

The seven permission states (their Table 1), each a set of accessible worlds over {take nothing, take S, take P, take both}; every state makes taking nothing accessible.

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

@[implicit_reducible]

instance Alsop2024.instDecidableEqFCIState : DecidableEq FCIState

Equations

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

def Alsop2024.instReprFCIState.repr : FCIState → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Alsop2024.instReprFCIState : Repr FCIState

Equations

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

@[implicit_reducible]

instance Alsop2024.instInhabitedFCIState : Inhabited FCIState

Equations

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

@[implicit_reducible]

instance Alsop2024.instFintypeFCIState : Fintype FCIState

Equations

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

inductive Alsop2024.Utterance : Type

The four utterances (their (31)).

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

@[implicit_reducible]

instance Alsop2024.instDecidableEqUtterance : DecidableEq Utterance

Equations

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

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✝

@[implicit_reducible]

instance Alsop2024.instReprUtterance : Repr Utterance

Equations

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

@[implicit_reducible]

instance Alsop2024.instInhabitedUtterance : Inhabited Utterance

Equations

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

@[implicit_reducible]

instance Alsop2024.instFintypeUtterance : Fintype Utterance

Equations

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

inductive Alsop2024.Parse : Type

The 12 utterance–parse pairs (their (32)–(35)): per-utterance licit exhaustified parses, a the weakest. May any has exactly two — the weak parse (34a, Szabolcsi: every class may be taken, possibly only together) and the strong parse (34b, Dayal: every class may be taken on its own).

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

@[implicit_reducible]

instance Alsop2024.instDecidableEqParse : DecidableEq Parse

Equations

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

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✝

@[implicit_reducible]

instance Alsop2024.instReprParse : Repr Parse

Equations

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

@[implicit_reducible]

instance Alsop2024.instInhabitedParse : Inhabited Parse

Equations

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

@[implicit_reducible]

instance Alsop2024.instFintypeParse : Fintype Parse

Equations

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

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 → FCIState → Bool

Truth conditions for each utterance–parse pair (their Table 2).

Equations

• Alsop2024.meaning Alsop2024.Parse.sA Alsop2024.FCIState.onlyS = true
• Alsop2024.meaning Alsop2024.Parse.sA Alsop2024.FCIState.only1 = true
• Alsop2024.meaning Alsop2024.Parse.sA Alsop2024.FCIState.anyNum = true
• Alsop2024.meaning Alsop2024.Parse.sA Alsop2024.FCIState.only2 = true
• Alsop2024.meaning Alsop2024.Parse.sA Alsop2024.FCIState.sOr2 = true
• Alsop2024.meaning Alsop2024.Parse.sA Alsop2024.FCIState.pOr2 = true
• Alsop2024.meaning Alsop2024.Parse.sA x✝ = false
• Alsop2024.meaning Alsop2024.Parse.sB Alsop2024.FCIState.onlyS = true
• Alsop2024.meaning Alsop2024.Parse.sB Alsop2024.FCIState.only1 = true
• Alsop2024.meaning Alsop2024.Parse.sB Alsop2024.FCIState.anyNum = true
• Alsop2024.meaning Alsop2024.Parse.sB Alsop2024.FCIState.sOr2 = true
• Alsop2024.meaning Alsop2024.Parse.sB x✝ = false
• Alsop2024.meaning Alsop2024.Parse.sC Alsop2024.FCIState.onlyS = true
• Alsop2024.meaning Alsop2024.Parse.sC x✝ = false
• Alsop2024.meaning Alsop2024.Parse.pA Alsop2024.FCIState.onlyP = true
• Alsop2024.meaning Alsop2024.Parse.pA Alsop2024.FCIState.only1 = true
• Alsop2024.meaning Alsop2024.Parse.pA Alsop2024.FCIState.anyNum = true
• Alsop2024.meaning Alsop2024.Parse.pA Alsop2024.FCIState.only2 = true
• Alsop2024.meaning Alsop2024.Parse.pA Alsop2024.FCIState.sOr2 = true
• Alsop2024.meaning Alsop2024.Parse.pA Alsop2024.FCIState.pOr2 = true
• Alsop2024.meaning Alsop2024.Parse.pA x✝ = false
• Alsop2024.meaning Alsop2024.Parse.pB Alsop2024.FCIState.onlyP = true
• Alsop2024.meaning Alsop2024.Parse.pB Alsop2024.FCIState.only1 = true
• Alsop2024.meaning Alsop2024.Parse.pB Alsop2024.FCIState.anyNum = true
• Alsop2024.meaning Alsop2024.Parse.pB Alsop2024.FCIState.pOr2 = true
• Alsop2024.meaning Alsop2024.Parse.pB x✝ = false
• Alsop2024.meaning Alsop2024.Parse.pC Alsop2024.FCIState.onlyP = true
• Alsop2024.meaning Alsop2024.Parse.pC x✝ = false
• Alsop2024.meaning Alsop2024.Parse.anyA Alsop2024.FCIState.only1 = true
• Alsop2024.meaning Alsop2024.Parse.anyA Alsop2024.FCIState.anyNum = true
• Alsop2024.meaning Alsop2024.Parse.anyA Alsop2024.FCIState.only2 = true
• Alsop2024.meaning Alsop2024.Parse.anyA Alsop2024.FCIState.sOr2 = true
• Alsop2024.meaning Alsop2024.Parse.anyA Alsop2024.FCIState.pOr2 = true
• Alsop2024.meaning Alsop2024.Parse.anyA x✝ = false
• Alsop2024.meaning Alsop2024.Parse.anyB Alsop2024.FCIState.only1 = true
• Alsop2024.meaning Alsop2024.Parse.anyB Alsop2024.FCIState.anyNum = true
• Alsop2024.meaning Alsop2024.Parse.anyB x✝ = false
• Alsop2024.meaning Alsop2024.Parse.evA Alsop2024.FCIState.only1 = true
• Alsop2024.meaning Alsop2024.Parse.evA Alsop2024.FCIState.anyNum = true
• Alsop2024.meaning Alsop2024.Parse.evA Alsop2024.FCIState.only2 = true
• Alsop2024.meaning Alsop2024.Parse.evA Alsop2024.FCIState.sOr2 = true
• Alsop2024.meaning Alsop2024.Parse.evA Alsop2024.FCIState.pOr2 = true
• Alsop2024.meaning Alsop2024.Parse.evA x✝ = false
• Alsop2024.meaning Alsop2024.Parse.evB Alsop2024.FCIState.anyNum = true
• Alsop2024.meaning Alsop2024.Parse.evB Alsop2024.FCIState.only2 = true
• Alsop2024.meaning Alsop2024.Parse.evB Alsop2024.FCIState.sOr2 = true
• Alsop2024.meaning Alsop2024.Parse.evB Alsop2024.FCIState.pOr2 = true
• Alsop2024.meaning Alsop2024.Parse.evB x✝ = false
• Alsop2024.meaning Alsop2024.Parse.evC Alsop2024.FCIState.only1 = true
• Alsop2024.meaning Alsop2024.Parse.evC Alsop2024.FCIState.anyNum = true
• Alsop2024.meaning Alsop2024.Parse.evC x✝ = false
• Alsop2024.meaning Alsop2024.Parse.evD Alsop2024.FCIState.only2 = true
• Alsop2024.meaning Alsop2024.Parse.evD x✝ = false

The canonical GI pipeline

@[reducible, inline]

noncomputable abbrev Alsop2024.l0 : Unit → Parse → PMF FCIState

Per-parse literal listener (eq. (36) at a uniform state prior): uniform on the parse's extension.

Equations

• Alsop2024.l0 = RSA.Canonical.L0OfBool (fun (x : Unit) (p : Alsop2024.Parse) => Alsop2024.meaning p) Alsop2024.ext_nonempty✝

instance Alsop2024.instViableSpeakerProdFCIStateUnitParsePowUtilityL0 (α : ℕ) : RSA.Canonical.ViableSpeaker (RSA.Canonical.powUtility α l0)

noncomputable def Alsop2024.speaker (α : ℕ) : FCIState × Unit → PMF Parse

The joint speaker over utterance–parse pairs (eqs. (37)–(38)): S1(u,p|s) ∝ L0(s|u,p)^α, equal costs.

Equations

• Alsop2024.speaker α = RSA.Canonical.S1 (RSA.Canonical.powUtility α Alsop2024.l0)

noncomputable def Alsop2024.speakerU (α : ℕ) (s : FCIState × Unit) : PMF Utterance

The parse-marginal speaker (eq. (39)): S1(u|s) = Σ_p S1(u,p|s).

Equations

• Alsop2024.speakerU α s = PMF.map Alsop2024.Parse.utt (Alsop2024.speaker α s)

@[reducible, inline]

noncomputable abbrev Alsop2024.prior : PMF (FCIState × Unit)

Uniform joint state prior.

Equations

• Alsop2024.prior = PMF.uniformOfFintype (Alsop2024.FCIState × Unit)

theorem Alsop2024.marginal_ne_zero (α : ℕ) (u : Utterance) : PMF.marginal (speakerU α) prior u ≠ 0

noncomputable def Alsop2024.listener (α : ℕ) (u : Utterance) : PMF (FCIState × Unit)

The pragmatic listener over states (eqs. (40)–(41), parse-marginal): the canonical posterior of the parse-marginal speaker.

Equations

• Alsop2024.listener α u = RSA.Canonical.L1 (Alsop2024.speakerU α) Alsop2024.prior u ⋯

Extension sizes (their Table 2 row sums)

B1 zeros: may any and may every exclude single-class states

theorem Alsop2024.speakerU_onlyS_mayAny (α : ℕ) (hα : α ≠ 0) : (speakerU α (FCIState.onlyS, ())) Utterance.mayAny = 0

Both parses of may any are false at Only-S, so the speaker never produces it there.

theorem Alsop2024.mayAny_rules_out_onlyS (α : ℕ) (hα : α ≠ 0) : (listener α Utterance.mayAny) (FCIState.onlyS, ()) = 0

Hearing may any, the listener assigns zero posterior to Only-S.

theorem Alsop2024.speakerU_onlyS_mayEvery (α : ℕ) (hα : α ≠ 0) : (speakerU α (FCIState.onlyS, ())) Utterance.mayEvery = 0

All four parses of may every are false at Only-S.

theorem Alsop2024.mayEvery_rules_out_onlyS (α : ℕ) (hα : α ≠ 0) : (listener α Utterance.mayEvery) (FCIState.onlyS, ()) = 0

Hearing may every, the listener assigns zero posterior to Only-S.

The mechanism: the strong parse wins

theorem Alsop2024.s1_prefers_strong_parse {α : ℕ} (hα : α ≠ 0) : (speaker α (FCIState.only1, ())) Parse.anyA < (speaker α (FCIState.only1, ())) Parse.anyB

At the Only-1 state the speaker prefers the strong parse (34b) of may any to the weak parse (34a), for every exponent α ≥ 1: the weak parse is true in five states (L0 = 1/5), the strong in two (L0 = 1/2), and within one state the softmax partition cancels. At α = 100 the ratio is (5/2)^100, the paper's "almost 100% of the time".

Exclusiveness (their Table 3, uniform prior, α = 100)

Per-state speaker bounds: at the exclusiveness states the strong parse alone gives may any more than a third of the speaker's mass; at the non-exclusive states only the weak parse survives and is dominated.

theorem Alsop2024.exclusiveness_derived : (listener 100 Utterance.mayAny).toOuterMeasure ↑{(FCIState.only2, ()), (FCIState.sOr2, ()), (FCIState.pOr2, ())} < (listener 100 Utterance.mayAny).toOuterMeasure ↑{(FCIState.only1, ()), (FCIState.anyNum, ())}

The exclusiveness implicature (their Table 3): hearing may any at a uniform prior, the listener puts more posterior mass on the exclusiveness states {Only 1, Any #} (where each class may be taken on its own; the paper's 0.50 + 0.50) than on the non-exclusive states {Only 2, S or 2, P or 2} (each ≈ 0).

May S communicates Only-S (their Table 3: 0.67 vs 0.33)

theorem Alsop2024.literal_s_communicates_onlyS : (listener 100 Utterance.mayS).toOuterMeasure ↑{(FCIState.sOr2, ())} < (listener 100 Utterance.mayS).toOuterMeasure ↑{(FCIState.onlyS, ())}

Hearing may S, the listener prefers Only-S to S-or-2 (their Table 3: 0.67 vs 0.33): the dedicated exhaustified parse (32c) is only available at Only-S.

The strict Only-1 / Any-# asymmetry (refining their Table 3)

theorem Alsop2024.exclusiveness_strict_asymmetry : (listener 100 Utterance.mayAny).toOuterMeasure ↑{(FCIState.anyNum, ())} < (listener 100 Utterance.mayAny).toOuterMeasure ↑{(FCIState.only1, ())}

The asymmetry the paper's Table 3 rounds away: at a uniform prior, L1(Only 1 | may any) strictly exceeds L1(Any # | may any) — the paper reports 0.50/0.50 at α = 100 (the difference is ≈ 2·10⁻³¹). Both parses of may any carry the same weight at the two states, but may every's parse (35b) is true at Any # and not at Only 1, strictly inflating the speaker's partition there, so the speaker is less likely to choose may any at Any #. A formaliser's refinement, not a claim of the paper's.