@cite{delpinal-bassi-sauerland-2024} — Free Choice and Presuppositional Exhaustification #
@cite{delpinal-bassi-sauerland-2024} @cite{bassi-delpinal-sauerland-2021}
"Free choice and presuppositional exhaustification" Semantics & Pragmatics 17, Article 3: 1–52.
Core Contribution #
pex^{IE+II} (presuppositional exhaustification) derives free choice by splitting the output of exhaustification into assertive and presuppositional components:
- asserts: the prejacent φ
- presupposes: negation of IE alternatives + homogeneity over II alternatives
This structural split solves embedded FC puzzles that flat exh cannot:
- §2: Basic FC, double prohibition, negative FC (from local pex)
- §3: Presupposed FC under negative factives ("Noah is unaware...")
- §4: Filtering FC in disjunction ("Either Maria can't... or she can...")
- §5: FC under universal, existential, and non-monotonic quantifiers
Architecture #
The core operator pexIEII is defined in
Theories/Semantics/Exhaustification/Presuppositional.lean.
This file connects pex to empirical free choice data and formalizes the
embedding puzzles from §3–§5.
Bridge to Phenomena #
pex predicts that free choice is a pragmatic inference (derived by the
covert operator pex), not a semantic entailment. This matches the empirical
data in Phenomena.FreeChoice.
§2.2: pex Applied to ◇(p ∨ q) #
Instantiating pexIEII_full on the five-world FC toy from
Phenomena.Modality.Studies.BarLevFox2020:
- φ = ◇(p ∨ q) =
permAorB=fcPrejacent - ALT = {◇(p ∨ q), ◇p, ◇q, ◇(p ∧ q)} =
fcALT - IE = {◇(p ∧ q)}
- II = {◇p, ◇q}
pex^{IE+II}[◇(p ∨ q)]: asserts: ◇(p ∨ q) presupposes: ¬◇(p ∧ q) ∧ (◇p ↔ ◇q)
Since ◇(p ∨ q) ∧ (◇p ↔ ◇q) entails ◇p ∧ ◇q, pex derives FC.
The pex output for free choice: pex^{IE+II}[◇(p ∨ q)].
Equations
Instances For
FC via pex: when presupposition and assertion hold, we get ◇p ∧ ◇q.
This is the paper's (14)–(15): ⟦pex^{IE+II}[◇[p ∨ q]]⟧ = ◇(p ∨ q)_{◇p↔◇q} ⊨ ◇p ∧ ◇q
The proof uses mem_II_of_cell_witness: separatelyAB is the cell
witness for fcALT (verified in BarLevFox2020.separatelyAB_in_cell),
and both permA and permB hold at separatelyAB.
Double prohibition: the negated pex output entails ¬◇p ∧ ¬◇q.
This is the paper's (16): ⟦¬[pex^{IE+II}[◇[T ∨ B]]]⟧ = ¬◇(T ∨ B)_{◇T↔◇B} ⊨ ¬◇T ∧ ¬◇B
Negative FC via pex: the ¬□ ↔ ◇ duality #
The alternative set for ¬□(p∧q) is {¬□(p∧q), ¬□p, ¬□q, ¬□(p∨q)}, which is isomorphic to the ◇∨ alternative set under the mapping:
| ¬□ world | ◇ world | Reinterpretation |
|---|---|---|
| ¬□(p∧q) | ◇(a∨b) | notReqAandB = fcPrejacent |
| ¬□p | ◇b | notReqA = permB |
| ¬□q | ◇a | notReqB = permA |
| ¬□(p∨q) | ◇(a∧b) | notReqAorB = permAandB |
Consequently, pexFC simultaneously derives both positive FC (◇a ∧ ◇b)
and negative FC (¬□p ∧ ¬□q) under reinterpretation.
¬□p: p is not required (= ◇¬p by duality). Under the isomorphism, this
is permB on FCWorld.
Instances For
¬□q: q is not required. Under the isomorphism, this is permA.
Instances For
¬□(p∧q): not both required. Under the isomorphism, this is
permAorB = fcPrejacent.
Instances For
¬□(p∨q): neither required. Under the isomorphism, this is
permAandB.
Instances For
The alternative set for ¬□(p∧q) is the same set as fcALT.
Negative FC via pex: pex^{IE+II}[¬□(p∧q)] ⊨ ¬□p ∧ ¬□q.
The paper's (19a): since pexFC on the ¬□-reinterpreted FCWorld
entails ◇b ∧ ◇a (= permB ∧ permA), and notReqA = permB,
notReqB = permA, we get ¬□p ∧ ¬□q.
Double requirement for necessity: ¬pex^{IE+II}[¬□(p∧q)] gives the negation of negative FC — i.e., both are required: □p ∧ □q.
This is the paper's (20): ⟦¬ pex^{IE+II}[¬□[T ∧ B]]⟧ = ¬(¬□T ∨ ¬□B)_{¬□T↔¬□B} ⊨ □T ∧ □B
Convenience re-export: exhIEII entails FC (proved as BarLevFox2020.free_choice).
Convenience re-export: pexIEII entails FC.
§3: The "Unaware" Puzzle #
Consider: "Noah is unaware that he may have tea or cake"
Intuition: This presupposes that Noah may have tea AND may have cake (FC is presupposed, not asserted).
Analysis with pex #
pex applies locally to ◇(t∨c), producing:
- assertion: ◇(t∨c)
- presupposition: ¬◇(t∧c) ∧ (◇t ↔ ◇c)
"Unaware" is a negative factive:
- presupposes: its complement (the full pex output holds)
- asserts: the subject doesn't believe it
The factive presupposes that pex holds — both assertion and presupposition. The homogeneity presupposition (◇t ↔ ◇c) combined with ◇(t∨c) entails ◇t ∧ ◇c. FC is presupposed!
Why flat exh fails #
With flat exh: exh(◇(t∨c)) = ◇(t∨c) ∧ ◇t ∧ ◇c ∧ ¬◇(t∧c) Under "unaware": presupposes the flat conjunction, asserts ¬Bel(flat)
The problem: the subject might fail to believe the conjunction for trivial reasons (not believing ¬◇(t∧c)), losing the FC presupposition. With pex, the FC-relevant content (homogeneity) is already presuppositional, so it projects independently.
Key theorem (§3): FC is presupposed under a negative factive.
When pex(◇(p∨q)) is embedded under "unaware", the overall sentence presupposes ◇p ∧ ◇q (free choice as presupposition).
Uses PrProp.negFactive from Core.Semantics.Presupposition.
The assertion of the negative factive embedding is about belief, not FC.
§4: Filtering FC in Disjunction #
Consider: "Either Maria can't study linguistics, or she can study syntax or semantics"
Intuition: FC inference arises — Maria can study syntax AND semantics.
Analysis with pex #
The second disjunct contains pex(◇(syn ∨ sem)):
- assertion: ◇(syn ∨ sem)
- presupposition: ◇syn ↔ ◇sem (homogeneity)
In disjunction "A ∨ B", the presupposition of B is filtered by ¬A (@cite{karttunen-1973}). Here:
- A = ¬◇ling
- ¬A = ◇ling (Maria CAN study linguistics)
- Under ◇ling, the presupposition ◇syn ↔ ◇sem is informative
The homogeneity presupposition projects (after filtering), and combined with ◇(syn ∨ sem), derives FC.
Why flat exh fails #
With flat exh in the second disjunct: ◇(syn∨sem) ∧ ◇syn ∧ ◇sem ∧ ¬◇(syn∧sem) The FC content is asserted, not presupposed. In disjunction, only presuppositions project — assertions do not. So the FC inference is trapped inside the second disjunct and doesn't become part of the overall meaning.
When the first disjunct is false, Karttunen filtering recovers full
satisfaction of the second disjunct.
Uses PrProp.disjFilterLeft from Core.Semantics.Presupposition.
Corollary: filtering FC for the concrete FCWorld case. When filtered pex holds and the first disjunct is false, FC follows.
Why pex Solves Puzzles That exh Cannot #
The fundamental difference is at-issue structure:
| exh^{IE+II}(φ) | pex^{IE+II}(φ) | |
|---|---|---|
| Asserts | φ ∧ ¬IE ∧ II | φ |
| Presupposes | nothing | ¬IE ∧ homog(II) |
This matters for embedding:
Under negation: Negation targets assertions, not presuppositions.
- ¬exh(φ) = ¬(φ ∧ ¬IE ∧ II) — FC lost under negation
- ¬pex(φ) = ¬φ with presup intact — double prohibition
Under factives: Factives presuppose their complement.
- aware(exh(φ)) presupposes the flat conjunction — muddled
- aware(pex(φ)) presupposes φ + homogeneity — clean FC projection
In disjunctions: Only presuppositions project/filter.
- A ∨ exh(φ): FC trapped in assertion, doesn't project
- A ∨ pex(φ): homogeneity presupposition projects, FC derives
Key structural fact: pex and exh agree on what they entail (both derive FC), but disagree on at-issue structure (assert vs presuppose).
Negative FC #
The duality isomorphism (Presuppositional.lean §7b) gives
negative FC from the same FCWorld computation. Here we verify the
embedded predictions.
§3.3: Presupposed negative FC under negative factives #
"Noah is unaware that Olivia is not required to take Logic and Algebra"
Presupposes: ¬□L ∧ ¬□A (negative FC). The solution parallels §3.2: pex applies locally, the negative factive presupposes the full pex output, and the homogeneity ¬□L ↔ ¬□A combined with ¬□(L∧A) entails ¬□L ∧ ¬□A.
Presupposed negative FC: under a negative factive, pex presupposes ¬□L ∧ ¬□A (negative free choice).
Filtering negative FC: when the first disjunct is false, the filtered presupposition of the second disjunct recovers negative FC.
§5.1: Universal, Existential, and Negative-Existential FC #
@cite{chemla-2009b} shows that ∀◇∨-sentences have universal FC readings and ¬∃□∧-sentences have universal negative FC readings.
Analysis with embedded pex #
The LFs with embedded pex^{IE+II}:
- ∀x ∈ S[pex^{IE+II}[◇[Cx ∨ ICx]]]
- ¬∃x ∈ S[pex^{IE+II}[□[Ax ∧ Bx]]]
- ∃x ∈ S[pex^{IE+II}[◇[Cx ∨ ICx]]]
pex triggers the homogeneity presupposition in the scope of the quantifier. Presuppositions project universally from the scope of universal quantifiers (@cite{chemla-2009a}, @cite{fox-2013}, @cite{mayr-sauerland-2015}). Combined with the assertive content, (universal/existential) FC follows.
Universal FC: universally projected homogeneity + universal assertion entails universal FC.
Universal negative FC: universally projected homogeneity + negated existential assertion entails universal negative FC.
Existential FC: universally projected homogeneity + existential assertion entails existential FC.
∃x ∈ S[pex^{IE+II}[◇[Cx ∨ ICx]]] yields:
- presupposes: ∀x ∈ S(◇Cx ↔ ◇ICx) (universal projection)
- asserts: ∃x ∈ S(◇(Cx ∨ ICx))
Together: ∃x ∈ S(◇Cx ∧ ◇ICx).
Universal FC via PrProp.forallPr: when each student's pex output
holds (presupposition projected universally + assertion holds),
universal FC follows.
This connects the abstract entailment theorems above to the concrete
forallPr combinator from Core.Semantics.Presupposition.
Existential FC via PrProp.existsPrUniv: with universal presupposition
projection from an existential quantifier, we get existential FC.
This connects the existential entailment theorem to the concrete
existsPrUniv combinator from Core.Semantics.Presupposition.
Universal negative FC via PrProp.negExistsPr: with universal
presupposition projection and negated existential assertion,
universal negative FC follows.
This connects universal_negative_fc to the concrete
negExistsPr combinator from Core.Semantics.Presupposition,
completing the set of quantifier bridges alongside
forallPr_fc and existsPrUniv_fc.
The shape differs from the positive bridges: forallPr_fc and
existsPrUniv_fc use hFC : holds → projA ∧ projB (assertion
decomposes to FC). Here, the assertion is negated, so we need:
hAssertEq: assertion ↔ reqA ∧ reqB (decomposition)hHomog: presup → reqA ↔ reqB (homogeneity) These are exactly the inputs touniversal_negative_fc.
§5.2: Non-Monotonic Quantifiers #
@cite{gotzner-romoli-santorio-2020} show that "exactly one"-sentences have salient readings where one student has FC/double prohibition while all others have the opposite. pex handles these straightforwardly via universal homogeneity projection + the cardinality constraint.
(76): "Exactly one student can take Logic or Calculus" #
The LF: ∃!x ∈ S[pex^{IE+II}[◇[Lx ∨ Cx]]]
pex triggers homogeneity ◇Lx ↔ ◇Cx universally (for all students). The assertive part says exactly one student satisfies ◇(Lx ∨ Cx).
Combined:
- The unique student has ◇(L ∨ C) ∧ (◇L ↔ ◇C) → ◇L ∧ ◇C (FC)
- All other students have ¬◇(L ∨ C) ∧ (◇L ↔ ◇C) → ¬◇L ∧ ¬◇C (double prohibition)
(77): "Exactly one student can't take Logic or Calculus" #
The LF: ∃!x ∈ S[¬ pex^{IE+II}[◇[Lx ∨ Cx]]]
Combined:
- The unique student has ¬◇(L ∨ C) ∧ (◇L ↔ ◇C) → ¬◇L ∧ ¬◇C (double prohibition)
- All other students have ◇(L ∨ C) ∧ (◇L ↔ ◇C) → ◇L ∧ ◇C (FC)
Non-monotonic FC (76a): universal homogeneity + "exactly one has ◇∨" entails that the unique student has FC and all others have double prohibition.
@cite{gotzner-romoli-santorio-2020}, @cite{delpinal-bassi-sauerland-2024} §5.2
Non-monotonic FC (77a): universal homogeneity + "exactly one lacks ◇∨" entails that the unique student has double prohibition and all others have FC.
@cite{gotzner-romoli-santorio-2020}, @cite{delpinal-bassi-sauerland-2024} §5.2
Why Flat exh Cannot Solve the Embedded FC Puzzles #
The paper's central argument is that flat exh (including exh^{IE+II}) cannot solve the presupposed & filtering FC puzzles because its output is fully assertive. Here we formalize the specific failure modes.
Failure 1: exh under negative factives (§3.1) #
With exh^{IE+II}, the output for ◇(L∨A) is flat: exh(◇(L∨A)) = ◇(L∨A) ∧ ◇L ∧ ◇A ∧ ¬◇(L∧A)
Under "S is unaware that exh(◇(L∨A))":
- presupposes: ◇(L∨A) ∧ ◇L ∧ ◇A ∧ ¬◇(L∧A) (the flat conjunction)
- asserts: ¬B_S(◇(L∨A) ∧ ◇L ∧ ◇A ∧ ¬◇(L∧A))
The problem: the assertion says S doesn't believe the whole conjunction. This is too weak — S might fail to believe ¬◇(L∧A) while still believing ◇L ∧ ◇A. The target is that S doesn't believe Olivia can take either class individually (a stronger claim about S's beliefs).
Failure 2: exh in filtering disjunction (§4.1) #
For "Either Maria can't study linguistics, or she can study syntax or semantics": the FC content (◇syn ∧ ◇sem) is assertive in exh's output, so it's trapped inside the second disjunct. In disjunction, only presuppositions project/filter — assertions don't. So the FC inference cannot reach the overall sentence meaning.
With pex, FC content is presuppositional, so it projects through disjunction via Karttunen filtering.
Flat exh output: exh^{IE+II}(◇(p∨q)) is fully assertive — no presuppositional component.
Equations
Instances For
Negative factive embedding of FLAT exh. "S is unaware that exh(◇(L∨A))":
- presupposes: the flat conjunction holds
- asserts: S doesn't believe the flat conjunction
Equations
- One or more equations did not get rendered due to their size.
Instances For
Failure 1a: Under flat exh, the factive asserts non-belief of the entire flat conjunction (FC + exclusivity). S might fail to believe the conjunction by not believing ¬◇(L∧A), while still believing ◇L ∧ ◇A.
Failure 1b: In contrast, pex's factive asserts non-belief of just the prejacent — the correct content for S's doxastic state.
Failure 2: When flat exh is placed in a filtering disjunction, the FC content is assertive and thus trapped inside the disjunct. Only presuppositions can project/filter in disjunctions.
For "A ∨ exh(◇(p∨q))": the presupposition is trivial (True).
pex's filtering disjunction has a non-trivial presupposition (homogeneity conditioned on ¬firstDisjunct).
Empirical Predictions #
| Puzzle | exh | pex | Status |
|---|---|---|---|
| Basic FC: ◇(p∨q) → ◇p∧◇q | ✓ | ✓ | pex_fc |
| Double prohibition: ¬◇(p∨q) → ¬◇p∧¬◇q | needs economy | ✓ | pex_double_prohibition |
| Negative FC: ¬□(p∧q) → ¬□p∧¬□q | needs economy | ✓ | pex_negative_fc |
| FC under neg. factive | ✗ | ✓ | fc_presupposed_under_neg_factive |
| Filtering FC | ✗ | ✓ | filtering_fc |
| Universal FC | ✓ (matrix exh) | ✓ | universal_fc |
| Existential FC | ✗ (matrix exh) | ✓ | existential_fc |
| Universal neg. FC | ✗ | ✓ | universal_negative_fc |
| Non-monotonic FC | problematic | ✓ | exactly_one_fc |
| Non-monotonic DP | problematic | ✓ | exactly_one_double_prohibition |
pex is the mirror image of "only" (@cite{horn-1969}): only presupposes its prejacent and asserts the negation of alternatives; pex asserts its prejacent and presupposes the alternative-derived content. Both split meaning into assertive and presuppositional components; they swap which goes where.
The key advantage of pex is that embedded FC puzzles are solved by standard presupposition projection — no new mechanisms needed.
Grounding in Projection Theory #
@cite{delpinal-bassi-sauerland-2024}'s central claim is that pex solves embedded FC puzzles using standard presupposition projection — no new mechanisms. We verify this by showing each embedding prediction is derived from independently formalized projection infrastructure:
| Prediction | Infrastructure | Bridge |
|---|---|---|
| Filtering FC (§4) | localCtxSecondDisjunct | local_context_matches_disjFilterLeft |
| Presupposed FC (§3) | transparentProjection | negFactive_entails_transparent |
| Double prohibition (§2) | negation_preserves_projection | definitional (PrProp.neg) |
| Quantificational FC (§5.1) | forallPr/existsPrUniv/negExistsPr | universal projection |
| Non-monotonic FC (§5.2) | universal homogeneity + cardinality | exactly_one_fc |
| Accommodation (§4.4) | heimSelect | accommodation_grounded_in_heim |
Filtering FC is grounded in Schlenker's local context algorithm.
filtering_fc uses PrProp.disjFilterLeft as a combinator.
local_context_matches_disjFilterLeft proves this is equivalent to
filtering at Schlenker's local context for the second disjunct:
the presupposition ψ of the second disjunct is satisfied in
the local context c ∧ ¬A iff ∀w∈c, ¬A(w) → ψ(w).
Presupposed FC is grounded in transparent projection.
fc_presupposed_under_neg_factive uses PrProp.negFactive as a
combinator. Here we decompose this into two steps:
negFactive_entails_transparent: negFactive's presupposition (complement holds) entails transparent projection of the presup.- Transparent projection + assertion → FC.
This shows that presupposed FC is an instance of Schlenker's transparent projection, not a stipulated combinator.
Opaque FC under belief embedding: when pex's presupposition is attributed to the attitude holder (opaque projection), the agent believes FC.
"Noah believes he may have tea or cake":
- pex applies locally: assertion = ◇(t∨c), presup = ◇t ↔ ◇c
- Opaque projection: Noah believes ◇t ↔ ◇c
- Combined with Noah believes ◇(t∨c): Noah believes ◇t ∧ ◇c
Both opaque and transparent projection yield FC — they differ in whose context the inference is anchored to.
Double prohibition is grounded in negation transparency.
PrProp.neg preserves presuppositions by construction (assertion negated,
presupposition unchanged). This matches negation_preserves_projection:
Schlenker's local context under negation has the same world set as the
parent context, so presuppositions project through negation unchanged.
Accommodation is grounded in Heim's global preference.
@cite{delpinal-bassi-sauerland-2024} §4.4: in standard cases, pex's
homogeneity presupposition is accommodated globally (added to the
common ground). This follows from heimSelect choosing global
accommodation whenever the result is consistent.
The bridge: when global accommodation of pex's presupposition is consistent, Heim's strategy selects global accommodation, matching the paper's prediction that homogeneity projects to the top level.
In "enemy territory" (§4.4), local ACC blocks global projection —
this corresponds to the case where heimSelect falls back to local
because global accommodation would be inconsistent.
When global accommodation is inconsistent (enemy territory), Heim's strategy falls back to local accommodation — blocking projection. This models the ACC operator from §4.4 that prevents homogeneity from projecting in hostile environments.
Bridge: pexFC as Implicature FCWorld Prop + non-cancellability #
The marquee BPS-style result the cross-mechanism Implicature spine in
Theories/Pragmatics/Implicature/Defs.lean was designed to host. The
free-choice inference (◇A ∧ ◇B from ◇(A ∨ B)) is wrapped as an
Implicature FCWorld Prop whose content is the presupposed component
of pexFC. Two non-cancellability theorems are stated, tracking the
structural-vs-substantive distinction documented at the
Presuppositional.lean BPS bridge: pexFC_not_cancellable follows from
the wrapper's choice to set assertion to holds; pexFC_neg_not_cancellable
follows from projection of pexFC.presup through PrProp.neg, the
formal counterpart to BPS's family-of-sentences test.
The free-choice inference, wrapped as a categorical implicature. The
content is pexFC.presup, i.e., the negated IE alternatives plus the
homogeneity over II alternatives — the non-at-issue content that BPS
treats as projective. The kind is updated to .freeChoice (the default
from bpsToImplicature is .scalar).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Structural non-cancellability for the FCWorld instance: when the
assertion is the full pex output (pexFC.holds), no continuation cancels
the inferred content. This follows from holds := presup ∧ assertion
trivially.
Substantive non-cancellability — projection through negation.
Even after asserting ¬pexFC (the negation of the FC pex output), the
free-choice inference (pexFC.presup, which yields permA w ∧ permB w
by pex_fc) survives. This is the formal counterpart to BPS's
projection argument: the inference is not at-issue, so embedding under
negation does not cancel it. The proof traces through
PrProp.neg_presup — the structural projection identity — not just
the trivial holds → presup.