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 (Excluder.preExhaustify, 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]
• [KS17]
• [AOMB10]
• [Fal14]
• [Fox07]
• [BLF20]
• [AP15]

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) is that Forood bought a book.

Equations

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

def AlonsoOvalleMoghiseh2025a.scalar : Finset Buy

The scalar alternative (54) is that 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) restrict the claim to each proper subdomain.

Equations

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

theorem AlonsoOvalleMoghiseh2025a.preExhaustify_domainAlts : Exhaustification.innocent.preExhaustify domainAlts = {prop fun (x : Buy) => x = {0}, prop fun (x : Buy) => x = {1}}

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

Modal contexts (§3, §5)

@[reducible, inline]

abbrev AlonsoOvalleMoghiseh2025a.Base : Type

A nonempty modal base collects 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 : SetRel Modal Modal

An accessible world has the same modal base and lies in it.

Equations

• AlonsoOvalleMoghiseh2025a.acc = {p : AlonsoOvalleMoghiseh2025a.Modal × AlonsoOvalleMoghiseh2025a.Modal | p.2.1 = p.1.1 ∧ p.2.2 ∈ ↑p.1.1}

@[instance_reducible]

instance AlonsoOvalleMoghiseh2025a.instDecidableMemProdModalSetRelAccMk (m m' : Modal) : Decidable ((m, m') ∈ acc)

Equations

• AlonsoOvalleMoghiseh2025a.instDecidableMemProdModalSetRelAccMk m m' = { decide := decide (m'.1 = m.1) && decide (m'.2 ∈ ↑m.1), reflects_decide := ⋯ }

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 apply the modal pointwise (fn. 15).

Equations

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

def AlonsoOvalleMoghiseh2025a.fc (m : Modal) : Prop

Free choice holds at a modal world when 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

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

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

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

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

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

theorem AlonsoOvalleMoghiseh2025a.modal_insertion : have φ := Exhaustification.tolerant.exh ({box' (at' scalar)} ∪ Exhaustification.innocent.preExhaustify (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)

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

Unembedded yek-i DPs (§4)

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

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

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

Partial scalar exhaustification gives uniqueness (93a).

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

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

theorem AlonsoOvalleMoghiseh2025a.root_innocent : Exhaustification.innocent.exh ({scalar} ∪ Exhaustification.innocent.preExhaustify 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 (Exhaustification.innocent.preExhaustify (lift dia domainAlts)) (dia (at' exactlyOne)) = prop fc ∩ dia (at' exactlyOne) ∧ world {{0}, {1}, {0, 1}} {0} deontic_tolerant_box._proof_1 ∈ Exhaustification.innocent.exh (Exhaustification.innocent.preExhaustify (lift dia domainAlts)) (dia (at' exactlyOne))

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

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

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

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

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

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

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

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

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

Downward entailing contexts (§3, §5)

@[reducible, inline]

abbrev AlonsoOvalleMoghiseh2025a.Cond : Type

A world of the conditional (77) records 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 (Exhaustification.innocent.preExhaustify condAlts) conditional = conditional ∧ Exhaustification.innocent.exh (Exhaustification.innocent.preExhaustify condAlts) conditionalUnique = conditionalUnique

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

theorem AlonsoOvalleMoghiseh2025a.conditional_weakening : conditional ⊂ conditionalUnique

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

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₅) : SetRel Buy₅ Buy₅

Accessibility from any world to the scenario's possibilities.

Equations

• AlonsoOvalleMoghiseh2025a.scenarioAcc A = SetRel.ofSuccessors fun (x : AlonsoOvalleMoghiseh2025a.Buy₅) => ↑A

@[instance_reducible]

instance AlonsoOvalleMoghiseh2025a.instDecidableMemProdBuy₅SetRelScenarioAccMk (A : Finset Buy₅) (u v : Buy₅) : Decidable ((u, v) ∈ scenarioAcc A)

Equations

• AlonsoOvalleMoghiseh2025a.instDecidableMemProdBuy₅SetRelScenarioAccMk A u v = AlonsoOvalleMoghiseh2025a.instDecidableMemProdBuy₅SetRelScenarioAccMk._aux_1 A u 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

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 : Datum) : 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 : Datum) : 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 : Datum) : row ∈ Examples.all → (row.feature? "modalInsertion").isSome = true → (row.feature? "partialExhaustification").isSome = true → (row.judgment = Judgment.ungrammatical ↔ row.feature? "modalInsertion" = some "no" ∧ row.feature? "partialExhaustification" = some "no")

An unembedded EFCI is ungrammatical exactly when it allows neither modal insertion nor partial exhaustification (Table 2).