Alonso-Ovalle & Moghiseh (2025): number marking in Farsi what interrogatives

Farsi singular what interrogatives, bare (chi) and complex (che ketab-i), allow both singular and plural answers (20), (23); with the differential object marker -ro only the bare ones do (26)–(27). The paper derives this from three assumptions: interrogatives range over the conjunctions and disjunctions of nonempty subdomains (29), the meets and joins of their individuals (hamblin, mem_conjProp); singular marking on bare interrogatives is a default over atoms and pluralities (37), while SING on complex interrogatives keeps atoms only (42) (neutral, atoms); and -ro restricts the subset selection function to singletons (52), the IsSingleton functions of [AOMB10], which collapses ⊓ and ⊔ to individual answers (hamblinRo, hamblinRo_neutral). Dayal's answerhood operator (8) presupposes a maximally strong true answer (Question.IsExhaustivelyResolvable on the finite Hamblin set); a plural answer is available iff the presupposition holds in a world where two atoms were bought (farsi, (40)/(45)/(53)/(55)).

The background pattern of §2 — English bare vs. singular and plural complex interrogatives under Dayal's atoms-only domains and the presuppositional exhaustifier (15) — is dayal_english, and the generalized-quantifier answer to the Spanish bare-interrogative problem (19) is spanish_gq. Questions with must (30)–(36) are answerable by free choice disjunctions only when the interrogative ranges over disjunctions, which -ro removes (modal_gq, (58)–(63)); collective predicates need pluralities in the domain (collective, (56)–(57)). The paper's answer judgments are checked in rows_agree.

References

• [AOM25b]
• [Day96]
• [Day16]
• [Ham73]
• [Mal20]
• [ENS22]
• [AOR23]
• [Sco22]
• [AOMB10]

Entities, worlds, and answers

@[reducible, inline]

abbrev AlonsoOvalleMoghiseh2025b.Atom : Type

The atomic things; an entity is a nonempty sum of atoms and a world records which atoms Roya bought.

Equations

• AlonsoOvalleMoghiseh2025b.Atom = Fin 2

@[reducible, inline]

abbrev AlonsoOvalleMoghiseh2025b.Entity : Type

Equations

• AlonsoOvalleMoghiseh2025b.Entity = Finset AlonsoOvalleMoghiseh2025b.Atom

@[reducible, inline]

abbrev AlonsoOvalleMoghiseh2025b.World : Type

Equations

• AlonsoOvalleMoghiseh2025b.World = Finset AlonsoOvalleMoghiseh2025b.Atom

def AlonsoOvalleMoghiseh2025b.bought (e : Entity) (w : World) : Prop

Distributive bought, true of an entity when every atom of it was bought.

Equations

• AlonsoOvalleMoghiseh2025b.bought e w = (e ⊆ w)

@[instance_reducible]

instance AlonsoOvalleMoghiseh2025b.instDecidablePredWorldBought (e : Entity) : DecidablePred (bought e)

Equations

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

theorem AlonsoOvalleMoghiseh2025b.bought_union (e₁ e₂ : Entity) (w : World) : bought (e₁ ∪ e₂) w ↔ bought e₁ w ∧ bought e₂ w

def AlonsoOvalleMoghiseh2025b.neutral : Finset Entity

The number-neutral root (37): atoms and pluralities.

Equations

• AlonsoOvalleMoghiseh2025b.neutral = {x : AlonsoOvalleMoghiseh2025b.Entity | Finset.Nonempty x}

def AlonsoOvalleMoghiseh2025b.atoms : Finset Entity

SING (42), the atoms.

Equations

• AlonsoOvalleMoghiseh2025b.atoms = {x : AlonsoOvalleMoghiseh2025b.Entity | Finset.card x = 1}

Hamblin sets over generalized quantifiers (29)

def AlonsoOvalleMoghiseh2025b.conjProp {W : Type u_1} [Fintype W] (P : Entity → W → Prop) [(e : Entity) → DecidablePred (P e)] (X : Finset Entity) : Finset W

The proposition that the conjunction ⊓X holds of P.

Equations

• AlonsoOvalleMoghiseh2025b.conjProp P X = {w : W | ∀ e ∈ X, P e w}

def AlonsoOvalleMoghiseh2025b.disjProp {W : Type u_1} [Fintype W] (P : Entity → W → Prop) [(e : Entity) → DecidablePred (P e)] (X : Finset Entity) : Finset W

The proposition that the disjunction ⊔X holds of P.

Equations

• AlonsoOvalleMoghiseh2025b.disjProp P X = {w : W | ∃ e ∈ X, P e w}

theorem AlonsoOvalleMoghiseh2025b.mem_conjProp {W : Type u_1} [Fintype W] (P : Entity → W → Prop) [(e : Entity) → DecidablePred (P e)] (X : Finset Entity) (w : W) : w ∈ conjProp P X ↔ (⨅ e ∈ X, Quantifier.NP.individual e) fun (x : Entity) => P x w

theorem AlonsoOvalleMoghiseh2025b.mem_disjProp {W : Type u_1} [Fintype W] (P : Entity → W → Prop) [(e : Entity) → DecidablePred (P e)] (X : Finset Entity) (w : W) : w ∈ disjProp P X ↔ (⨆ e ∈ X, Quantifier.NP.individual e) fun (x : Entity) => P x w

def AlonsoOvalleMoghiseh2025b.hamblin {W : Type u_1} [Fintype W] (P : Entity → W → Prop) [(e : Entity) → DecidablePred (P e)] [DecidableEq W] (D : Finset Entity) : Finset (Finset W)

The Hamblin set (29), the meets and joins over every nonempty subdomain of D, applied to P.

Equations

• AlonsoOvalleMoghiseh2025b.hamblin P D = Finset.image (AlonsoOvalleMoghiseh2025b.conjProp P) (Finset.Ioc ∅ D) ∪ Finset.image (AlonsoOvalleMoghiseh2025b.disjProp P) (Finset.Ioc ∅ D)

def AlonsoOvalleMoghiseh2025b.hamblinRo {W : Type u_1} [Fintype W] (P : Entity → W → Prop) [(e : Entity) → DecidablePred (P e)] [DecidableEq W] (D : Finset Entity) : Finset (Finset W)

With -ro (52) the selection function returns a singleton, so the Hamblin set is the union of the Hamblin sets over the singleton subdomains.

Equations

• AlonsoOvalleMoghiseh2025b.hamblinRo P D = D.biUnion fun (e : AlonsoOvalleMoghiseh2025b.Entity) => AlonsoOvalleMoghiseh2025b.hamblin P {e}

def AlonsoOvalleMoghiseh2025b.dom {W : Type u_1} [Fintype W] [DecidableEq W] (H : Finset (Finset W)) : Finset W

The worlds where the question's presupposition (8) holds.

Equations

• AlonsoOvalleMoghiseh2025b.dom H = Finset.filter (Question.IsExhaustivelyResolvable (Question.ofFinset H)) Finset.univ

def AlonsoOvalleMoghiseh2025b.ExhP {W : Type u_1} [Fintype W] [DecidableEq W] (φ ψ : Finset (Finset W)) (w : W) : Prop

EXHp (15) holds when φ is defined and every alternative ψ with a stronger presupposition is undefined.

Equations

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

@[instance_reducible]

instance AlonsoOvalleMoghiseh2025b.instDecidableExhP {W : Type u_1} [Fintype W] [DecidableEq W] (φ ψ : Finset (Finset W)) (w : W) : Decidable (ExhP φ ψ w)

Equations

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

The predictions

@[reducible, inline]

abbrev AlonsoOvalleMoghiseh2025b.one : World

The worlds a singular and a plural answer describe.

Equations

• AlonsoOvalleMoghiseh2025b.one = {0}

@[reducible, inline]

abbrev AlonsoOvalleMoghiseh2025b.two : World

Equations

• AlonsoOvalleMoghiseh2025b.two = {0, 1}

def AlonsoOvalleMoghiseh2025b.answers (H : Finset (Finset World)) : Bool × Bool

Whether a singular and a plural answer are available, that is, whether the presupposition (8) holds in the world where one atom was bought and in the world where two were.

Equations

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

def AlonsoOvalleMoghiseh2025b.exhAnswers (φ ψ : Finset (Finset World)) : Bool × Bool

The answers available through EXHp (15) of φ against its alternative ψ.

Equations

• AlonsoOvalleMoghiseh2025b.exhAnswers φ ψ = (decide (AlonsoOvalleMoghiseh2025b.ExhP φ ψ AlonsoOvalleMoghiseh2025b.one), decide (AlonsoOvalleMoghiseh2025b.ExhP φ ψ AlonsoOvalleMoghiseh2025b.two))

theorem AlonsoOvalleMoghiseh2025b.hamblinRo_neutral : hamblinRo bought neutral = Finset.image (fun (e : Entity) => Finset.filter (bought e) Finset.univ) neutral ∧ hamblinRo bought atoms = Finset.image (fun (e : Entity) => Finset.filter (bought e) Finset.univ) atoms

Over a singleton subdomain the meet and the join collapse, so the -ro Hamblin sets of (53) and (55) contain the individual answers only, with the plurality for the neutral domain.

theorem AlonsoOvalleMoghiseh2025b.dayal_english : answers (hamblinRo bought neutral) = (true, true) ∧ answers (hamblinRo bought atoms) = (true, false) ∧ dom (hamblinRo bought atoms) ⊂ dom (hamblinRo bought neutral) ∧ exhAnswers (hamblinRo bought neutral) (hamblinRo bought atoms) = (false, true)

In section 2, English bare interrogatives (9)–(11) allow both answers, singular complex ones (12)–(13) only a singular answer, and plural complex ones (14)–(15), whose singular alternative has the stronger presupposition, only a plural one.

theorem AlonsoOvalleMoghiseh2025b.spanish_gq : answers (hamblinRo bought atoms) = (true, false) ∧ answers (hamblin bought atoms) = (true, true)

In (19), over atoms alone a Spanish singular bare interrogative wrongly presupposes uniqueness, while ranging over their conjunctions and disjunctions admits the plural answer.

theorem AlonsoOvalleMoghiseh2025b.farsi : answers (hamblin bought neutral) = (true, true) ∧ answers (hamblin bought atoms) = (true, true) ∧ answers (hamblinRo bought neutral) = (true, true) ∧ answers (hamblinRo bought atoms) = (true, false)

In (40) and (45) singular bare and complex interrogatives allow both answers, in (53) so does the -ro bare interrogative through the plurality, and in (55) the -ro complex interrogative allows only the singular answer.

Questions with must (30)–(36) and collective predicates (56)–(57)

@[reducible, inline]

abbrev AlonsoOvalleMoghiseh2025b.Base : Type

A deontic world, given by the nonempty set of buy-worlds it permits.

Equations

• AlonsoOvalleMoghiseh2025b.Base = { A : Finset AlonsoOvalleMoghiseh2025b.World // A.Nonempty }

def AlonsoOvalleMoghiseh2025b.permits : SetRel Base World

The accessibility of must, relating a deontic world to the buy-worlds it permits.

Equations

• AlonsoOvalleMoghiseh2025b.permits = SetRel.ofSuccessors fun (A : AlonsoOvalleMoghiseh2025b.Base) => ↑↑A

theorem AlonsoOvalleMoghiseh2025b.permits_singleton (v : World) : ∃ (A : Base), ∀ (u : World), (A, u) ∈ permits ↔ u = v

Every buy-world is the sole world some deontic world permits.

def AlonsoOvalleMoghiseh2025b.freeChoice : Base

The scenario of (59), where Forood must buy one of two things and either is permitted.

Equations

• AlonsoOvalleMoghiseh2025b.freeChoice = ⟨{{0}, {1}}, AlonsoOvalleMoghiseh2025b.freeChoice._proof_1⟩

theorem AlonsoOvalleMoghiseh2025b.modal_gq (D : Finset Entity) : D ∈ [neutral, atoms] → Question.IsExhaustivelyResolvable (Question.box (Question.ofFinset (hamblin bought D)) permits) freeChoice ∧ ¬Question.IsExhaustivelyResolvable (Question.box (Question.ofFinset (hamblinRo bought D)) permits) freeChoice

With the interrogative binding into the scope of must (34), the question is resolvable in the free-choice scenario iff the interrogative ranges over disjunctions, which -ro removes, the contrast between (35)–(36) and (32)–(33) and between (62) and (63).

def AlonsoOvalleMoghiseh2025b.mixed (e : Entity) (w : World) : Prop

Mixed together, a collective predicate true of a plurality that was bought.

Equations

• AlonsoOvalleMoghiseh2025b.mixed e w = (2 ≤ Finset.card e ∧ e ⊆ w)

@[instance_reducible]

instance AlonsoOvalleMoghiseh2025b.instDecidablePredWorldMixed (e : Entity) : DecidablePred (mixed e)

Equations

• AlonsoOvalleMoghiseh2025b.instDecidablePredWorldMixed e w = { decide := decide (2 ≤ Finset.card e) && decide (e ⊆ w), reflects_decide := ⋯ }

theorem AlonsoOvalleMoghiseh2025b.collective : answers (hamblin mixed neutral) = (false, true) ∧ answers (hamblinRo mixed neutral) = (false, true) ∧ answers (hamblin mixed atoms) = (false, false) ∧ answers (hamblinRo mixed atoms) = (false, false)

In (56)–(57) a collective predicate has a true answer over the neutral domain, with or without -ro, and none over the atoms.

The paper's answer judgments

def AlonsoOvalleMoghiseh2025b.hamblinOf (row : Datum) : Option (Finset (Finset World))

The Hamblin set a row's type, ro, and language features name, for the interrogatives the paper derives.

Equations

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

def AlonsoOvalleMoghiseh2025b.predicted (row : Datum) : Option (Bool × Bool)

Whether a singular and a plural answer are predicted, where the English plural complex interrogative goes through EXHp against its singular alternative and the others through ANS.

Equations

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

def AlonsoOvalleMoghiseh2025b.observed (row : Datum) : Bool × Bool

A row's answer judgments, read off its singular answer/plural answer readings.

Equations

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

theorem AlonsoOvalleMoghiseh2025b.rows_agree (row : Datum) : row ∈ Examples.all → ∀ (b : Bool × Bool), predicted row = some b → (row.readings.any fun (r : String × Judgment) => decide ("singular".toList <+: r.1.toList)) = true → observed row = b

Every derived interrogative's answers are those the paper reports.

theorem AlonsoOvalleMoghiseh2025b.scenario_rows (row : Datum) : row ∈ Examples.all → row.feature? "scenario" = some "freeChoice59" → Option.map (fun (H : Finset (Finset World)) => decide (Question.IsExhaustivelyResolvableOn (Question.ofFinset H) ↑↑freeChoice)) (hamblinOf row) = some (row.feature? "verdict" == some "true")

In (60)–(63) the embedded questions are felicitous in (59) iff their interrogative ranges over disjunctions (isExhaustivelyResolvable_box_iff relates this to the question with must).