Alonso-Ovalle & Moghiseh 2025: Existential Free Choice Items #
@cite{alonso-ovalle-moghiseh-2025}
Existential free choice items: The case of Farsi yek-i DPs. Semantics & Pragmatics 18, Article 4.
Core Contribution #
Farsi yek-i DPs instantiate a new EFCI profile: they pattern with other EFCIs in DE and modal contexts (plain existential in DE, strengthened under modals), but in root contexts they are grammatical, have no modal component, and convey uniqueness. The paper argues this profile derives from split exhaustification: scalar and domain alternatives are exhaustified by independent operators, with scalar exhaustification clause-bounded below the modal.
Key Theoretical Results Formalized Here #
- Root + full exhaustification = ⊥ (motivates rescue mechanisms)
- Root + scalar-only = uniqueness (yek-i's partial exhaustification)
- Root + domain-only = conjunction (blocked by Economy Principle)
- ◇ + split exh = FC + embedded uniqueness (yek-i under deontic ◇)
- DE + scalar exh weakens (Maximize Strength blocks it)
- EFCI typology (Table 2: modal insertion × partial exh)
- Split necessity (alternatives 143-146: single/two-operator alternatives fail)
Relationship to SplitExhaustification.lean #
Each result is verified computationally on small finite world types
(PQWorld, PermW, CondW) via the Excluder API
(innocent.exh/tolerant.exh). The companion module
Exhaustification.SplitExhaustification proves the same results
structurally at the Prop level for arbitrary domains. The two are
complementary: the general module proves WHY the results hold; this
file verifies the algorithm computes the right answers.
Root Contexts (§4) #
With a domain D = {b₁, b₂}, the assertion of unembedded yek-i is
b₁ ∨ b₂ ("Forood bought a book"). PQWorld enumerates the four
possible book-buying configurations.
The three alternative classes:
- Scalar: {b₁ ∧ b₂} (bought ≥ 2, from replacing numeral yek)
- Domain: {b₁, b₂} (restricting quantification to subdomains)
- Pre-exhaustified domain: {b₁ ∧ ¬b₂, b₂ ∧ ¬b₁}
Equations
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- AlonsoOvalleMoghiseh2025.instDecidableEqPQWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯
Equations
- One or more equations did not get rendered due to their size.
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Pre-exhaustified domain alternatives are derived from IE, not stipulated.
innocent.exh({b₁,b₂})(b₁) = b₁ ∧ ¬b₂ and dually for b₂.
Theorem (eq. 92): Chierchia's contradiction-tolerating operator applied to all alternatives yields ⊥ — the assertion conjoined with negation of all non-entailed alternatives is unsatisfiable.
(b₁∨b₂) ∧ ¬(b₁∧b₂) ∧ ¬(b₁∧¬b₂) ∧ ¬(b₂∧¬b₁) ⟺ ⊥
With Fox's IE, full exhaustification is vacuous (IE = ∅, no alternative is in every MCE).
Note on MCE count: The paper's (101) lists 2 MCEs for this
alternative set, but there are actually 3 — {b₁∧b₂, b₁∧¬b₂},
{b₁∧b₂, b₂∧¬b₁}, and {b₁∧¬b₂, b₂∧¬b₁}. Since no alternative
appears in all 3, IE = ∅ and Fox's operator is vacuous. The paper's
result (103) = uniqueness requires IE = {b₁∧b₂}, which holds when
the operators are applied separately (scalar-only IE correctly
excludes b₁∧b₂ — see root_scalar_only_uniqueness).
Innocent vs tolerant: For this specific alternative set, tolerant
yields ⊥ while innocent is vacuous — they differ maximally. The
split exhaustification architecture (O_σ and O_EXH-D as independent
operators) means the paper's predictions go through innocent on
each operator separately, not tolerant on the combined set.
Theorem (eq. 93a): O_σ (scalar-only exhaustification) yields uniqueness: (b₁ ∨ b₂) ∧ ¬(b₁ ∧ b₂) = "exactly one book."
This is yek-i's reading in root contexts via partial exhaustification.
Uniqueness is contingent (not contradictory).
Theorem (eq. 93b): O_EXH-D (domain-only exhaustification) yields conjunction: (b₁ ∨ b₂) ∧ (b₁ ↔ b₂) ⟺ b₁ ∧ b₂.
This is blocked by Chierchia's Economy Principle (the result is equivalent to the scalar alternative).
Domain-only result is equivalent to the scalar alternative → blocked by the Exhaustification Economy Principle.
Deontic Possibility (§5, eq. 114–119) #
LF: O_EXH-D ◇ O_σ [IP ye book-i ... Forood buy t₁]
Step 1: O_σ on IP → (b₁∨b₂) ∧ ¬(b₁∧b₂) = "exactly one book" Step 2: ◇ applied → ◇(b₁⊻b₂) = "permitted to buy exactly one" Step 3: O_EXH-D negates pre-exhaustified domain alternatives
The result is FC + embedded uniqueness: ◇b₁ ∧ ◇b₂ ∧ ◇(b₁⊻b₂), meaning each book is a permitted option and in each permitted world exactly one book is bought.
World Type #
Worlds are parameterized by which atomic modal propositions hold: ◇(b₁∧¬b₂), ◇(b₂∧¬b₁), ◇(b₁∧b₂). This gives 8 possible states.
Modal worlds for the EFCI analysis. Each world represents a permission state parameterized by three atomic modal propositions: ◇(b₁∧¬b₂), ◇(b₂∧¬b₁), ◇(b₁∧b₂). Named by which are true (1) or false (0) in order.
Instances For
Equations
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- AlonsoOvalleMoghiseh2025.instDecidableEqPermW x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯
Equations
Equations
- AlonsoOvalleMoghiseh2025.instBEqPermW.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)
Instances For
Equations
- One or more equations did not get rendered due to their size.
Pre-exhaustified domain alts are correctly computed by applying innocent.exh
to each domain alternative w.r.t. the domain alternative set.
Theorem (eq. 119): Split exhaustification under ◇ derives FC + embedded uniqueness: ◇(b₁⊻b₂) ∧ (◇b₁ ↔ ◇b₂)
Equivalently: ◇(b₁⊻b₂) ∧ ◇b₁ ∧ ◇b₂ — each book is a permitted option, and in each permitted world exactly one book is bought.
FC component: the result entails ◇b₁ ∧ ◇b₂ whenever true.
Embedded uniqueness: the assertion ◇(b₁⊻b₂) means in every permitted world exactly one book is bought (the ⊻ is under ◇).
The result is compatible with ◇(b₁∧b₂) being true (fn. 14): Forood may be permitted to buy more than one book.
Theorem: Single IE on ◇(b₁∨b₂) without split gives ◇(b₁∨b₂) ∧ ¬◇(b₁∧b₂) — anti-conjunction at the modal level (only ◇(b₁∧b₂) is innocently excludable), but NOT free choice.
This shows split exhaustification is necessary for yek-i's distinctive FC + embedded uniqueness profile.
The single-exh result is NOT free choice: there exists a world satisfying the exhaustified assertion where ◇b₁ but ¬◇b₂.
Why Split Exhaustification Is Necessary #
The paper argues that only split exhaustification — two independent operators targeting different alternative classes — derives the correct result. Three alternative architectures all fail:
- Single operator below ◇ (eq. 143): gives ◇(uniqueness), too weak
- Single operator above ◇ (eq. 146): gives FC + unwanted ¬◇(b₁∧b₂)
- Two operators above+below (eq. 144): same as (2) — too strong
Only split exh (O_EXH-D above ◇, O_σ below ◇) avoids negating the modal scalar alternative, producing FC + uniqueness without ¬◇(b₁∧b₂).
Single operator below ◇ too weak (eq. 143): after scalar exhaustification below the modal gives ◇(b₁⊻b₂), the result is compatible with only one book being permitted — no FC emerges without domain exhaustification above the modal.
Single operator above ◇ too strong (eq. 146): a single IE operator above ◇ with all alternatives on the unexhaustified assertion ◇(b₁∨b₂) gives FC (from domain alts) BUT ALSO ¬◇(b₁∧b₂) (from scalar alt).
Compare with split exh (deontic_poss_split_exh): the only
difference is && !canJoint w. Split exh allows ◇(b₁∧b₂),
this forbids it.
Two operators above+below ◇ too strong (eq. 144-145): two IE operators (O_σ below gives ◇(b₁⊻b₂), then full IE above) produces FC + embedded uniqueness BUT ALSO ¬◇(b₁∧b₂).
Compare with split exh: identical result except for && !canJoint w.
The scalar alternative ◇(b₁∧b₂) is innocently excludable because it
is non-entailed and consistently negatable alongside domain-alt
negations.
Two-IE exhaustification is strictly stronger than split: it entails the split result but not vice versa. The difference is exactly ¬◇(b₁∧b₂) — split exh never negates the modal scalar alternative.
The distinguishing case: split exh allows ◇(b₁∧b₂) (compatible with Forood buying both), while any architecture targeting the scalar alternative at the modal level forbids it.
Deontic Necessity (§5, eq. 120) #
LF: O_EXH-D □ O_σ [IP ye book-i ... Forood buy t₁]
The same split exhaustification structure under □ instead of ◇.
Step 1: O_σ on IP → b₁⊻b₂ (as before) Step 2: □ applied → □(b₁⊻b₂) = "must buy exactly one" Step 3: O_EXH-D negates pre-exhaustified domain alternatives under □
Box Operators (reusing PermW) #
□b₁ = ¬◇(b₂∧¬b₁) = ¬canExB2: every accessible world has b₁. □b₂ = ¬◇(b₁∧¬b₂) = ¬canExB1: every accessible world has b₂. □(b₁⊻b₂) = ¬◇(b₁∧b₂) = ¬canJoint: no joint-purchase world accessible.
Pre-exhaustified domain alts under □ are derived from IE.
Theorem (eq. 120): Split exhaustification under □ derives FC + embedded uniqueness: □(b₁⊻b₂) ∧ (□b₁ ↔ □b₂).
"Must buy exactly one book, and neither book is predetermined" — each book remains a possible choice within the obligation.
FC component under □: ¬□b₁ ∧ ¬□b₂ (neither book is obligatory) whenever the exhaustified assertion holds non-vacuously.
Embedded uniqueness under □: no joint-purchase world is accessible.
DE Contexts (§5, eq. 129–135) #
In DE contexts (e.g., conditional antecedents), scalar exhaustification below the operator is blocked by Maximize Strength: it globally weakens the matrix sentence.
"If Forood reads ye book-i, he gets a gift"
- Without O_σ: (b₁ ∨ b₂) → g
- With O_σ: ((b₁ ∨ b₂) ∧ ¬(b₁ ∧ b₂)) → g ← strictly weaker!
Since weakening is detected, O_σ is blocked, and the EFCI contributes plain existential force.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Equations
- AlonsoOvalleMoghiseh2025.instDecidableEqCondW x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯
Equations
- One or more equations did not get rendered due to their size.
Theorem (eq. 131–134): Scalar exhaustification inside a conditional antecedent strictly weakens the matrix.
condNoExhF ⊂ condWithExhF: the exhaustified version is true in
strictly more worlds, so it carries less information.
Without exhaustification, the conditional is stronger: every
condNoExh-world is a condWithExh-world.
With exhaustification, there's a world satisfying condWithExh
but not condNoExh.
Theorem: In DE contexts, domain exhaustification on the
conditional is vacuous. The assertion (b₁∨b₂)→g already entails
both b₁→g and b₂→g, so the pre-exhaustified domain alternatives
(b₁→g ∧ ¬(b₂→g)) and (b₂→g ∧ ¬(b₁→g)) are both inconsistent
with the assertion. IE correctly returns ∅, and innocent.exh
is the identity.
This means even without Maximize Strength blocking O_σ, O_EXH-D alone contributes nothing in DE contexts — the plain existential reading emerges regardless.
EFCI Typology #
@cite{alonso-ovalle-moghiseh-2025} Table 2: EFCIs vary along two parameters — modal insertion and partial exhaustification.
| Type | Modal insertion | Partial exh |
|---|---|---|
| vreun | − | − |
| irgendein | + | − |
| yek-i | − | + |
- vreun: neither mechanism → contradiction in root → ungrammatical
- irgendein: modal insertion → covert □ rescues → epistemic ignorance
- yek-i: partial exh (scalar only) → uniqueness in root
A rescue parameter bundle for an EFCI.
- modalInsertion : Bool
- partialExh : Bool
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- AlonsoOvalleMoghiseh2025.instBEqEFCIParams.beq { modalInsertion := a, partialExh := a_1 } { modalInsertion := b, partialExh := b_1 } = (a == b && a_1 == b_1)
- AlonsoOvalleMoghiseh2025.instBEqEFCIParams.beq x✝¹ x✝ = false
Instances For
Equations
Equations
- AlonsoOvalleMoghiseh2025.vreunParams = { modalInsertion := false, partialExh := false }
Instances For
Equations
- AlonsoOvalleMoghiseh2025.irgendeinParams = { modalInsertion := true, partialExh := false }
Instances For
Equations
- AlonsoOvalleMoghiseh2025.yekiParams = { modalInsertion := false, partialExh := true }
Instances For
Grammaticality in root: an EFCI is grammatical iff at least one rescue mechanism is available.
Equations
Instances For
Root reading when grammatical.
- uniqueness : RootReading
- epistemicIgnorance : RootReading
- ungrammatical : RootReading
Instances For
Equations
- AlonsoOvalleMoghiseh2025.instDecidableEqRootReading x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Derive root reading from rescue parameters. Modal insertion takes priority when both are available.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Bridge to Determiners Lexicon #
The study's EFCIParams/rootReading and the Fragment lexicon's
IndefiniteEntry/getReading are two views of the same typology.
These bridge theorems prove they agree for all three EFCI types.
Convert study-level RootReading to Determiners EFCIReading option.
Equations
- AlonsoOvalleMoghiseh2025.RootReading.uniqueness.toDetReading = some Fragments.Farsi.Determiners.EFCIReading.uniqueness
- AlonsoOvalleMoghiseh2025.RootReading.epistemicIgnorance.toDetReading = some Fragments.Farsi.Determiners.EFCIReading.epistemicIgnorance
- AlonsoOvalleMoghiseh2025.RootReading.ungrammatical.toDetReading = none
Instances For
yek-i: study predicts uniqueness, lexicon agrees.
irgendein: study predicts epistemic ignorance, lexicon agrees.
vreun: study predicts ungrammatical (none), lexicon agrees.
The study's grammaticality prediction matches the lexicon:
getReading returns some _ iff grammaticalInRoot is true.