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} @cite{holliday-mandelkern-2024}
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 #
- @cite{fox-2007}: Double exhaustification (Exh²) with Innocent Exclusion
- @cite{bar-lev-fox-2020}: Innocent Inclusion (II) + Innocent Exclusion (IE)
- @cite{champollion-alsop-grosu-2019}: RSA with semantic uncertainty (disjunction)
- @cite{alsop-2024}: RSA with Global Intentions (universal any)
- @cite{aloni-2022}: BSML - Bilateral State-based Modal Logic (team semantics)
- @cite{elliott-sudo-2025}: BUS - Bilateral Update Semantics (dynamic)
- @cite{holliday-mandelkern-2024}: Possibility semantics (ortholattice algebra)
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 #
Free Choice Inference (FCI): ◇(A ∨ B) → ◇A ∧ ◇B
- "You may have coffee or tea" → "You may have coffee" AND "You may have tea"
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.
FCI is a pragmatic inference, not semantic
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 Exhaustification/InnocentExclusion.lean for the computable algorithm and
full derivation.
Fox 2007: FC is derived via double exhaustification (Exh²).
Re-exports the verified computation from InnocentExclusion.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
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:
- Speaker wants to convey "Only One" (you may choose either)
- If speaker says "You may A", hearer might use I₂ → "Only A"
- To avoid this, speaker uses "You may A or B"
- Hearer reasons: "Speaker avoided A to prevent me thinking Only A"
- 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)
Champollion et al.: L1 assigns majority probability to FCI states for Or.
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:
- Speaker wants to convey "you may take any (= each) class"
- If speaker uses weak parse, hearer might only infer "some class is OK"
- To be informative, speaker intends the strong (Dayal) parse
- Hearer reasons: "Speaker chose 'any' with the strong parse"
- 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) |
Alsop: L1 assigns majority probability to exclusiveness states for "may any".
Alsop: Exclusiveness is robust to prior manipulation.
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:
- [◇(α ∨ β)]⁺ = ◇([α]⁺ ∨ [β]⁺) ∧ NE
- Split disjunction partitions the team
- [α]⁺ and [β]⁺ both include NE, so both parts must be non-empty
- Therefore ◇α and ◇β are both supported
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:
- For ◇(φ ∨ ψ) to be possible, positive update must be non-empty
- This requires BOTH disjuncts to contribute possibilities
- 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: ¬◇φ ∧ ¬◇ψ → ¬◇(φ ∨ ψ)
Algebraic Account: Possibility Semantics (Ortholattice) #
@cite{holliday-mandelkern-2024} provide a structural account of free choice rooted in the algebra of propositions. In possibility semantics, propositions form an ortholattice — validated by excluded middle and non-contradiction, but NOT by distributivity. A partial possibility can verify A ∨ B without verifying either disjunct, because disjunction is De Morgan (A ∨ B = ¬(¬A ∧ ¬B)), weaker than set-theoretic union.
The Mechanism #
Free choice selective validity: ◇(A ∨ B) → ◇A ∧ ◇B holds for propositions in the image of the Boolean embedding (Proposition 5.12.3), but fails when the ortholattice is genuinely non-Boolean.
In the 5-point epistemic scale:
- At x₃ (full uncertainty), FC holds: both p and ¬p are accessible
- At x₁ (knows p), FC fails: ◇(p ∨ ¬p) is true but ◇¬p is false
Key Difference #
This is neither pragmatic (reasoning about alternatives) nor dynamic
(update semantics) — it's algebraic. Free choice depends on whether
the proposition space is Boolean. Standard modal logic (all possibilities
are worlds, compat = identity) is the special case where the algebra is
Boolean and FC holds universally (via diamond_eq_kripkeEval_classical).
Holliday & Mandelkern: FC holds at full uncertainty (x₃).
Holliday & Mandelkern: FC FAILS at knowledge (x₁). The non-Boolean ortholattice selectively blocks FC where the agent's epistemic state rules out one disjunct.
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 |
Equations
- One or more equations did not get rendered due to their size.
Instances For
FCI: All theories derive it
Equations
- One or more equations did not get rendered due to their size.
Instances For
Dual Prohibition: Negation blocks FC
Equations
- One or more equations did not get rendered due to their size.
Instances For
Secondary inference asymmetry
Equations
- One or more equations did not get rendered due to their size.
Instances For
Cross-disjunct anaphora
Equations
- One or more equations did not get rendered due to their size.
Instances For
All comparisons
Equations
- One or more equations did not get rendered due to their size.
Instances For
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 |
Equations
- One or more equations did not get rendered due to their size.
Instances For
Classify theories by approach
Equations
- Phenomena.Modality.FreeChoiceCompare.theoryApproach "Bar-Lev & Fox 2020" = Phenomena.Modality.FreeChoiceCompare.ApproachType.pragmatic
- Phenomena.Modality.FreeChoiceCompare.theoryApproach "Champollion et al. 2019" = Phenomena.Modality.FreeChoiceCompare.ApproachType.pragmatic
- Phenomena.Modality.FreeChoiceCompare.theoryApproach "Alsop 2024" = Phenomena.Modality.FreeChoiceCompare.ApproachType.pragmatic
- Phenomena.Modality.FreeChoiceCompare.theoryApproach "Aloni 2022" = Phenomena.Modality.FreeChoiceCompare.ApproachType.semantic
- Phenomena.Modality.FreeChoiceCompare.theoryApproach "Elliott & Sudo 2025" = Phenomena.Modality.FreeChoiceCompare.ApproachType.semantic
- Phenomena.Modality.FreeChoiceCompare.theoryApproach x✝ = Phenomena.Modality.FreeChoiceCompare.ApproachType.pragmatic
Instances For
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.
Bar-Lev & Fox: closure under conjunction determines outcome.
- closed : ClosureStatus
- notClosed : ClosureStatus
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Prediction based on closure
Equations
- Phenomena.Modality.FreeChoiceCompare.closurePrediction Phenomena.Modality.FreeChoiceCompare.ClosureStatus.closed = "Exclusive-or (standard scalar implicature)"
- Phenomena.Modality.FreeChoiceCompare.closurePrediction Phenomena.Modality.FreeChoiceCompare.ClosureStatus.notClosed = "Free choice (via Innocent Inclusion)"
Instances For
Simple disjunction is closed
Equations
Instances For
FC disjunction is not closed
Equations
Instances For
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
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
All phenomena are correctly predicted by all theories
Equations
Instances For
Summary: Free Choice Theory Landscape #
Seven Theories, Three 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
Algebraic (FC from proposition structure):
- @cite{holliday-mandelkern-2024}: Possibility semantics — FC holds when the proposition algebra is Boolean, fails in non-Boolean ortholattices
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 |
| Why FC fails selectively | Holliday & Mandelkern |
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
- Holliday & Mandelkern: WHEN FC holds (Boolean algebra) vs fails (ortholattice)