Alonso-Ovalle & Moghiseh (2025): existential free choice items

Farsi yek-i DPs are existential free choice items: plain existentials in downward entailing contexts, free choice under deontic modals and modal variation under epistemic ones (§2), but, unlike irgendein or vreun, grammatical and non-modal when unembedded, where they convey uniqueness (§2.4). In [Chi13]'s framework the DP introduces the scalar alternative at least two and the pre-exhaustified domain alternatives (preExhaustified, computed by innocent exclusion as in (56f)). Under a modal, negating the domain alternatives gives free choice (deontic_tolerant, the general freeChoice_of_proper), but negating the scalar alternative too is too strong under ◇ and too weak under □ (deontic_tolerant_box); in a conditional antecedent exhaustification is vacuous (conditional_vacuous). Unembedded, the contradiction-tolerant operator yields ⊥ (root_tolerant, (92)); modal insertion (85)–(87) rescues irgendein (modal_insertion), while yek-i prunes the domain alternatives, and partial scalar exhaustification gives uniqueness (root_scalar) where partial domain exhaustification returns the scalar alternative itself, which the Economy Principle (94) blocks (root_domain). Fox's contradiction-free operator does not deliver (103): the paper's (101) omits the maximal exclusion {¬(b₁∧¬b₂), ¬(b₂∧¬b₁)}, so no alternative is innocently excludable and exhaustification is vacuous (root_innocent).

The embedded uniqueness of §5 needs split exhaustification, scalar below the modal and domain above it (113): split_diamond and split_box derive (119)–(120), leaving ◇(b₁∧b₂) open, while the single-operator LFs (143)–(146) are too weak or too strong (single_below, single_above, two_innocent). Below if, scalar exhaustification weakens the sentence (conditional_weakening), so Maximize Strength (132) prunes it. The scenario verdicts of §§2–5 are checked in rows_agree on five-book models, and Table 2's typology in table2_rows.

References

• [AOM25a]
• [Chi13]
• [kratzer-shimoyama-2002]
• [alonso-ovalle-menendez-benito-2010]
• [Fal14]
• [Fox07]
• [BLF20]
• [aloni-port-2015]

The two-book model (§3)

@[reducible, inline]

abbrev AlonsoOvalleMoghiseh2025a.Buy : Type

A world records which of the two books Forood bought.

Equations

• AlonsoOvalleMoghiseh2025a.Buy = Finset (Fin 2)

def AlonsoOvalleMoghiseh2025a.buys (v : Buy) (i : Fin 2) : Prop

Book i is bought at v.

Equations

• AlonsoOvalleMoghiseh2025a.buys v i = (i ∈ v)

@[instance_reducible]

instance AlonsoOvalleMoghiseh2025a.instDecidablePredFinOfNatNatBuys (v : Buy) : DecidablePred (buys v)

Equations

• AlonsoOvalleMoghiseh2025a.instDecidablePredFinOfNatNatBuys v i = AlonsoOvalleMoghiseh2025a.instDecidablePredFinOfNatNatBuys._aux_1 v i

@[reducible, inline]

abbrev AlonsoOvalleMoghiseh2025a.prop {W : Type u_1} [Fintype W] (p : W → Prop) [DecidablePred p] : Finset W

The proposition denoted by a decidable predicate on worlds.

Equations

• AlonsoOvalleMoghiseh2025a.prop p = Finset.filter p Finset.univ

def AlonsoOvalleMoghiseh2025a.assertion : Finset Buy

The assertion (56c): Forood bought a book.

Equations

• AlonsoOvalleMoghiseh2025a.assertion = AlonsoOvalleMoghiseh2025a.prop (Exhaustification.claim AlonsoOvalleMoghiseh2025a.buys Finset.univ)

def AlonsoOvalleMoghiseh2025a.scalar : Finset Buy

The scalar alternative (54): Forood bought at least two books.

Equations

• AlonsoOvalleMoghiseh2025a.scalar = AlonsoOvalleMoghiseh2025a.prop fun (x : AlonsoOvalleMoghiseh2025a.Buy) => 2 ≤ Finset.card x

def AlonsoOvalleMoghiseh2025a.exactlyOne : Finset Buy

Exactly one book is bought.

Equations

• AlonsoOvalleMoghiseh2025a.exactlyOne = AlonsoOvalleMoghiseh2025a.prop fun (x : AlonsoOvalleMoghiseh2025a.Buy) => Finset.card x = 1

def AlonsoOvalleMoghiseh2025a.domainAlts : Finset (Finset Buy)

The domain alternatives (55): the claim restricted to each proper subdomain.

Equations

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

def AlonsoOvalleMoghiseh2025a.preExhaustified {W : Type u_1} [Fintype W] [DecidableEq W] (ALT : Finset (Finset W)) : Finset (Finset W)

The pre-exhaustified alternatives (56f): each alternative strengthened by innocent exclusion of the others.

Equations

• AlonsoOvalleMoghiseh2025a.preExhaustified ALT = Finset.image (Exhaustification.innocent.exh ALT) ALT

theorem AlonsoOvalleMoghiseh2025a.preExhaustified_domainAlts : preExhaustified domainAlts = {prop fun (x : Buy) => x = {0}, prop fun (x : Buy) => x = {1}}

(56f): the pre-exhaustified domain alternatives are only b₁ and only b₂.

Modal contexts (§3, §5)

@[reducible, inline]

abbrev AlonsoOvalleMoghiseh2025a.Base : Type

A nonempty modal base: the permitted (or epistemically possible) buy-worlds.

Equations

• AlonsoOvalleMoghiseh2025a.Base = { A : Finset AlonsoOvalleMoghiseh2025a.Buy // A.Nonempty }

@[instance_reducible]

instance AlonsoOvalleMoghiseh2025a.instFintypeBase : Fintype Base

Equations

• AlonsoOvalleMoghiseh2025a.instFintypeBase = Subtype.fintype fun (A : Finset AlonsoOvalleMoghiseh2025a.Buy) => A.Nonempty

@[instance_reducible]

instance AlonsoOvalleMoghiseh2025a.instDecidableEqBase : DecidableEq Base

Equations

• AlonsoOvalleMoghiseh2025a.instDecidableEqBase = Subtype.instDecidableEq

@[reducible, inline]

abbrev AlonsoOvalleMoghiseh2025a.Modal : Type

A modal world pairs a modal base with the actual buy-world; accessibility keeps the base and moves to one of its worlds, so the frame is serial.

Equations

• AlonsoOvalleMoghiseh2025a.Modal = (AlonsoOvalleMoghiseh2025a.Base × AlonsoOvalleMoghiseh2025a.Buy)

@[instance_reducible]

instance AlonsoOvalleMoghiseh2025a.instDecidableEqModal : DecidableEq Modal

Equations

• AlonsoOvalleMoghiseh2025a.instDecidableEqModal = instDecidableEqProd

@[instance_reducible]

instance AlonsoOvalleMoghiseh2025a.instFintypeModal : Fintype Modal

Equations

• AlonsoOvalleMoghiseh2025a.instFintypeModal = instFintypeProd AlonsoOvalleMoghiseh2025a.Base AlonsoOvalleMoghiseh2025a.Buy

def AlonsoOvalleMoghiseh2025a.acc (m m' : Modal) : Prop

Accessibility: an accessible world has the same modal base and lies in it.

Equations

• AlonsoOvalleMoghiseh2025a.acc m m' = (m'.1 = m.1 ∧ m'.2 ∈ ↑m.1)

@[instance_reducible]

instance AlonsoOvalleMoghiseh2025a.instDecidableRelModalAcc : DecidableRel acc

Equations

• AlonsoOvalleMoghiseh2025a.instDecidableRelModalAcc m m' = AlonsoOvalleMoghiseh2025a.instDecidableRelModalAcc._aux_1 m m'

def AlonsoOvalleMoghiseh2025a.world (A : Finset Buy) (v : Buy) (h : A.Nonempty := by decide) : Modal

The modal world with base A and actual buy-world v.

Equations

• AlonsoOvalleMoghiseh2025a.world A v h = (⟨A, h⟩, v)

def AlonsoOvalleMoghiseh2025a.buysM (m : Modal) (i : Fin 2) : Prop

Book i is bought at the modal world m.

Equations

• AlonsoOvalleMoghiseh2025a.buysM m i = (i ∈ m.2)

@[instance_reducible]

instance AlonsoOvalleMoghiseh2025a.instDecidablePredFinOfNatNatBuysM (m : Modal) : DecidablePred (buysM m)

Equations

• AlonsoOvalleMoghiseh2025a.instDecidablePredFinOfNatNatBuysM m i = AlonsoOvalleMoghiseh2025a.instDecidablePredFinOfNatNatBuysM._aux_1 m i

def AlonsoOvalleMoghiseh2025a.at' (p : Finset Buy) : Finset Modal

A proposition about the buy-world, evaluated at a modal world.

Equations

• AlonsoOvalleMoghiseh2025a.at' p = AlonsoOvalleMoghiseh2025a.prop fun (x : AlonsoOvalleMoghiseh2025a.Modal) => x.2 ∈ p

def AlonsoOvalleMoghiseh2025a.dia (p : Finset Modal) : Finset Modal

◇ as an operation on propositions.

Equations

• AlonsoOvalleMoghiseh2025a.dia p = AlonsoOvalleMoghiseh2025a.prop (ModalLogic.diamond AlonsoOvalleMoghiseh2025a.acc fun (x : AlonsoOvalleMoghiseh2025a.Modal) => x ∈ p)

def AlonsoOvalleMoghiseh2025a.box' (p : Finset Modal) : Finset Modal

□ as an operation on propositions.

Equations

• AlonsoOvalleMoghiseh2025a.box' p = AlonsoOvalleMoghiseh2025a.prop (ModalLogic.box AlonsoOvalleMoghiseh2025a.acc fun (x : AlonsoOvalleMoghiseh2025a.Modal) => x ∈ p)

def AlonsoOvalleMoghiseh2025a.lift (M : Finset Modal → Finset Modal) (ALT : Finset (Finset Buy)) : Finset (Finset Modal)

The alternatives of a modalized clause: the modal applied pointwise (fn. 15).

Equations

• AlonsoOvalleMoghiseh2025a.lift M ALT = Finset.image (M ∘ AlonsoOvalleMoghiseh2025a.at') ALT

def AlonsoOvalleMoghiseh2025a.fc (m : Modal) : Prop

Free choice at a modal world: each book is permitted.

Equations

• AlonsoOvalleMoghiseh2025a.fc m = Exhaustification.FreeChoice AlonsoOvalleMoghiseh2025a.acc m Finset.univ AlonsoOvalleMoghiseh2025a.buysM

@[instance_reducible]

instance AlonsoOvalleMoghiseh2025a.instDecidablePredModalFc : DecidablePred fc

Equations

• AlonsoOvalleMoghiseh2025a.instDecidablePredModalFc m = AlonsoOvalleMoghiseh2025a.instDecidablePredModalFc._aux_1 m

theorem AlonsoOvalleMoghiseh2025a.deontic_tolerant : Exhaustification.tolerant.exh ({dia (at' scalar)} ∪ preExhaustified (lift dia domainAlts)) (dia (at' assertion)) = prop fc \ dia (at' scalar)

(61): exhaustifying ◇(b₁∨b₂) over all alternatives at once gives free choice together with the unattested ¬◇(b₁∧b₂).

theorem AlonsoOvalleMoghiseh2025a.deontic_tolerant_box : world {{0}, {1}, {0, 1}} {0} ⋯ ∈ Exhaustification.tolerant.exh ({box' (at' scalar)} ∪ preExhaustified (lift box' domainAlts)) (box' (at' assertion))

(67)–(68): under □ the same exhaustification is too weak — it holds where Forood may buy more than one book.

theorem AlonsoOvalleMoghiseh2025a.modal_insertion : have φ := Exhaustification.tolerant.exh ({box' (at' scalar)} ∪ preExhaustified (lift box' domainAlts)) (box' (at' assertion)); φ.Nonempty ∧ φ ⊆ dia (prop fun (x : Modal) => buysM x 0) ∩ dia (prop fun (x : Modal) => buysM x 1) ∩ dia (prop fun (x : Modal) => ¬buysM x 0) ∩ dia (prop fun (x : Modal) => ¬buysM x 1)

(85)–(87): modal insertion rescues an unembedded irgendein — the result is contingent and conveys ignorance about each book.

Unembedded yek-i DPs (§4)

theorem AlonsoOvalleMoghiseh2025a.root_tolerant : Exhaustification.tolerant.exh ({scalar} ∪ preExhaustified domainAlts) assertion = ∅

(92): unembedded, the contradiction-tolerant operator yields ⊥.

theorem AlonsoOvalleMoghiseh2025a.root_scalar : Exhaustification.innocent.exh {scalar} assertion = exactlyOne

(93a): partial scalar exhaustification gives uniqueness.

theorem AlonsoOvalleMoghiseh2025a.root_domain : Exhaustification.innocent.exh (preExhaustified domainAlts) assertion = scalar

(93b)–(94): partial domain exhaustification returns the scalar alternative itself, so the Exhaustification Economy Principle blocks it.

theorem AlonsoOvalleMoghiseh2025a.root_innocent : Exhaustification.innocent.exh ({scalar} ∪ preExhaustified domainAlts) assertion = assertion

(101)–(103) do not go through: {¬(b₁∧¬b₂), ¬(b₂∧¬b₁)} is a third maximal consistent exclusion, so no alternative is innocently excludable and the contradiction-free operator is vacuous rather than delivering uniqueness.

Split exhaustification (§5)

theorem AlonsoOvalleMoghiseh2025a.split_diamond : Exhaustification.innocent.exh (preExhaustified (lift dia domainAlts)) (dia (at' exactlyOne)) = prop fc ∩ dia (at' exactlyOne) ∧ world {{0}, {1}, {0, 1}} {0} ⋯ ∈ Exhaustification.innocent.exh (preExhaustified (lift dia domainAlts)) (dia (at' exactlyOne))

(119): scalar exhaustification below ◇ and domain exhaustification above it give free choice with embedded uniqueness, compatible with ◇(b₁∧b₂).

theorem AlonsoOvalleMoghiseh2025a.split_box : Exhaustification.innocent.exh (preExhaustified (lift box' domainAlts)) (box' (at' exactlyOne)) = prop fc ∩ box' (at' exactlyOne)

(120): under □, every permitted world has exactly one book bought and each book is permitted.

theorem AlonsoOvalleMoghiseh2025a.single_below : world {{0}} {0} ⋯ ∈ dia (at' (Exhaustification.innocent.exh ({scalar} ∪ preExhaustified domainAlts) assertion)) ∧ ¬fc (world {{0}} {0} ⋯)

(143): a single contradiction-free operator below ◇ is vacuous (root_innocent), so the result is ◇(b₁∨b₂) — too weak for free choice.

theorem AlonsoOvalleMoghiseh2025a.single_above : Exhaustification.innocent.exh ({dia (at' scalar)} ∪ preExhaustified (lift dia domainAlts)) (dia (at' assertion)) = prop fc \ dia (at' scalar)

(146): a single contradiction-free operator above ◇ negates the scalar alternative, forbidding ◇(b₁∧b₂).

theorem AlonsoOvalleMoghiseh2025a.two_innocent : Exhaustification.innocent.exh ({dia (at' scalar)} ∪ preExhaustified (lift dia domainAlts)) (dia (at' exactlyOne)) = (prop fc ∩ dia (at' exactlyOne)) \ dia (at' scalar)

(144)–(145): two contradiction-free operators, below and above ◇, also forbid ◇(b₁∧b₂).

Downward entailing contexts (§3, §5)

@[reducible, inline]

abbrev AlonsoOvalleMoghiseh2025a.Cond : Type

A world of the conditional (77): the books read and whether Forood gets a gift.

Equations

• AlonsoOvalleMoghiseh2025a.Cond = (AlonsoOvalleMoghiseh2025a.Buy × Bool)

def AlonsoOvalleMoghiseh2025a.conditional : Finset Cond

If Forood reads a book, he gets a gift (78b).

Equations

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

def AlonsoOvalleMoghiseh2025a.conditionalUnique : Finset Cond

The conditional with scalar exhaustification in its antecedent (130e).

Equations

• AlonsoOvalleMoghiseh2025a.conditionalUnique = AlonsoOvalleMoghiseh2025a.prop fun (c : AlonsoOvalleMoghiseh2025a.Cond) => Finset.card c.1 = 1 → c.2 = true

def AlonsoOvalleMoghiseh2025a.condAlts : Finset (Finset Cond)

The domain alternatives of the conditional (78d).

Equations

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

theorem AlonsoOvalleMoghiseh2025a.conditional_vacuous : Exhaustification.tolerant.exh {prop fun (c : Cond) => 2 ≤ Finset.card c.1 → c.2 = true} conditional = conditional ∧ Exhaustification.innocent.exh (preExhaustified condAlts) conditional = conditional ∧ Exhaustification.innocent.exh (preExhaustified condAlts) conditionalUnique = conditionalUnique

(78)–(80): the scalar alternative is entailed and the domain alternatives are vacuous, so the plain existential reading survives; likewise for (135).

theorem AlonsoOvalleMoghiseh2025a.conditional_weakening : conditional ⊂ conditionalUnique

(131): scalar exhaustification inside the antecedent weakens the conditional, which Maximize Strength (132) forbids.

The paper's verdicts

@[reducible, inline]

abbrev AlonsoOvalleMoghiseh2025a.Buy₅ : Type

Five books; a scenario fixes the permitted or epistemically possible buy-worlds.

Equations

• AlonsoOvalleMoghiseh2025a.Buy₅ = Finset (Fin 5)

def AlonsoOvalleMoghiseh2025a.buys₅ (v : Buy₅) (i : Fin 5) : Prop

Equations

• AlonsoOvalleMoghiseh2025a.buys₅ v i = (i ∈ v)

@[instance_reducible]

instance AlonsoOvalleMoghiseh2025a.instDecidablePredFinOfNatNatBuys₅ (v : Buy₅) : DecidablePred (buys₅ v)

Equations

• AlonsoOvalleMoghiseh2025a.instDecidablePredFinOfNatNatBuys₅ v i = AlonsoOvalleMoghiseh2025a.instDecidablePredFinOfNatNatBuys₅._aux_1 v i

def AlonsoOvalleMoghiseh2025a.scenarioAcc (A : Finset Buy₅) : Buy₅ → Buy₅ → Prop

Accessibility from any world to the scenario's possibilities.

Equations

• AlonsoOvalleMoghiseh2025a.scenarioAcc A x✝ v = (v ∈ A)

@[instance_reducible]

instance AlonsoOvalleMoghiseh2025a.instDecidableRelBuy₅ScenarioAcc (A : Finset Buy₅) : DecidableRel (scenarioAcc A)

Equations

• AlonsoOvalleMoghiseh2025a.instDecidableRelBuy₅ScenarioAcc A x✝ v = AlonsoOvalleMoghiseh2025a.instDecidableRelBuy₅ScenarioAcc._aux_1 A x✝ v

def AlonsoOvalleMoghiseh2025a.scenario : String → Option (Finset Buy₅)

The possibilities a row's scenario feature names.

Equations

• AlonsoOvalleMoghiseh2025a.scenario "permitted24" = some {{0}, {1}, {2}}
• AlonsoOvalleMoghiseh2025a.scenario "required28" = some {{0}, {1}, {2}}
• AlonsoOvalleMoghiseh2025a.scenario "known34" = some {{0}, {1}, {2}}
• AlonsoOvalleMoghiseh2025a.scenario "known31" = some {∅, {0}, {1}, {2}}
• AlonsoOvalleMoghiseh2025a.scenario "anyNumber104" = some {x : AlonsoOvalleMoghiseh2025a.Buy₅ | Finset.Nonempty x}
• AlonsoOvalleMoghiseh2025a.scenario "twoBooks108" = some {x : AlonsoOvalleMoghiseh2025a.Buy₅ | Finset.card x = 2}
• AlonsoOvalleMoghiseh2025a.scenario x✝ = none

def AlonsoOvalleMoghiseh2025a.verdict (A : Finset Buy₅) : String → String → Option Bool

The verdict of an item under a modal over the possibilities A: a plain existential needs the claim under the modal, irgendein free choice, algún modal variation, and yek-i free choice or modal variation by flavor together with embedded uniqueness.

Equations

• One or more equations did not get rendered due to their size.
• AlonsoOvalleMoghiseh2025a.verdict A x✝¹ x✝ = none

def AlonsoOvalleMoghiseh2025a.predicted (row : Data.Examples.LinguisticExample) : Option Bool

A row's predicted verdict from its scenario, item, and modal features.

Equations

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

theorem AlonsoOvalleMoghiseh2025a.rows_agree (row : Data.Examples.LinguisticExample) : row ∈ Examples.all → ∀ (b : Bool), predicted row = some b → row.feature? "verdict" = some (if b = true then "true" else "false")

Every scenario row carries the predicted verdict.

theorem AlonsoOvalleMoghiseh2025a.table2_rows (row : Data.Examples.LinguisticExample) : row ∈ Examples.all → (row.feature? "modalInsertion").isSome = true → (row.feature? "partialExhaustification").isSome = true → (row.judgment = Features.Judgment.ungrammatical ↔ row.feature? "modalInsertion" = some "no" ∧ row.feature? "partialExhaustification" = some "no")

Table 2: an unembedded EFCI is ungrammatical exactly when it allows neither modal insertion nor partial exhaustification.