@cite{champollion-alsop-grosu-2019} — Free Choice Disjunction as RSA

@cite{champollion-alsop-grosu-2019} @cite{bergen-levy-goodman-2016} @cite{fox-2007} @cite{franke-2011}"Free choice disjunction as a rational speech act" Proceedings of SALT 29: 238-257.

The Model

Domain: "You may take an apple or a pear" with 2 items {A, B}. 5 states based on permission structure. 4 utterances. 2 interpretation functions (I₁ literal vs I₂ exhaustified), following @cite{bergen-levy-goodman-2016}.

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

Parameters: α = 2 (paper uses α = 100; qualitative predictions hold at α = 2, where "L1 assigns only 70% probability to the FCI states" — p. 249).

Key Innovation

Standard RSA cannot derive free choice because disjunction is always less informative than its disjuncts. Adding semantic uncertainty — speakers and listeners reason about which interpretation function is being used — creates an avoidance pattern that drives the inference.

The two interpretation functions represent optional exhaustification:

• I₁: Literal meanings (unexhaustified)
• I₂: Strengthened meanings (exhaustified)

How Free Choice Emerges

1. S1 wants to convey "Only One" (each item individually permitted)
2. If S1 says "You may A", L0 might interpret via I₂ as "Only A"
3. To avoid this misunderstanding, S1 uses disjunction
4. L1 reasons: "S1 chose Or to prevent me thinking Only A or Only B"
5. L1 infers: Only One or Any Number → Free choice

Qualitative Findings

#	Finding	Theorem
1	FCI derived (uniform prior)	fci_derived
2	FCI robust to biased prior	fci_robust_to_prior
3	EI holds under uniform prior	ei_uniform
4	EI weakened under biased prior	ei_prior_sensitive

State Space (Table 2)

State	◇A	◇B	◇(A∧B)	FCI?	EI?
Only A	T	F	F	no	yes
Only B	F	T	F	no	yes
Only One	T	T	F	yes	yes
Any Number	T	T	T	yes	no
Only Both	T	T	T	no	no

Note: "Only Both" means you may ONLY take both together (not either alone).

inductive RSA.FreeChoice.FCState : Type

The 5 states from Table 2, based on permission structure.

• onlyA : FCState
• onlyB : FCState
• onlyOne : FCState
• anyNumber : FCState
• onlyBoth : FCState

instance RSA.FreeChoice.instDecidableEqFCState : DecidableEq FCState

Equations

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

instance RSA.FreeChoice.instBEqFCState : BEq FCState

Equations

• RSA.FreeChoice.instBEqFCState = { beq := RSA.FreeChoice.instBEqFCState.beq }

def RSA.FreeChoice.instBEqFCState.beq : FCState → FCState → Bool

Equations

• RSA.FreeChoice.instBEqFCState.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def RSA.FreeChoice.instReprFCState.repr : FCState → ℕ → Std.Format

Equations

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

instance RSA.FreeChoice.instReprFCState : Repr FCState

Equations

• RSA.FreeChoice.instReprFCState = { reprPrec := RSA.FreeChoice.instReprFCState.repr }

instance RSA.FreeChoice.instInhabitedFCState : Inhabited FCState

Equations

• RSA.FreeChoice.instInhabitedFCState = { default := RSA.FreeChoice.instInhabitedFCState.default }

def RSA.FreeChoice.instInhabitedFCState.default : FCState

Equations

• RSA.FreeChoice.instInhabitedFCState.default = RSA.FreeChoice.FCState.onlyA

instance RSA.FreeChoice.instFintypeFCState : Fintype FCState

Equations

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

inductive RSA.FreeChoice.Utterance : Type

The 4 utterances from (5).

• a : Utterance
• b : Utterance
• or_ : Utterance
• and_ : Utterance

instance RSA.FreeChoice.instDecidableEqUtterance : DecidableEq Utterance

Equations

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

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

Equations

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

instance RSA.FreeChoice.instBEqUtterance : BEq Utterance

Equations

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

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

Equations

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

instance RSA.FreeChoice.instReprUtterance : Repr Utterance

Equations

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

def RSA.FreeChoice.instInhabitedUtterance.default : Utterance

Equations

• RSA.FreeChoice.instInhabitedUtterance.default = RSA.FreeChoice.Utterance.a

instance RSA.FreeChoice.instInhabitedUtterance : Inhabited Utterance

Equations

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

instance RSA.FreeChoice.instFintypeUtterance : Fintype Utterance

Equations

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

inductive RSA.FreeChoice.Interp : Type

Two interpretation functions representing optional exhaustification.

• literal : Interp
• exhaustified : Interp

instance RSA.FreeChoice.instDecidableEqInterp : DecidableEq Interp

Equations

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

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

Equations

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

instance RSA.FreeChoice.instBEqInterp : BEq Interp

Equations

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

instance RSA.FreeChoice.instReprInterp : Repr Interp

Equations

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

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

Equations

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

def RSA.FreeChoice.instInhabitedInterp.default : Interp

Equations

• RSA.FreeChoice.instInhabitedInterp.default = RSA.FreeChoice.Interp.literal

instance RSA.FreeChoice.instInhabitedInterp : Inhabited Interp

Equations

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

instance RSA.FreeChoice.instFintypeInterp : Fintype Interp

Equations

• RSA.FreeChoice.instFintypeInterp = { elems := {RSA.FreeChoice.Interp.literal, RSA.FreeChoice.Interp.exhaustified}, complete := RSA.FreeChoice.instFintypeInterp._proof_1 }

def RSA.FreeChoice.hasFCI : FCState → Bool

Free choice inference: each item is individually permitted. ◇(A∧¬B) ∧ ◇(B∧¬A). True at {onlyOne, anyNumber}.

Equations

• RSA.FreeChoice.hasFCI RSA.FreeChoice.FCState.onlyOne = true
• RSA.FreeChoice.hasFCI RSA.FreeChoice.FCState.anyNumber = true
• RSA.FreeChoice.hasFCI x✝ = false

def RSA.FreeChoice.hasEI : FCState → Bool

Exclusivity inference: taking both is not permitted. ¬◇(A∧B). True at {onlyA, onlyB, onlyOne}.

Equations

• RSA.FreeChoice.hasEI RSA.FreeChoice.FCState.onlyA = true
• RSA.FreeChoice.hasEI RSA.FreeChoice.FCState.onlyB = true
• RSA.FreeChoice.hasEI RSA.FreeChoice.FCState.onlyOne = true
• RSA.FreeChoice.hasEI x✝ = false

def RSA.FreeChoice.I1 : Utterance → FCState → Bool

Interpretation function I₁ (literal/unexhaustified) from (6).

• ⟦A⟧^I₁ = {Only A, Only One, Any Number, Only Both}
• ⟦B⟧^I₁ = {Only B, Only One, Any Number, Only Both}
• ⟦Or⟧^I₁ = all 5 states
• ⟦And⟧^I₁ = {Any Number, Only Both}

Equations

• RSA.FreeChoice.I1 RSA.FreeChoice.Utterance.a RSA.FreeChoice.FCState.onlyB = false
• RSA.FreeChoice.I1 RSA.FreeChoice.Utterance.a x✝ = true
• RSA.FreeChoice.I1 RSA.FreeChoice.Utterance.b RSA.FreeChoice.FCState.onlyA = false
• RSA.FreeChoice.I1 RSA.FreeChoice.Utterance.b x✝ = true
• RSA.FreeChoice.I1 RSA.FreeChoice.Utterance.or_ x✝ = true
• RSA.FreeChoice.I1 RSA.FreeChoice.Utterance.and_ RSA.FreeChoice.FCState.anyNumber = true
• RSA.FreeChoice.I1 RSA.FreeChoice.Utterance.and_ RSA.FreeChoice.FCState.onlyBoth = true
• RSA.FreeChoice.I1 RSA.FreeChoice.Utterance.and_ x✝ = false

def RSA.FreeChoice.I2 : Utterance → FCState → Bool

Interpretation function I₂ (exhaustified) from (7). Strengthened via innocent exclusion:

• ⟦A⟧^I₂ = {Only A}
• ⟦B⟧^I₂ = {Only B}
• ⟦Or⟧^I₂ = {Only A, Only B, Only One, Any Number}
• ⟦And⟧^I₂ = {Only Both}

Equations

• RSA.FreeChoice.I2 RSA.FreeChoice.Utterance.a RSA.FreeChoice.FCState.onlyA = true
• RSA.FreeChoice.I2 RSA.FreeChoice.Utterance.a x✝ = false
• RSA.FreeChoice.I2 RSA.FreeChoice.Utterance.b RSA.FreeChoice.FCState.onlyB = true
• RSA.FreeChoice.I2 RSA.FreeChoice.Utterance.b x✝ = false
• RSA.FreeChoice.I2 RSA.FreeChoice.Utterance.or_ RSA.FreeChoice.FCState.onlyBoth = false
• RSA.FreeChoice.I2 RSA.FreeChoice.Utterance.or_ x✝ = true
• RSA.FreeChoice.I2 RSA.FreeChoice.Utterance.and_ RSA.FreeChoice.FCState.onlyBoth = true
• RSA.FreeChoice.I2 RSA.FreeChoice.Utterance.and_ x✝ = false

def RSA.FreeChoice.interpMeaning : Interp → Utterance → FCState → Bool

Combined meaning function indexed by interpretation.

Equations

• RSA.FreeChoice.interpMeaning RSA.FreeChoice.Interp.literal = RSA.FreeChoice.I1
• RSA.FreeChoice.interpMeaning RSA.FreeChoice.Interp.exhaustified = RSA.FreeChoice.I2

theorem RSA.FreeChoice.I2_refines_I1 (u : Utterance) (w : FCState) : I2 u w = true → I1 u w = true

I₂ refines I₁ for all utterances: I₂(u,w) = true → I₁(u,w) = true.

theorem RSA.FreeChoice.I1_or_everywhere (w : FCState) : I1 Utterance.or_ w = true

I₁(Or) is true everywhere (maximally uninformative).

theorem RSA.FreeChoice.I2_or_excludes_onlyBoth : I2 Utterance.or_ FCState.onlyBoth = false ∧ ∀ (w : FCState), w ≠ FCState.onlyBoth → I2 Utterance.or_ w = true

I₂(Or) excludes exactly onlyBoth.

theorem RSA.FreeChoice.I2_a_singleton (w : FCState) : I2 Utterance.a w = true ↔ w = FCState.onlyA

I₂(A) singles out exactly onlyA.

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

@cite{champollion-alsop-grosu-2019} RSA model with semantic uncertainty. Two interpretation functions 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.FreeChoice.uniformCfg : RSAConfig Utterance FCState

Uniform prior: all states equally likely.

Equations

• RSA.FreeChoice.uniformCfg = RSA.FreeChoice.cfg (fun (x : RSA.FreeChoice.FCState) => 1) RSA.FreeChoice.uniformCfg._proof_1

@[reducible, inline]

noncomputable abbrev RSA.FreeChoice.biasedCfg : RSAConfig Utterance FCState

Biased prior: P(anyNumber) = 3, others = 1. Models a context where taking any combination is a priori more likely, testing prior sensitivity of FCI vs EI.

Equations

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

theorem RSA.FreeChoice.fci_derived : uniformCfg.L1_marginal Utterance.or_ hasFCI > uniformCfg.L1_marginal Utterance.or_ fun (w : FCState) => !hasFCI w

FCI is derived: L1 assigns more mass to FCI states (Only One + Any Number) than non-FCI states upon hearing "Or". This is the central result of the paper.

theorem RSA.FreeChoice.fci_robust_to_prior : biasedCfg.L1_marginal Utterance.or_ hasFCI > biasedCfg.L1_marginal Utterance.or_ fun (w : FCState) => !hasFCI w

FCI is robust to prior manipulation: holds even when anyNumber is a priori 3× more likely.

theorem RSA.FreeChoice.ei_uniform : uniformCfg.L1_marginal Utterance.or_ hasEI > uniformCfg.L1_marginal Utterance.or_ fun (w : FCState) => !hasEI w

EI holds under uniform prior.

theorem RSA.FreeChoice.ei_prior_sensitive : ¬biasedCfg.L1_marginal Utterance.or_ hasEI > biasedCfg.L1_marginal Utterance.or_ fun (w : FCState) => !hasEI w

EI is prior-sensitive: a prior biased toward anyNumber defeats EI.

inductive RSA.FreeChoice.Finding : Type

The 4 qualitative findings from @cite{champollion-alsop-grosu-2019}.

• fci_derived : Finding
• fci_robust_to_prior : Finding
• ei_uniform : Finding
• ei_prior_sensitive : Finding

instance RSA.FreeChoice.instDecidableEqFinding : DecidableEq Finding

Equations

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

instance RSA.FreeChoice.instBEqFinding : BEq Finding

Equations

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

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

Equations

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

instance RSA.FreeChoice.instReprFinding : Repr Finding

Equations

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

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

Equations

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

noncomputable def RSA.FreeChoice.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.FreeChoice.all_findings_verified (f : Finding) : formalize f

The RSA model accounts for all 4 findings from @cite{champollion-alsop-grosu-2019}.

The model derives FCI even without the conjunction alternative. This requires either removing the Only Both state or adding a null utterance. We define the null utterance version (Table 8).

inductive RSA.FreeChoice.UtteranceWithNull : Type

Utterances with null option (no conjunction).

• a : UtteranceWithNull
• b : UtteranceWithNull
• or_ : UtteranceWithNull
• null : UtteranceWithNull

instance RSA.FreeChoice.instDecidableEqUtteranceWithNull : DecidableEq UtteranceWithNull

Equations

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

def RSA.FreeChoice.instBEqUtteranceWithNull.beq : UtteranceWithNull → UtteranceWithNull → Bool

Equations

• RSA.FreeChoice.instBEqUtteranceWithNull.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance RSA.FreeChoice.instBEqUtteranceWithNull : BEq UtteranceWithNull

Equations

• RSA.FreeChoice.instBEqUtteranceWithNull = { beq := RSA.FreeChoice.instBEqUtteranceWithNull.beq }

def RSA.FreeChoice.instReprUtteranceWithNull.repr : UtteranceWithNull → ℕ → Std.Format

Equations

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

instance RSA.FreeChoice.instReprUtteranceWithNull : Repr UtteranceWithNull

Equations

• RSA.FreeChoice.instReprUtteranceWithNull = { reprPrec := RSA.FreeChoice.instReprUtteranceWithNull.repr }

def RSA.FreeChoice.instInhabitedUtteranceWithNull.default : UtteranceWithNull

Equations

• RSA.FreeChoice.instInhabitedUtteranceWithNull.default = RSA.FreeChoice.UtteranceWithNull.a

instance RSA.FreeChoice.instInhabitedUtteranceWithNull : Inhabited UtteranceWithNull

Equations

• RSA.FreeChoice.instInhabitedUtteranceWithNull = { default := RSA.FreeChoice.instInhabitedUtteranceWithNull.default }

instance RSA.FreeChoice.instFintypeUtteranceWithNull : Fintype UtteranceWithNull

Equations

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

def RSA.FreeChoice.I1_null : UtteranceWithNull → FCState → Bool

I₁ with null (true everywhere).

Equations

• RSA.FreeChoice.I1_null RSA.FreeChoice.UtteranceWithNull.a RSA.FreeChoice.FCState.onlyB = false
• RSA.FreeChoice.I1_null RSA.FreeChoice.UtteranceWithNull.a x✝ = true
• RSA.FreeChoice.I1_null RSA.FreeChoice.UtteranceWithNull.b RSA.FreeChoice.FCState.onlyA = false
• RSA.FreeChoice.I1_null RSA.FreeChoice.UtteranceWithNull.b x✝ = true
• RSA.FreeChoice.I1_null RSA.FreeChoice.UtteranceWithNull.or_ x✝ = true
• RSA.FreeChoice.I1_null RSA.FreeChoice.UtteranceWithNull.null x✝ = true

def RSA.FreeChoice.I2_null : UtteranceWithNull → FCState → Bool

I₂ with null.

Equations

• RSA.FreeChoice.I2_null RSA.FreeChoice.UtteranceWithNull.a RSA.FreeChoice.FCState.onlyA = true
• RSA.FreeChoice.I2_null RSA.FreeChoice.UtteranceWithNull.a x✝ = false
• RSA.FreeChoice.I2_null RSA.FreeChoice.UtteranceWithNull.b RSA.FreeChoice.FCState.onlyB = true
• RSA.FreeChoice.I2_null RSA.FreeChoice.UtteranceWithNull.b x✝ = false
• RSA.FreeChoice.I2_null RSA.FreeChoice.UtteranceWithNull.or_ RSA.FreeChoice.FCState.onlyBoth = false
• RSA.FreeChoice.I2_null RSA.FreeChoice.UtteranceWithNull.or_ x✝ = true
• RSA.FreeChoice.I2_null RSA.FreeChoice.UtteranceWithNull.null x✝ = true

def RSA.FreeChoice.interpMeaningNull : Interp → UtteranceWithNull → FCState → Bool

Combined meaning for the null-utterance model.

Equations

• RSA.FreeChoice.interpMeaningNull RSA.FreeChoice.Interp.literal = RSA.FreeChoice.I1_null
• RSA.FreeChoice.interpMeaningNull RSA.FreeChoice.Interp.exhaustified = RSA.FreeChoice.I2_null

noncomputable def RSA.FreeChoice.nullCfg : RSAConfig UtteranceWithNull FCState

RSAConfig for the model without conjunction (Table 8). Replaces "and" with a null utterance (true everywhere under both interpretations).

Equations

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

theorem RSA.FreeChoice.fci_without_conjunction : nullCfg.L1_marginal UtteranceWithNull.or_ hasFCI > nullCfg.L1_marginal UtteranceWithNull.or_ fun (w : FCState) => !hasFCI w

FCI is derived even without the conjunction alternative (Tables 7-8). The avoidance mechanism between A/B and Or is sufficient — the conjunction alternative is not essential.

Bridge content (merged from RSA_ChampollionAlsopGrosu2019Bridge.lean)

Bridge: RSA Free Choice Disjunction → Phenomena Data

@cite{champollion-alsop-grosu-2019}

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

Bridge Theorems

• predicts_free_choice: L1 free choice prediction matches data
• fc_not_semantic: Free choice is pragmatic, not semantic

Connection to Empirical Data

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

1. Free Choice Permission (coffeeOrTea):

   • "You may have coffee or tea" → "You may have coffee AND you may have tea"
   • Derived: L1 assigns ~100% to FCI states

2. Exclusivity Cancelability:

   • EI ("not both") is sensitive to world knowledge
   • FCI is robust across priors

3. Ross's Paradox (postOrBurn):

   • "Post the letter" semantically entails "Post or burn"
   • But pragmatically, adding "or burn" triggers free choice
   • The asymmetry comes from the alternative structure

theorem Phenomena.Modality.RSA_ChampollionAlsopGrosu2019Bridge.predicts_free_choice : FreeChoice.coffeeOrTea.isPragmaticInference = true

Free choice is predicted

theorem Phenomena.Modality.RSA_ChampollionAlsopGrosu2019Bridge.fc_not_semantic : FreeChoice.coffeeOrTea.isSemanticEntailment = false

The inference is not semantic