@cite{alsop-2024} — Free Choice Any as GI-RSA

@cite{alsop-2024} @cite{champollion-alsop-grosu-2019} @cite{franke-bergen-2020} @cite{tessler-franke-2019}

"Disjunction, Free Choice, and Exhaustification" (Chapter 4)

The Model

Domain: "You may take any class" with 2 items {S, P}. 7 states based on permission structure (which baskets are permitted). 4 utterances. 2 global interpretation functions (weak/Szabolcsi vs strong/Dayal), following the GI-RSA architecture of @cite{franke-bergen-2020}.

• L0: L0(w|u,I) ∝ ⟦u⟧^I(w) (meaning under interpretation I)
• S1: S1(u|w,I) ∝ L0(w|u,I)^α (rpow belief-based)
• L1: L1(w|u) ∝ P(w) · Σ_I P(I) · S1(u|w,I)

Parameters: α = 2, uniform interpretation prior, configurable world prior.

Qualitative Findings

#	Finding	Theorem
1	Exclusiveness derived	exclusiveness_derived
2	Exclusiveness robust to prior	exclusiveness_robust
3	Not-every holds under uniform prior	not_every_uniform
4	Not-every weakened under biased prior	not_every_weakened
5	Hearing "may S" → S is permitted	literal_s_correct
6	Hearing "may every" → both permitted	every_permBoth
7	Ambiguity essential for FC	exclusiveness_requires_ambiguity
8	No FC under negation	no_fc_under_negation

inductive RSA.FCIAny.FCIState : Type

The 7 states from @cite{alsop-2024} for a 2-item domain {S, P}. Each state is defined by which baskets are permitted: w0 (nothing), wS (S only), wP (P only), wSP (both).

• onlyS : FCIState
• onlyP : FCIState
• only1 : FCIState
• anyNum : FCIState
• only2 : FCIState
• sOrBoth : FCIState
• pOrBoth : FCIState

instance RSA.FCIAny.instDecidableEqFCIState : DecidableEq FCIState

Equations

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

instance RSA.FCIAny.instBEqFCIState : BEq FCIState

Equations

• RSA.FCIAny.instBEqFCIState = { beq := RSA.FCIAny.instBEqFCIState.beq }

def RSA.FCIAny.instBEqFCIState.beq : FCIState → FCIState → Bool

Equations

• RSA.FCIAny.instBEqFCIState.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def RSA.FCIAny.instReprFCIState.repr : FCIState → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• RSA.FCIAny.instReprFCIState.repr RSA.FCIAny.FCIState.onlyS prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "RSA.FCIAny.FCIState.onlyS")).group prec✝
• RSA.FCIAny.instReprFCIState.repr RSA.FCIAny.FCIState.onlyP prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "RSA.FCIAny.FCIState.onlyP")).group prec✝
• RSA.FCIAny.instReprFCIState.repr RSA.FCIAny.FCIState.only1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "RSA.FCIAny.FCIState.only1")).group prec✝
• RSA.FCIAny.instReprFCIState.repr RSA.FCIAny.FCIState.anyNum prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "RSA.FCIAny.FCIState.anyNum")).group prec✝
• RSA.FCIAny.instReprFCIState.repr RSA.FCIAny.FCIState.only2 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "RSA.FCIAny.FCIState.only2")).group prec✝

instance RSA.FCIAny.instReprFCIState : Repr FCIState

Equations

• RSA.FCIAny.instReprFCIState = { reprPrec := RSA.FCIAny.instReprFCIState.repr }

instance RSA.FCIAny.instInhabitedFCIState : Inhabited FCIState

Equations

• RSA.FCIAny.instInhabitedFCIState = { default := RSA.FCIAny.instInhabitedFCIState.default }

def RSA.FCIAny.instInhabitedFCIState.default : FCIState

Equations

• RSA.FCIAny.instInhabitedFCIState.default = RSA.FCIAny.FCIState.onlyS

instance RSA.FCIAny.instFintypeFCIState : Fintype FCIState

Equations

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

inductive RSA.FCIAny.Utterance : Type

The 4 utterances.

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

instance RSA.FCIAny.instDecidableEqUtterance : DecidableEq Utterance

Equations

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

def RSA.FCIAny.instBEqUtterance.beq : Utterance → Utterance → Bool

Equations

• RSA.FCIAny.instBEqUtterance.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance RSA.FCIAny.instBEqUtterance : BEq Utterance

Equations

• RSA.FCIAny.instBEqUtterance = { beq := RSA.FCIAny.instBEqUtterance.beq }

instance RSA.FCIAny.instReprUtterance : Repr Utterance

Equations

• RSA.FCIAny.instReprUtterance = { reprPrec := RSA.FCIAny.instReprUtterance.repr }

def RSA.FCIAny.instReprUtterance.repr : Utterance → ℕ → Std.Format

Equations

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

instance RSA.FCIAny.instInhabitedUtterance : Inhabited Utterance

Equations

• RSA.FCIAny.instInhabitedUtterance = { default := RSA.FCIAny.instInhabitedUtterance.default }

def RSA.FCIAny.instInhabitedUtterance.default : Utterance

Equations

• RSA.FCIAny.instInhabitedUtterance.default = RSA.FCIAny.Utterance.mayS

instance RSA.FCIAny.instFintypeUtterance : Fintype Utterance

Equations

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

inductive RSA.FCIAny.Interp : Type

Two global interpretation functions (GI-RSA). Each assigns a meaning to every utterance simultaneously.

• weak : Interp
• strong : Interp

instance RSA.FCIAny.instDecidableEqInterp : DecidableEq Interp

Equations

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

def RSA.FCIAny.instBEqInterp.beq : Interp → Interp → Bool

Equations

• RSA.FCIAny.instBEqInterp.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance RSA.FCIAny.instBEqInterp : BEq Interp

Equations

• RSA.FCIAny.instBEqInterp = { beq := RSA.FCIAny.instBEqInterp.beq }

instance RSA.FCIAny.instReprInterp : Repr Interp

Equations

• RSA.FCIAny.instReprInterp = { reprPrec := RSA.FCIAny.instReprInterp.repr }

def RSA.FCIAny.instReprInterp.repr : Interp → ℕ → Std.Format

Equations

• RSA.FCIAny.instReprInterp.repr RSA.FCIAny.Interp.weak prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "RSA.FCIAny.Interp.weak")).group prec✝
• RSA.FCIAny.instReprInterp.repr RSA.FCIAny.Interp.strong prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "RSA.FCIAny.Interp.strong")).group prec✝

def RSA.FCIAny.instInhabitedInterp.default : Interp

Equations

• RSA.FCIAny.instInhabitedInterp.default = RSA.FCIAny.Interp.weak

instance RSA.FCIAny.instInhabitedInterp : Inhabited Interp

Equations

• RSA.FCIAny.instInhabitedInterp = { default := RSA.FCIAny.instInhabitedInterp.default }

instance RSA.FCIAny.instFintypeInterp : Fintype Interp

Equations

• RSA.FCIAny.instFintypeInterp = { elems := {RSA.FCIAny.Interp.weak, RSA.FCIAny.Interp.strong}, complete := RSA.FCIAny.instFintypeInterp._proof_1 }

def RSA.FCIAny.permS : FCIState → Bool

◇take(S)_strict: taking S alone is a permitted basket (wS accessible).

Equations

• RSA.FCIAny.permS RSA.FCIAny.FCIState.onlyS = true
• RSA.FCIAny.permS RSA.FCIAny.FCIState.only1 = true
• RSA.FCIAny.permS RSA.FCIAny.FCIState.anyNum = true
• RSA.FCIAny.permS RSA.FCIAny.FCIState.sOrBoth = true
• RSA.FCIAny.permS x✝ = false

def RSA.FCIAny.permP : FCIState → Bool

◇take(P)_strict: taking P alone is a permitted basket (wP accessible).

Equations

• RSA.FCIAny.permP RSA.FCIAny.FCIState.onlyP = true
• RSA.FCIAny.permP RSA.FCIAny.FCIState.only1 = true
• RSA.FCIAny.permP RSA.FCIAny.FCIState.anyNum = true
• RSA.FCIAny.permP RSA.FCIAny.FCIState.pOrBoth = true
• RSA.FCIAny.permP x✝ = false

def RSA.FCIAny.permBoth : FCIState → Bool

◇take(S∧P): taking both together is permitted (wSP accessible).

Equations

• RSA.FCIAny.permBoth RSA.FCIAny.FCIState.anyNum = true
• RSA.FCIAny.permBoth RSA.FCIAny.FCIState.only2 = true
• RSA.FCIAny.permBoth RSA.FCIAny.FCIState.sOrBoth = true
• RSA.FCIAny.permBoth RSA.FCIAny.FCIState.pOrBoth = true
• RSA.FCIAny.permBoth x✝ = false

def RSA.FCIAny.permS_liberal (w : FCIState) : Bool

◇take(S)_liberal: S is obtainable (alone or via both).

Equations

• RSA.FCIAny.permS_liberal w = (RSA.FCIAny.permS w || RSA.FCIAny.permBoth w)

def RSA.FCIAny.permP_liberal (w : FCIState) : Bool

◇take(P)_liberal: P is obtainable (alone or via both).

Equations

• RSA.FCIAny.permP_liberal w = (RSA.FCIAny.permP w || RSA.FCIAny.permBoth w)

def RSA.FCIAny.hasExclusiveness : FCIState → Bool

Exclusiveness: each item is individually (strictly) permitted. ∀x[◇take(x)_strict]. True at {only1, anyNum}.

Equations

• RSA.FCIAny.hasExclusiveness RSA.FCIAny.FCIState.only1 = true
• RSA.FCIAny.hasExclusiveness RSA.FCIAny.FCIState.anyNum = true
• RSA.FCIAny.hasExclusiveness x✝ = false

def RSA.FCIAny.hasNotEvery : FCIState → Bool

Not-every: taking both is not permitted. ¬◇(S∧P). True at {onlyS, onlyP, only1}.

Equations

• RSA.FCIAny.hasNotEvery RSA.FCIAny.FCIState.onlyS = true
• RSA.FCIAny.hasNotEvery RSA.FCIAny.FCIState.onlyP = true
• RSA.FCIAny.hasNotEvery RSA.FCIAny.FCIState.only1 = true
• RSA.FCIAny.hasNotEvery x✝ = false

def RSA.FCIAny.weakMeaning : Utterance → FCIState → Bool

Weak (Szabolcsi) interpretation: unexhaustified meanings.

• May S: ◇take(S)_liberal (6 states, all except onlyP)
• May P: ◇take(P)_liberal (6 states, all except onlyS)
• May Any: ∃x[◇take(x)] (7 states, always true)
• May Every: ◇take(S∧P) (4 states: anyNum, only2, sOrBoth, pOrBoth)

Equations

• RSA.FCIAny.weakMeaning RSA.FCIAny.Utterance.mayS x✝ = RSA.FCIAny.permS_liberal x✝
• RSA.FCIAny.weakMeaning RSA.FCIAny.Utterance.mayP x✝ = RSA.FCIAny.permP_liberal x✝
• RSA.FCIAny.weakMeaning RSA.FCIAny.Utterance.mayAny x✝ = true
• RSA.FCIAny.weakMeaning RSA.FCIAny.Utterance.mayEvery x✝ = RSA.FCIAny.permBoth x✝

def RSA.FCIAny.strongMeaning : Utterance → FCIState → Bool

Strong (Dayal) interpretation: exhaustified meanings.

• May S: {onlyS} (only S permitted, not P, not both)
• May P: {onlyP} (only P permitted, not S, not both)
• May Any: {only1, anyNum} (∀x[◇take(x)_strict], exclusiveness)
• May Every: {only2} (must take both, neither alone)

Equations

• RSA.FCIAny.strongMeaning RSA.FCIAny.Utterance.mayS RSA.FCIAny.FCIState.onlyS = true
• RSA.FCIAny.strongMeaning RSA.FCIAny.Utterance.mayP RSA.FCIAny.FCIState.onlyP = true
• RSA.FCIAny.strongMeaning RSA.FCIAny.Utterance.mayAny RSA.FCIAny.FCIState.only1 = true
• RSA.FCIAny.strongMeaning RSA.FCIAny.Utterance.mayAny RSA.FCIAny.FCIState.anyNum = true
• RSA.FCIAny.strongMeaning RSA.FCIAny.Utterance.mayEvery RSA.FCIAny.FCIState.only2 = true
• RSA.FCIAny.strongMeaning x✝¹ x✝ = false

def RSA.FCIAny.interpMeaning : Interp → Utterance → FCIState → Bool

Combined meaning function indexed by interpretation.

Equations

• RSA.FCIAny.interpMeaning RSA.FCIAny.Interp.weak = RSA.FCIAny.weakMeaning
• RSA.FCIAny.interpMeaning RSA.FCIAny.Interp.strong = RSA.FCIAny.strongMeaning

theorem RSA.FCIAny.strong_characterizes_exclusiveness (w : FCIState) : strongMeaning Utterance.mayAny w = hasExclusiveness w

The strong interpretation characterizes exclusiveness exactly.

theorem RSA.FCIAny.weak_mayAny_always_true (w : FCIState) : weakMeaning Utterance.mayAny w = true

The weak interpretation is always true for "may any".

theorem RSA.FCIAny.exclusiveness_eq_allStrict (w : FCIState) : hasExclusiveness w = (permS w && permP w)

Exclusiveness = ∀x[◇take(x)_strict].

theorem RSA.FCIAny.notEvery_eq_not_permBoth (w : FCIState) : hasNotEvery w = !permBoth w

Not-every = ¬permBoth.

theorem RSA.FCIAny.strong_refines_weak (u : Utterance) (w : FCIState) : strongMeaning u w = true → weakMeaning u w = true

The strong interpretation refines the weak for all utterances.

theorem RSA.FCIAny.permission_correspondence : (permS FCIState.onlyS = true ∧ permP FCIState.onlyS = false ∧ permBoth FCIState.onlyS = false) ∧ (permS FCIState.only1 = true ∧ permP FCIState.only1 = true ∧ permBoth FCIState.only1 = false) ∧ permS FCIState.only2 = false ∧ permP FCIState.only2 = false ∧ permBoth FCIState.only2 = true

Permission predicates correctly characterize key states.

noncomputable def RSA.FCIAny.cfg (worldPr : FCIState → ℝ) (hp : ∀ (w : FCIState), 0 ≤ worldPr w) : RSAConfig Utterance FCIState

@cite{alsop-2024} GI-RSA model for free choice any. Two global interpretations serve as latent variables. S1 score is rpow(L0, α) — standard belief-based RSA.

Equations

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

@[reducible, inline]

noncomputable abbrev RSA.FCIAny.uniformCfg : RSAConfig Utterance FCIState

Uniform prior: all states equally likely.

Equations

• RSA.FCIAny.uniformCfg = RSA.FCIAny.cfg (fun (x : RSA.FCIAny.FCIState) => 1) RSA.FCIAny.uniformCfg._proof_1

@[reducible, inline]

noncomputable abbrev RSA.FCIAny.biasedCfg : RSAConfig Utterance FCIState

Biased prior: P(anyNum) = 3, others = 1. Biases toward the state where exclusiveness holds but not-every does not, testing prior sensitivity of the two inferences.

Equations

• RSA.FCIAny.biasedCfg = RSA.FCIAny.cfg (fun (w : RSA.FCIAny.FCIState) => match w with | RSA.FCIAny.FCIState.anyNum => 3 | x => 1) RSA.FCIAny.biasedCfg._proof_2

theorem RSA.FCIAny.exclusiveness_derived : uniformCfg.L1_marginal Utterance.mayAny hasExclusiveness > uniformCfg.L1_marginal Utterance.mayAny fun (w : FCIState) => !hasExclusiveness w

Exclusiveness is derived: L1 assigns more mass to exclusiveness states than non-exclusiveness states upon hearing "may any".

theorem RSA.FCIAny.exclusiveness_robust : biasedCfg.L1_marginal Utterance.mayAny hasExclusiveness > biasedCfg.L1_marginal Utterance.mayAny fun (w : FCIState) => !hasExclusiveness w

Exclusiveness is robust: holds even under a prior biased toward anyNum.

theorem RSA.FCIAny.not_every_uniform : uniformCfg.L1_marginal Utterance.mayAny hasNotEvery > uniformCfg.L1_marginal Utterance.mayAny fun (w : FCIState) => !hasNotEvery w

Not-every holds under uniform prior.

theorem RSA.FCIAny.not_every_weakened : ¬biasedCfg.L1_marginal Utterance.mayAny hasNotEvery > biasedCfg.L1_marginal Utterance.mayAny fun (w : FCIState) => !hasNotEvery w

Not-every is weakened under biased prior (prior-sensitive).

theorem RSA.FCIAny.literal_s_correct : (uniformCfg.L1_marginal Utterance.mayS fun (w : FCIState) => permS w) > uniformCfg.L1_marginal Utterance.mayS fun (w : FCIState) => !permS w

Hearing "may S", the listener infers S is (strictly) permitted.

theorem RSA.FCIAny.every_permBoth : (uniformCfg.L1_marginal Utterance.mayEvery fun (w : FCIState) => permBoth w) > uniformCfg.L1_marginal Utterance.mayEvery fun (w : FCIState) => !permBoth w

Hearing "may every", the listener infers both are permitted.

noncomputable def RSA.FCIAny.weakOnlyCfg : RSAConfig Utterance FCIState

Counterfactual: both interpretations use weak meaning (no ambiguity). Without the informativity gap between weak (7 states for "may any") and strong (2 states), S1 cannot discriminate exclusiveness states.

Equations

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

theorem RSA.FCIAny.exclusiveness_requires_ambiguity : ¬weakOnlyCfg.L1_marginal Utterance.mayAny hasExclusiveness > weakOnlyCfg.L1_marginal Utterance.mayAny fun (w : FCIState) => !hasExclusiveness w

Without interpretation ambiguity, exclusiveness is NOT derived. The informativity gap between weak (7 states) and strong (2 states) is what drives L1 toward exclusiveness states. Without a strong parse, "may any" is uninformative and the prior dominates: 2/7 exclusiveness states vs 5/7 non-exclusiveness states.

inductive RSA.FCIAny.UtteranceNeg : Type

Extended utterances including negation of "may any".

• mayS : UtteranceNeg
• mayP : UtteranceNeg
• mayAny : UtteranceNeg
• mayEvery : UtteranceNeg
• mayNotAny : UtteranceNeg

instance RSA.FCIAny.instDecidableEqUtteranceNeg : DecidableEq UtteranceNeg

Equations

• RSA.FCIAny.instDecidableEqUtteranceNeg x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def RSA.FCIAny.instBEqUtteranceNeg.beq : UtteranceNeg → UtteranceNeg → Bool

Equations

• RSA.FCIAny.instBEqUtteranceNeg.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance RSA.FCIAny.instBEqUtteranceNeg : BEq UtteranceNeg

Equations

• RSA.FCIAny.instBEqUtteranceNeg = { beq := RSA.FCIAny.instBEqUtteranceNeg.beq }

def RSA.FCIAny.instReprUtteranceNeg.repr : UtteranceNeg → ℕ → Std.Format

Equations

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

instance RSA.FCIAny.instReprUtteranceNeg : Repr UtteranceNeg

Equations

• RSA.FCIAny.instReprUtteranceNeg = { reprPrec := RSA.FCIAny.instReprUtteranceNeg.repr }

def RSA.FCIAny.instInhabitedUtteranceNeg.default : UtteranceNeg

Equations

• RSA.FCIAny.instInhabitedUtteranceNeg.default = RSA.FCIAny.UtteranceNeg.mayS

instance RSA.FCIAny.instInhabitedUtteranceNeg : Inhabited UtteranceNeg

Equations

• RSA.FCIAny.instInhabitedUtteranceNeg = { default := RSA.FCIAny.instInhabitedUtteranceNeg.default }

instance RSA.FCIAny.instFintypeUtteranceNeg : Fintype UtteranceNeg

Equations

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

def RSA.FCIAny.weakMeaningNeg : UtteranceNeg → FCIState → Bool

Weak meaning extended with negation. "May not any" under weak = ¬∃x[◇take(x)] = false everywhere, since the weak existential meaning is trivially true at all states.

Equations

• RSA.FCIAny.weakMeaningNeg RSA.FCIAny.UtteranceNeg.mayS x✝ = RSA.FCIAny.permS_liberal x✝
• RSA.FCIAny.weakMeaningNeg RSA.FCIAny.UtteranceNeg.mayP x✝ = RSA.FCIAny.permP_liberal x✝
• RSA.FCIAny.weakMeaningNeg RSA.FCIAny.UtteranceNeg.mayAny x✝ = true
• RSA.FCIAny.weakMeaningNeg RSA.FCIAny.UtteranceNeg.mayEvery x✝ = RSA.FCIAny.permBoth x✝
• RSA.FCIAny.weakMeaningNeg RSA.FCIAny.UtteranceNeg.mayNotAny x✝ = false

def RSA.FCIAny.strongMeaningNeg : UtteranceNeg → FCIState → Bool

Strong meaning extended with negation. "May not any" under strong = ¬∀x[◇take(x)_strict] = ¬hasExclusiveness. True at 5 of 7 states (all except only1 and anyNum).

Equations

• RSA.FCIAny.strongMeaningNeg RSA.FCIAny.UtteranceNeg.mayS RSA.FCIAny.FCIState.onlyS = true
• RSA.FCIAny.strongMeaningNeg RSA.FCIAny.UtteranceNeg.mayP RSA.FCIAny.FCIState.onlyP = true
• RSA.FCIAny.strongMeaningNeg RSA.FCIAny.UtteranceNeg.mayAny RSA.FCIAny.FCIState.only1 = true
• RSA.FCIAny.strongMeaningNeg RSA.FCIAny.UtteranceNeg.mayAny RSA.FCIAny.FCIState.anyNum = true
• RSA.FCIAny.strongMeaningNeg RSA.FCIAny.UtteranceNeg.mayEvery RSA.FCIAny.FCIState.only2 = true
• RSA.FCIAny.strongMeaningNeg RSA.FCIAny.UtteranceNeg.mayNotAny x✝ = !RSA.FCIAny.hasExclusiveness x✝
• RSA.FCIAny.strongMeaningNeg x✝¹ x✝ = false

def RSA.FCIAny.interpMeaningNeg : Interp → UtteranceNeg → FCIState → Bool

Combined meaning for the extended model.

Equations

• RSA.FCIAny.interpMeaningNeg RSA.FCIAny.Interp.weak = RSA.FCIAny.weakMeaningNeg
• RSA.FCIAny.interpMeaningNeg RSA.FCIAny.Interp.strong = RSA.FCIAny.strongMeaningNeg

noncomputable def RSA.FCIAny.negCfg : RSAConfig UtteranceNeg FCIState

RSAConfig for the extended model with negation.

Equations

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

theorem RSA.FCIAny.no_fc_under_negation : ¬negCfg.L1_marginal UtteranceNeg.mayNotAny hasExclusiveness > negCfg.L1_marginal UtteranceNeg.mayNotAny fun (w : FCIState) => !hasExclusiveness w

Free choice does NOT emerge under negation. Under negation, the weak interpretation is vacuous (false everywhere) and the strong interpretation supports only non-exclusiveness states. The informativity gap that drives FC in the positive case disappears.

inductive RSA.FCIAny.Finding : Type

The 8 qualitative findings from @cite{alsop-2024}.

• exclusiveness_derived : Finding
• exclusiveness_robust : Finding
• not_every_uniform : Finding
• not_every_weakened : Finding
• literal_s_correct : Finding
• every_permBoth : Finding
• exclusiveness_requires_ambiguity : Finding
• no_fc_under_negation : Finding

instance RSA.FCIAny.instDecidableEqFinding : DecidableEq Finding

Equations

• RSA.FCIAny.instDecidableEqFinding x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def RSA.FCIAny.instBEqFinding.beq : Finding → Finding → Bool

Equations

• RSA.FCIAny.instBEqFinding.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance RSA.FCIAny.instBEqFinding : BEq Finding

Equations

• RSA.FCIAny.instBEqFinding = { beq := RSA.FCIAny.instBEqFinding.beq }

def RSA.FCIAny.instReprFinding.repr : Finding → ℕ → Std.Format

Equations

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

instance RSA.FCIAny.instReprFinding : Repr Finding

Equations

• RSA.FCIAny.instReprFinding = { reprPrec := RSA.FCIAny.instReprFinding.repr }

noncomputable def RSA.FCIAny.formalize : Finding → Prop

Map each finding to its RSA formalization.

Equations

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

theorem RSA.FCIAny.all_findings_verified (f : Finding) : formalize f

The RSA model accounts for all 8 findings from @cite{alsop-2024}.

Bridge content (merged from RSA_Alsop2024Bridge.lean)

Bridge: RSA Free Choice Any → Phenomena Data

@cite{alsop-2024}

Connects the RSA free choice any model from @cite{alsop-2024} to empirical data in Phenomena.Modality.FreeChoice.

Bridge Theorems

• predicts_fci_any: Exclusiveness arises for permission any
• predicts_robustness: Exclusiveness is robust to prior manipulation

Connection to Phenomena

The model predicts the patterns in Phenomena.Modality.FreeChoice:

1. FCI Any (anyClass, anyFruit):

   • "You may take any class" → permission for each class specifically
   • Derived: L1 assigns ~100% to exclusiveness states

2. Robustness to priors:

   • Exclusiveness holds even with unfavorable priors
   • Parallels FCI robustness in disjunction

3. Not-every is cancelable:

   • "You may take any class (in fact, you must take all of them)"
   • The "not every" inference can be cancelled, unlike exclusiveness

theorem Phenomena.Modality.RSA_Alsop2024Bridge.predicts_fci_any : FreeChoice.anyClass.exclusivenessArises = true

Free choice any is predicted for permission sentences

theorem Phenomena.Modality.RSA_Alsop2024Bridge.predicts_robustness : FreeChoice.anyClass.robustToPriors = true

Exclusiveness is robust to priors (as recorded in the data)