Free Choice: Theory Comparison

@cite{aloni-2022} @cite{alsop-2024} @cite{bar-lev-fox-2020} @cite{champollion-alsop-grosu-2019} @cite{elliott-2025} @cite{fox-2007}

Comparing how different theories derive free choice inferences.

The Puzzle

"You may have coffee or tea" pragmatically implies: "You may have coffee AND you may have tea"

Semantically: ◇(A ∨ B) ↔ ◇A ∨ ◇B (standard modal logic) Pragmatically: ◇(A ∨ B) → ◇A ∧ ◇B (free choice!)

Theories Compared

1. @cite{fox-2007}: Double exhaustification (Exh²) with Innocent Exclusion
2. @cite{bar-lev-fox-2020}: Innocent Inclusion (II) + Innocent Exclusion (IE)
3. @cite{champollion-alsop-grosu-2019}: RSA with semantic uncertainty (disjunction)
4. @cite{alsop-2024}: RSA with Global Intentions (universal any)
5. @cite{aloni-2022}: BSML - Bilateral State-based Modal Logic (team semantics)
6. @cite{elliott-sudo-2025}: BUS - Bilateral Update Semantics (dynamic)

The Core Puzzle

Standard modal logic gives us: ◇(A ∨ B) ↔ ◇A ∨ ◇B

But pragmatically, we infer: ◇(A ∨ B) → ◇A ∧ ◇B

This is not a semantic entailment. The challenge is to derive it pragmatically.

Two Related Inferences

1. Free Choice Inference (FCI): ◇(A ∨ B) → ◇A ∧ ◇B

   • "You may have coffee or tea" → "You may have coffee" AND "You may have tea"

2. Exclusivity Inference (EI): ◇(A ∨ B) → ¬◇(A ∧ B)

   • "You may have coffee or tea" → "You may not have both"

FCI is robust; EI is cancelable. Any theory must explain this asymmetry.

theorem Comparisons.FreeChoice.fci_is_pragmatic : Phenomena.Modality.FreeChoice.coffeeOrTea.isSemanticEntailment = false

FCI is a pragmatic inference, not semantic

theorem Comparisons.FreeChoice.fci_is_captured : Phenomena.Modality.FreeChoice.coffeeOrTea.isPragmaticInference = true

FCI is captured pragmatically

@cite{fox-2007}: Free Choice via Recursive Exhaustification

The original grammatical account: recursive application of exh (the covert exhaustivity operator) derives FC without Innocent Inclusion.

• Layer 1: Exh(C)(◇(p∨q)) = ◇(p∨q) ∧ ¬◇(p∧q)
• Layer 2: Exh²(◇(p∨q)) = ◇p ∧ ◇q ∧ ¬◇(p∧q) — free choice!

See Exhaustivity/Fox2007.lean for the computable algorithm and full derivation.

theorem Comparisons.FreeChoice.fox2007_derives_fc (w : NeoGricean.Exhaustivity.Fox2007.ModalW) : NeoGricean.Exhaustivity.Fox2007.exhB NeoGricean.Exhaustivity.Fox2007.mDomain NeoGricean.Exhaustivity.Fox2007.layer2Alts NeoGricean.Exhaustivity.Fox2007.layer1Result w = (NeoGricean.Exhaustivity.Fox2007.diamP w && NeoGricean.Exhaustivity.Fox2007.diamQ w && !NeoGricean.Exhaustivity.Fox2007.diamPandQ w)

Fox 2007: FC is derived via double exhaustification (Exh²). Re-exports the verified computation from Fox2007.lean.

Neo-Gricean Account: Innocent Inclusion

@cite{bar-lev-fox-2020} extend @cite{fox-2007}'s Innocent Exclusion with Innocent Inclusion.

The Mechanism

Step 1: Innocent Exclusion (IE)

• Find maximal sets of alternatives that can consistently be assigned FALSE
• An alternative is in IE if it's in ALL such maximal sets

Step 2: Innocent Inclusion (II)

• After IE, find maximal sets that can consistently be assigned TRUE
• An alternative is in II if it's in ALL such maximal sets

Step 3: Combined Exhaustification Exh^{IE+II}(φ) = φ ∧ ∀q ∈ IE[¬q] ∧ ∀r ∈ II[r]

Why It Works for Free Choice

The key is closure under conjunction:

Alternative Set	Closed under ∧?	Result
{a∨b, a, b, a∧b}	YES	Exclusive-or
{◇(a∨b), ◇a, ◇b, ◇(a∧b)}	NO	Free choice

For FC alternatives:

• ◇a ∧ ◇b ≠ ◇(a ∧ b) in modal logic
• This non-closure allows II to include ◇a and ◇b

theorem Comparisons.FreeChoice.barlevfox_derives_fc (w : NeoGricean.FreeChoice.FCWorld) : NeoGricean.Exhaustivity.exhIEII NeoGricean.FreeChoice.fcALT NeoGricean.FreeChoice.fcPrejacent w → NeoGricean.FreeChoice.permA w ∧ NeoGricean.FreeChoice.permB w

Bar-Lev & Fox: Free choice is derived via Innocent Inclusion

RSA Account: Semantic Uncertainty

@cite{champollion-alsop-grosu-2019} use RSA with multiple interpretation functions (following @cite{bergen-levy-goodman-2016}'s lexical uncertainty).

The Mechanism

Two Interpretation Functions:

• I₁ (literal): Standard modal logic meanings
• I₂ (exhaustified): Strengthened meanings (à @cite{fox-2007})

For "You may A":

• Under I₁: {Only A, Only One, Any Number, Only Both}
• Under I₂: {Only A} only (exhaustified to exclude others)

The Derivation:

1. Speaker wants to convey "Only One" (you may choose either)
2. If speaker says "You may A", hearer might use I₂ → "Only A"
3. To avoid this, speaker uses "You may A or B"
4. Hearer reasons: "Speaker avoided A to prevent me thinking Only A"
5. Hearer concludes: Must be Only One or Any Number → FCI!

Insight

The semantic uncertainty creates an avoidance pattern:

• Disjuncts are "risky" (might be interpreted exclusively)
• Disjunction is "safe" (always allows both options)

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

Champollion et al.: L1 assigns majority probability to FCI states for Or.

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

Champollion et al.: FCI is robust to prior manipulation.

RSA Account for Universal Any: Global Intentions

@cite{alsop-2024} extends the RSA approach to universal free choice items like any, using the Global Intentions model from @cite{franke-bergen-2020}.

The Mechanism

Two Parses (instead of two interpretation functions):

• Szabolcsi parse (weak): ∃x[◇take(x)] - "some option is permitted"
• Dayal parse (strong): ∀x[◇take(x)] - "each option is permitted"

The Derivation:

1. Speaker wants to convey "you may take any (= each) class"
2. If speaker uses weak parse, hearer might only infer "some class is OK"
3. To be informative, speaker intends the strong (Dayal) parse
4. Hearer reasons: "Speaker chose 'any' with the strong parse"
5. Hearer concludes: Each class is individually permitted → Exclusiveness!

Key Parallel to Champollion et al.

Aspect	Disjunction (@cite{champollion-alsop-grosu-2019})	Universal any (2024)
FC inference	◇(a∨b) → ◇a ∧ ◇b	◇∃x.P(x) → ∀x.◇P(x)
Robust inference	FCI	Exclusiveness
Prior-sensitive	EI (not-both)	Not-every
Ambiguity	Interpretation (I₁/I₂)	Parse (Szabolcsi/Dayal)

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

Alsop: L1 assigns majority probability to exclusiveness states for "may any".

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

Alsop: Exclusiveness is robust to prior manipulation.

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

Alsop: Not-every is prior-sensitive (unlike exclusiveness).

Semantic Account: BSML (Bilateral State-based Modal Logic)

@cite{aloni-2022} derives FC semantically using team semantics.

The Mechanism

Split Disjunction: t ⊨ φ ∨ ψ iff ∃t₁,t₂: t₁ ∪ t₂ = t ∧ t₁ ⊨ φ ∧ t₂ ⊨ ψ

Non-emptiness Enrichment: [φ]⁺ adds NE constraints recursively

FC Derivation:

1. [◇(α ∨ β)]⁺ = ◇([α]⁺ ∨ [β]⁺) ∧ NE
2. Split disjunction partitions the team
3. [α]⁺ and [β]⁺ both include NE, so both parts must be non-empty
4. Therefore ◇α and ◇β are both supported

theorem Comparisons.FreeChoice.aloni_dne {W : Type u_1} [DecidableEq W] (M : Semantics.Dynamic.BSML.BSMLModel W) (φ : Semantics.Dynamic.BSML.BSMLFormula) (t : Semantics.Dynamic.TeamSemantics.Team W) : Semantics.Dynamic.BSML.support M φ.neg.neg t = Semantics.Dynamic.BSML.support M φ t

Aloni BSML: DNE holds definitionally

Semantic Account: BUS (Bilateral Update Semantics)

@cite{elliott-sudo-2025} derive FC semantically using dynamic bilateral updates.

The Mechanism

Modal Disjunction Precondition: s[φ ∨ ψ]⁺ = s[φ ∨ ψ]⁺ if s[φ ∨ ψ]⁺₁ ≠ ∅ AND s[φ ∨ ψ]⁺₂ ≠ ∅, else ∅

FC Derivation:

1. For ◇(φ ∨ ψ) to be possible, positive update must be non-empty
2. This requires BOTH disjuncts to contribute possibilities
3. Therefore ◇φ and ◇ψ are both possible

Key Advantage: Cross-Disjunct Anaphora

BUS is uniquely designed to handle "bathroom disjunctions":

• "Either there's no bathroom or it's in a funny place"
• The pronoun "it" is bound by the existential under negation
• DNE (from bilateral structure) enables this binding

Elliott & Sudo FC is derived from modal disjunction semantics. The BUS module provides FC derivation via:

• fc_semantic_first_disjunct: ◇(φ ∨ ψ) → ◇φ
• fc_semantic_second_disjunct: ◇(φ ∨ ψ) → ψ possible after ¬φ
• dual_prohibition: ¬◇φ ∧ ¬◇ψ → ¬◇(φ ∨ ψ)

Side-by-Side Comparison

Aspect	Bar-Lev & Fox	Champollion et al.	Alsop	Aloni	E&S
Framework	Neo-Gricean	RSA	RSA	Team Sem	Dynamic
Type	Pragmatic	Pragmatic	Pragmatic	Semantic	Semantic
Key mechanism	Innocent Inclusion	Semantic uncertainty	Parse ambiguity	NE + split ∨	Modal ∨ precond
Nature	Categorical	Probabilistic	Probabilistic	Categorical	Categorical
Anaphora	No	No	No	No	Yes
Why FC works	Non-closure	Avoid I₂	Dayal informative	NE forces both	Both contribute

structure Comparisons.FreeChoice.TheoryComparison : Type

Comparison result type (extended for all theories)

• phenomenon : String
• barlevfox : String
• champollion : String
• alsop : String
• aloni : String
• elliottSudo : String
• allAgree : Bool

def Comparisons.FreeChoice.instReprTheoryComparison.repr : TheoryComparison → ℕ → Std.Format

Equations

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

instance Comparisons.FreeChoice.instReprTheoryComparison : Repr TheoryComparison

Equations

• Comparisons.FreeChoice.instReprTheoryComparison = { reprPrec := Comparisons.FreeChoice.instReprTheoryComparison.repr }

def Comparisons.FreeChoice.fciComparison : TheoryComparison

FCI: All theories derive it

Equations

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

def Comparisons.FreeChoice.dualProhibitionComparison : TheoryComparison

Dual Prohibition: Negation blocks FC

Equations

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

def Comparisons.FreeChoice.secondaryInference : TheoryComparison

Secondary inference asymmetry

Equations

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

def Comparisons.FreeChoice.anaphoraComparison : TheoryComparison

Cross-disjunct anaphora

Equations

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

def Comparisons.FreeChoice.allComparisons : List TheoryComparison

All comparisons

Equations

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

Pragmatic vs Semantic Derivation

A key division among FC theories:

Pragmatic Approaches (FC as implicature)

• Bar-Lev & Fox: Exhaustification with Innocent Inclusion
• Champollion et al.: RSA reasoning about interpretation uncertainty
• Alsop: RSA reasoning about parse ambiguity

Semantic Approaches (FC built into meaning)

• Aloni (BSML): Split disjunction + non-emptiness enrichment
• Elliott & Sudo (BUS): Modal disjunction precondition

Trade-offs

Aspect	Pragmatic	Semantic
FC source	Reasoning about alternatives	Lexical meaning
Cancelability	Predicted (pragmatic)	Must be stipulated
Gradient	RSA: yes; Neo-Gricean: no	No
Cross-disjunct anaphora	Hard to capture	BUS: natural
Dual prohibition	Requires explanation	Built in

inductive Comparisons.FreeChoice.ApproachType : Type

Approach classification

• pragmatic : ApproachType
• semantic : ApproachType

instance Comparisons.FreeChoice.instDecidableEqApproachType : DecidableEq ApproachType

Equations

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

def Comparisons.FreeChoice.instBEqApproachType.beq : ApproachType → ApproachType → Bool

Equations

• Comparisons.FreeChoice.instBEqApproachType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Comparisons.FreeChoice.instBEqApproachType : BEq ApproachType

Equations

• Comparisons.FreeChoice.instBEqApproachType = { beq := Comparisons.FreeChoice.instBEqApproachType.beq }

instance Comparisons.FreeChoice.instReprApproachType : Repr ApproachType

Equations

• Comparisons.FreeChoice.instReprApproachType = { reprPrec := Comparisons.FreeChoice.instReprApproachType.repr }

def Comparisons.FreeChoice.instReprApproachType.repr : ApproachType → ℕ → Std.Format

Equations

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

def Comparisons.FreeChoice.theoryApproach : String → ApproachType

Classify theories by approach

Equations

• Comparisons.FreeChoice.theoryApproach "Bar-Lev & Fox 2020" = Comparisons.FreeChoice.ApproachType.pragmatic
• Comparisons.FreeChoice.theoryApproach "Champollion et al. 2019" = Comparisons.FreeChoice.ApproachType.pragmatic
• Comparisons.FreeChoice.theoryApproach "Alsop 2024" = Comparisons.FreeChoice.ApproachType.pragmatic
• Comparisons.FreeChoice.theoryApproach "Aloni 2022" = Comparisons.FreeChoice.ApproachType.semantic
• Comparisons.FreeChoice.theoryApproach "Elliott & Sudo 2025" = Comparisons.FreeChoice.ApproachType.semantic
• Comparisons.FreeChoice.theoryApproach x✝ = Comparisons.FreeChoice.ApproachType.pragmatic

Different Structural Insights

Bar-Lev & Fox: Closure Under Conjunction

The key structural property is whether the alternative set is closed under ∧.

Simple disjunction: ALT = {a∨b, a, b, a∧b}

• a ∧ b IS in ALT
• Closed → IE excludes everything, II includes nothing
• Result: Exclusive-or (or contradiction)

FC disjunction: ALT = {◇(a∨b), ◇a, ◇b, ◇(a∧b)}

• ◇a ∧ ◇b is NOT equivalent to ◇(a∧b)
• Not closed → IE excludes ◇(a∧b), II includes ◇a, ◇b
• Result: Free choice!

Aloni: Non-Emptiness + Split Disjunction

The key is that disjunction SPLITS the team: t ⊨ φ ∨ ψ iff ∃t₁,t₂: t₁ ∪ t₂ = t ∧ t₁ ⊨ φ ∧ t₂ ⊨ ψ

Combined with pragmatic enrichment adding NE: [φ ∨ ψ]⁺ = ([φ]⁺ ∨ [ψ]⁺) ∧ NE

Each part of the partition must be non-empty → both disjuncts possible!

Elliott & Sudo: Bilateral + Precondition

Modal disjunction has a PRECONDITION requiring both disjuncts contribute: s[φ ∨ ψ]⁺ = s[φ ∨ ψ]⁺ if s[φ ∨ ψ]⁺₁ ≠ ∅ AND s[φ ∨ ψ]⁺₂ ≠ ∅, else ∅

This SEMANTICALLY derives FC: if the disjunction is assertable, both must contribute possibilities.

inductive Comparisons.FreeChoice.ClosureStatus : Type

Bar-Lev & Fox: closure under conjunction determines outcome.

• closed : ClosureStatus
• notClosed : ClosureStatus

instance Comparisons.FreeChoice.instDecidableEqClosureStatus : DecidableEq ClosureStatus

Equations

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

instance Comparisons.FreeChoice.instBEqClosureStatus : BEq ClosureStatus

Equations

• Comparisons.FreeChoice.instBEqClosureStatus = { beq := Comparisons.FreeChoice.instBEqClosureStatus.beq }

def Comparisons.FreeChoice.instBEqClosureStatus.beq : ClosureStatus → ClosureStatus → Bool

Equations

• Comparisons.FreeChoice.instBEqClosureStatus.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Comparisons.FreeChoice.instReprClosureStatus.repr : ClosureStatus → ℕ → Std.Format

Equations

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

instance Comparisons.FreeChoice.instReprClosureStatus : Repr ClosureStatus

Equations

• Comparisons.FreeChoice.instReprClosureStatus = { reprPrec := Comparisons.FreeChoice.instReprClosureStatus.repr }

def Comparisons.FreeChoice.closurePrediction : ClosureStatus → String

Prediction based on closure

Equations

• Comparisons.FreeChoice.closurePrediction Comparisons.FreeChoice.ClosureStatus.closed = "Exclusive-or (standard scalar implicature)"
• Comparisons.FreeChoice.closurePrediction Comparisons.FreeChoice.ClosureStatus.notClosed = "Free choice (via Innocent Inclusion)"

def Comparisons.FreeChoice.simpleDisjunctionClosure : ClosureStatus

Simple disjunction is closed

Equations

• Comparisons.FreeChoice.simpleDisjunctionClosure = Comparisons.FreeChoice.ClosureStatus.closed

def Comparisons.FreeChoice.fcDisjunctionClosure : ClosureStatus

FC disjunction is not closed

Equations

• Comparisons.FreeChoice.fcDisjunctionClosure = Comparisons.FreeChoice.ClosureStatus.notClosed

Where Theories Make Different Predictions

1. Gradient vs Categorical Judgments

Pragmatic (RSA): FCI is gradient (probability varies with α, priors) Pragmatic (Neo-Gricean): FCI is categorical Semantic: FCI is categorical (semantic entailment)

Test: Do speakers show gradient acceptance of FC readings?

2. EI Cancelability Asymmetry

Bar-Lev & Fox: Both FCI and EI derived by same mechanism Champollion et al.: FCI from reasoning, EI from priors → asymmetry Semantic: Must explain cancelability differently

3. Cross-Disjunct Anaphora

Most theories: Cannot handle "Either there's no bathroom or it's upstairs" Elliott & Sudo: Primary motivation; handles via bilateral + DNE

structure Comparisons.FreeChoice.EmpiricalPrediction : Type

Empirical prediction type

• test : String
• pragmaticRSA : String
• pragmaticNG : String
• semantic : String
• testable : Bool

def Comparisons.FreeChoice.instReprEmpiricalPrediction.repr : EmpiricalPrediction → ℕ → Std.Format

Equations

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

instance Comparisons.FreeChoice.instReprEmpiricalPrediction : Repr EmpiricalPrediction

Equations

• Comparisons.FreeChoice.instReprEmpiricalPrediction = { reprPrec := Comparisons.FreeChoice.instReprEmpiricalPrediction.repr }

def Comparisons.FreeChoice.gradientPrediction : EmpiricalPrediction

Equations

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

def Comparisons.FreeChoice.eiAsymmetryPrediction : EmpiricalPrediction

Equations

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

def Comparisons.FreeChoice.anaphoraPrediction : EmpiricalPrediction

Equations

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

def Comparisons.FreeChoice.empiricalPredictions : List EmpiricalPrediction

Equations

• Comparisons.FreeChoice.empiricalPredictions = [Comparisons.FreeChoice.gradientPrediction, Comparisons.FreeChoice.eiAsymmetryPrediction, Comparisons.FreeChoice.anaphoraPrediction]

Predictions for Phenomena Data

All theories correctly predict the patterns in Phenomena.FreeChoice.Data:

Basic Free Choice (coffeeOrTea)

• Input: "You may have coffee or tea"
• Output: "You may have coffee AND you may have tea"
• All: ✓ Derived

Ross's Paradox (postOrBurn)

• "Post the letter" ⊢ "Post or burn" (semantically)
• But "Post or burn" → "You may burn" (pragmatically via FC)
• All: ✓ Explained

Modal Free Choice (deonticFC, epistemicFC, abilityFC)

• FC works with different modal flavors
• All: ✓ Predicted (mechanism is general)

Cancellation (explicitCancellation)

• "You may have A or B, but I don't know which"
• Pragmatic: ✓ Predicted (defeasible)
• Semantic: Must add mechanism for cancellation

def Comparisons.FreeChoice.allPredictBasicFC : Bool

All phenomena are correctly predicted by all theories

Equations

• Comparisons.FreeChoice.allPredictBasicFC = Phenomena.Modality.FreeChoice.coffeeOrTea.isPragmaticInference

def Comparisons.FreeChoice.allPredictRoss : Bool

Equations

• Comparisons.FreeChoice.allPredictRoss = decide (Phenomena.Modality.FreeChoice.postOrBurn.pragmaticallyFelicitous = false)

def Comparisons.FreeChoice.allPredictCancellation : Bool

Equations

• Comparisons.FreeChoice.allPredictCancellation = Phenomena.Modality.FreeChoice.explicitCancellation.felicitous

Summary: Free Choice Theory Landscape

Five Theories, Two Approaches

Pragmatic (FC as implicature):

• @cite{bar-lev-fox-2020}: Innocent Inclusion (categorical)
• @cite{champollion-alsop-grosu-2019}: RSA + interpretation uncertainty (gradient)
• @cite{alsop-2024}: RSA + parse ambiguity (gradient)

Semantic (FC in meaning):

• @cite{aloni-2022}: BSML - team semantics + NE enrichment
• @cite{elliott-sudo-2025}: BUS - bilateral dynamics + modal ∨ precondition

Key Differentiators

Feature	Best Theory
Gradient judgments	RSA approaches
EI asymmetry	RSA approaches
Formal precision	Bar-Lev & Fox
Cross-disjunct anaphora	Elliott & Sudo
Static team semantics	Aloni

Complementary Insights

Each theory contributes something unique:

• Bar-Lev & Fox: WHY closure under ∧ matters
• Champollion et al.: HOW reasoning produces gradient judgments
• Alsop: Extension to universal FCIs (any)
• Aloni: Static team-semantic alternative to dynamics
• Elliott & Sudo: Anaphora + bilateral structure