Alonso-Ovalle & Moghiseh (2025): Number Marking in What Interrogatives

@cite{alonso-ovalle-moghiseh-2025b}

Luis Alonso-Ovalle and Esmail Moghiseh. Number marking in interrogative phrases: What interrogatives in Farsi. In: Proceedings of Sinn und Bedeutung 29, pp. 1–16.

Overview

Farsi what interrogatives display a distinctive number-marking pattern: singular what CIs (che ketab-i, "what book") allow both singular and plural answers, unlike English where singular CIs restrict to singular answers only. This divergence is derived from four assumptions:

1. Interrogatives range over generalized quantifiers — conjunctions (⊓) and disjunctions (⊔) built from non-empty subsets of an entity domain (@cite{xiang-2016}, @cite{elliott-nicolae-sauerland-2022}).
2. Singular marking on bare interrogatives is a morphological default with no semantic import (@cite{maldonado-2020}).
3. Singular marking on complex interrogatives has semantic import: SING restricts the domain to atoms (@cite{scontras-2022}).
4. Differential object marker -ro restricts the subset selection function to singletons, signaling specificity (@cite{karimi-2003}).

Predictions

Type	±ro	Sg	Pl	Ex.
SBI	−	✓	✓	20
PBI	−	✗	✓	21
SCI	−	✓	✓	23
PCI	−	✗	✓	25
SBI	+	✓	✓	26
SCI	+	✓	✗	27
PCI	+	✗	✓	28

Connection to yek-i DPs

Farsi interrogative forms (chi, che) are homophonous with indefinites (@cite{alonso-ovalle-moghiseh-2025}, §5). The interrogative and indefinite share the same domain-building mechanism (⊓ ∪ ⊔ over GQs), but interrogatives compose with ANS while indefinites compose with existential closure. See Fragments.Farsi.Determiners and Phenomena.FreeChoice.FarsiYekI for the indefinite paradigm.

inductive AlonsoOvalleMoghiseh2025b.Entity : Type

Entity domain: two atomic individuals and their mereological join. t12 = t1 ⊕ t2 in the sense of @cite{link-1983}.

• t1 : Entity
• t2 : Entity
• t12 : Entity

@[implicit_reducible]

instance AlonsoOvalleMoghiseh2025b.instDecidableEqEntity : DecidableEq Entity

Equations

• AlonsoOvalleMoghiseh2025b.instDecidableEqEntity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance AlonsoOvalleMoghiseh2025b.instBEqEntity : BEq Entity

Equations

• AlonsoOvalleMoghiseh2025b.instBEqEntity = { beq := AlonsoOvalleMoghiseh2025b.instBEqEntity.beq }

def AlonsoOvalleMoghiseh2025b.instBEqEntity.beq : Entity → Entity → Bool

Equations

• AlonsoOvalleMoghiseh2025b.instBEqEntity.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def AlonsoOvalleMoghiseh2025b.instReprEntity.repr : Entity → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance AlonsoOvalleMoghiseh2025b.instReprEntity : Repr Entity

Equations

• AlonsoOvalleMoghiseh2025b.instReprEntity = { reprPrec := AlonsoOvalleMoghiseh2025b.instReprEntity.repr }

inductive AlonsoOvalleMoghiseh2025b.World : Type

Evaluation worlds: what did Roya buy?

• w1 : World
• w2 : World
• w12 : World

@[implicit_reducible]

instance AlonsoOvalleMoghiseh2025b.instDecidableEqWorld : DecidableEq World

Equations

• AlonsoOvalleMoghiseh2025b.instDecidableEqWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def AlonsoOvalleMoghiseh2025b.instBEqWorld.beq : World → World → Bool

Equations

• AlonsoOvalleMoghiseh2025b.instBEqWorld.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance AlonsoOvalleMoghiseh2025b.instBEqWorld : BEq World

Equations

• AlonsoOvalleMoghiseh2025b.instBEqWorld = { beq := AlonsoOvalleMoghiseh2025b.instBEqWorld.beq }

def AlonsoOvalleMoghiseh2025b.instReprWorld.repr : World → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance AlonsoOvalleMoghiseh2025b.instReprWorld : Repr World

Equations

• AlonsoOvalleMoghiseh2025b.instReprWorld = { reprPrec := AlonsoOvalleMoghiseh2025b.instReprWorld.repr }

def AlonsoOvalleMoghiseh2025b.allEntities : List Entity

Equations

• AlonsoOvalleMoghiseh2025b.allEntities = [AlonsoOvalleMoghiseh2025b.Entity.t1, AlonsoOvalleMoghiseh2025b.Entity.t2, AlonsoOvalleMoghiseh2025b.Entity.t12]

def AlonsoOvalleMoghiseh2025b.allWorlds : List World

Equations

• AlonsoOvalleMoghiseh2025b.allWorlds = [AlonsoOvalleMoghiseh2025b.World.w1, AlonsoOvalleMoghiseh2025b.World.w2, AlonsoOvalleMoghiseh2025b.World.w12]

def AlonsoOvalleMoghiseh2025b.isAtom : Entity → Prop

Mereological atom predicate. Corresponds to [+atomic] in @cite{harbour-2014} (Features.Number) and Mereology.Atom.

Equations

• AlonsoOvalleMoghiseh2025b.isAtom AlonsoOvalleMoghiseh2025b.Entity.t1 = True
• AlonsoOvalleMoghiseh2025b.isAtom AlonsoOvalleMoghiseh2025b.Entity.t2 = True
• AlonsoOvalleMoghiseh2025b.isAtom AlonsoOvalleMoghiseh2025b.Entity.t12 = False

@[implicit_reducible]

instance AlonsoOvalleMoghiseh2025b.instDecidablePredEntityIsAtom : DecidablePred isAtom

Equations

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

def AlonsoOvalleMoghiseh2025b.bought : Entity → World → Bool

Distributive predicate: bought(e, roya, w). Distributivity: bought t12 w = bought t1 w ∧ bought t2 w.

Equations

• AlonsoOvalleMoghiseh2025b.bought AlonsoOvalleMoghiseh2025b.Entity.t1 AlonsoOvalleMoghiseh2025b.World.w1 = true
• AlonsoOvalleMoghiseh2025b.bought AlonsoOvalleMoghiseh2025b.Entity.t1 AlonsoOvalleMoghiseh2025b.World.w12 = true
• AlonsoOvalleMoghiseh2025b.bought AlonsoOvalleMoghiseh2025b.Entity.t2 AlonsoOvalleMoghiseh2025b.World.w2 = true
• AlonsoOvalleMoghiseh2025b.bought AlonsoOvalleMoghiseh2025b.Entity.t2 AlonsoOvalleMoghiseh2025b.World.w12 = true
• AlonsoOvalleMoghiseh2025b.bought AlonsoOvalleMoghiseh2025b.Entity.t12 AlonsoOvalleMoghiseh2025b.World.w12 = true
• AlonsoOvalleMoghiseh2025b.bought x✝¹ x✝ = false

theorem AlonsoOvalleMoghiseh2025b.bought_distributive (w : World) : bought Entity.t12 w = (bought Entity.t1 w && bought Entity.t2 w)

Distributivity holds for the join entity at all worlds.

The GQ generators conjGQs/disjGQs and their underlying lattice operations (conjGQ/disjGQ) are imported from Core.Logic.Quantification.Generators, where they are defined as iterated meets/joins of Montagovian individual quantifiers.

- `conjGQ X P = X.all P` — universal quantification over X
- `disjGQ X P = X.any P` — existential quantification over X
- `conjGQs dom` — all ⊓(X) for ∅ ≠ X ⊆ dom (@cite{xiang-2016})
- `disjGQs dom` — all ⊔(X) for ∅ ≠ X ⊆ dom 

def AlonsoOvalleMoghiseh2025b.hamblinSet (dom : List Entity) : List (World → Bool)

Hamblin set: propositions from applying each GQ in ⊓(dom) ∪ ⊔(dom) to the VP bought. Implements eq. (29) for the buy predicate.

⟦Q⟧(dom) = {λw. Q(λe. bought(e, w)) | Q ∈ ⊓(dom) ∪ ⊔(dom)}

Since NPQ Entity = (Entity → Prop) → Prop, we use the propositional characterization conjGQ_iff_forall / disjGQ_iff_exists to compute a Bool result from the Bool predicate bought.

Equations

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

def AlonsoOvalleMoghiseh2025b.hamblinSetRo (dom : List Entity) : List (World → Bool)

Hamblin set with -ro: restricted to singleton subsets (eq. 52). -ro imposes |f(P)| = 1, so each entity contributes exactly one proposition, eliminating conjunctive and disjunctive GQs.

Also serves as the individual-level Hamblin set for EXH_P competition: the singular alternative ranges over individual GQs (singletons), which is exactly what -ro does. The coincidence is structural — both operations restrict to |X| = 1.

Equations

• AlonsoOvalleMoghiseh2025b.hamblinSetRo dom = List.map (fun (e : AlonsoOvalleMoghiseh2025b.Entity) (w : AlonsoOvalleMoghiseh2025b.World) => AlonsoOvalleMoghiseh2025b.bought e w) dom

def AlonsoOvalleMoghiseh2025b.entails (p q : World → Bool) : Bool

Propositional entailment over the finite world set.

Equations

• AlonsoOvalleMoghiseh2025b.entails p q = AlonsoOvalleMoghiseh2025b.allWorlds.all fun (w : AlonsoOvalleMoghiseh2025b.World) => !p w || q w

def AlonsoOvalleMoghiseh2025b.epHolds (hamblin : List (World → Bool)) (w : World) : Bool

Dayal's Exhaustivity Presupposition: does ANS find a strongest true answer at w? (@cite{dayal-1996}, eq. 8)

EP(H, w) = ∃p ∈ H. p(w) ∧ ∀q ∈ H. q(w) → p ⊆ q

Corresponds to dayalEP in Theories.Semantics.Questions.Exhaustivity.

Equations

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

def AlonsoOvalleMoghiseh2025b.exhPAntiUniq (singularIndivH : List (World → Bool)) (w : World) : Bool

EXH_P anti-uniqueness (@cite{marty-2017}, @cite{elliott-sauerland-2019}, eq. 15). For plural interrogatives competing with singular alternatives: the question is felicitous at w only if more than one individual-level proposition in the singular alternative's Hamblin set is true.

Connects to pexIEII in Theories.Semantics.Exhaustification.Presuppositional.

Equations

• AlonsoOvalleMoghiseh2025b.exhPAntiUniq singularIndivH w = decide ((List.filter (fun (x : AlonsoOvalleMoghiseh2025b.World → Bool) => x w) singularIndivH).length > 1)

def AlonsoOvalleMoghiseh2025b.biDomain : List Entity

BI domain: atoms + pluralities. Singular marking on BIs is a default with no semantic import (§4, assumption 2).

Equations

• AlonsoOvalleMoghiseh2025b.biDomain = AlonsoOvalleMoghiseh2025b.allEntities

def AlonsoOvalleMoghiseh2025b.ciDomain : List Entity

CI domain: atoms only. ⟦SING⟧ = λP.λx: ATOM(x). P(x) (eq. 42, @cite{scontras-2022}). Implements the semantic content of singular marking on CIs.

Equations

• AlonsoOvalleMoghiseh2025b.ciDomain = List.filter (fun (e : AlonsoOvalleMoghiseh2025b.Entity) => decide (AlonsoOvalleMoghiseh2025b.isAtom e)) AlonsoOvalleMoghiseh2025b.allEntities

The model's predictions derive from three structural facts about propositional entailment under the bought predicate:

1. **Conjunction strength**: ⊓({t1,t2}) yields B(t1) ∧ B(t2), which
   entails both B(t1) and B(t2). This creates strongest answers at
   plural worlds — the mechanism behind Farsi SCIs accepting plurals.

2. **Atomic independence**: B(t1) and B(t2) are logically independent.
   Without conjunction GQs, no strongest answer exists at plural worlds.

3. **Singleton absorption**: At singular worlds (one atom bought),
   the unique true atomic proposition entails every true disjunction
   (by disjunction introduction), so EP always holds.

The entailment facts in (1) and (3) are derived from the lattice
structure of GQ generators in `Core.Logic.Quantification.Generators`:
- `conjGQ_le_individual`: ⊓(X) ≤ individual(a) for a ∈ X
- `individual_le_disjGQ`: individual(a) ≤ ⊔(X) for a ∈ X
- `conjGQ_le_disjGQ'`: ⊓(X) ≤ ⊔(X) for non-empty X

The bridge `npq_le_entails` lifts NPQ lattice `≤` to the study's
propositional `entails`, connecting the abstract lattice structure
to the concrete model. 

theorem AlonsoOvalleMoghiseh2025b.atoms_independent : entails (bought Entity.t1) (bought Entity.t2) = false ∧ entails (bought Entity.t2) (bought Entity.t1) = false

B(t1) and B(t2) are logically independent.

• w1 witnesses B(t1) ⊬ B(t2): Roya bought t1 but not t2
• w2 witnesses B(t2) ⊬ B(t1): Roya bought t2 but not t1 This is why EP fails for individual-only Hamblin sets at w12: neither individual proposition can serve as the strongest true answer.

theorem AlonsoOvalleMoghiseh2025b.conj_entails_atoms : entails (fun (w : World) => bought Entity.t1 w && bought Entity.t2 w) (bought Entity.t1) = true ∧ entails (fun (w : World) => bought Entity.t1 w && bought Entity.t2 w) (bought Entity.t2) = true

B(t1) ∧ B(t2) entails each atom individually (conjunction elimination). Structural proof: ⊓({t1,t2}) ≤ individual(tᵢ) in the NPQ lattice (conjGQ_le_individual), lifted to propositional entailment via npq_le_entails.

theorem AlonsoOvalleMoghiseh2025b.atom_entails_containing_disj : (entails (bought Entity.t1) fun (w : World) => bought Entity.t1 w || bought Entity.t2 w) = true ∧ (entails (bought Entity.t1) fun (w : World) => bought Entity.t1 w || bought Entity.t12 w) = true

B(t1) entails any disjunction containing it (disjunction introduction). Structural proof: individual(t1) ≤ ⊔(X) for t1 ∈ X in the NPQ lattice (individual_le_disjGQ), lifted to propositional entailment.

theorem AlonsoOvalleMoghiseh2025b.conj_entails_disj : (entails (fun (w : World) => bought Entity.t1 w && bought Entity.t2 w) fun (w : World) => bought Entity.t1 w || bought Entity.t2 w) = true

The conjunction also entails the disjunction of its conjuncts. Structural proof: ⊓(X) ≤ ⊔(X) for non-empty X (conjGQ_le_disjGQ'), lifted to propositional entailment. Combined with conj_entails_atoms, this makes ⊓({t1,t2}) the strongest element in any Hamblin set built from {t1, t2}.

theorem AlonsoOvalleMoghiseh2025b.ep_gq_atoms_w12 : epHolds (hamblinSet ciDomain) World.w12 = true

EP holds at w12 for GQ-ranging over atoms: ⊓({t1,t2}) = B(t1) ∧ B(t2) is true at w12 and entails every other proposition in the Hamblin set (by conj_entails_atoms and conj_entails_disj).

theorem AlonsoOvalleMoghiseh2025b.ep_indiv_atoms_w12 : epHolds (hamblinSetRo ciDomain) World.w12 = false

EP fails at w12 for individual-ranging over atoms: the Hamblin set is {B(t1), B(t2)}, both true at w12, but independent by atoms_independent. Neither can be strongest → no ANS → EP fails. This is the English SCI pattern.

theorem AlonsoOvalleMoghiseh2025b.ep_at_singular_world : epHolds (hamblinSet biDomain) World.w1 = true ∧ epHolds (hamblinSet ciDomain) World.w1 = true ∧ epHolds (hamblinSetRo biDomain) World.w1 = true ∧ epHolds (hamblinSetRo ciDomain) World.w1 = true

At w1 (only t1 bought), EP holds for any Hamblin set containing B(t1). B(t1) is the unique true atomic proposition, and it entails every true disjunction via atom_entails_containing_disj. The proof covers both the full GQ Hamblin set and the individual Hamblin set.

theorem AlonsoOvalleMoghiseh2025b.ep_gq_full_w12 : epHolds (hamblinSet biDomain) World.w12 = true

At w12 (both atoms bought), EP holds for GQ-ranging over the full domain: ⊓({t1,t2,t12}) = B(t1) ∧ B(t2) ∧ B(t12) is the strongest true proposition (entails all others by conjunction elimination).

theorem AlonsoOvalleMoghiseh2025b.antiUniq_w1 : exhPAntiUniq (hamblinSetRo biDomain) World.w1 = false ∧ exhPAntiUniq (hamblinSetRo ciDomain) World.w1 = false

Anti-uniqueness at w1: only one individual proposition true (B(t1)), so the count is 1, not > 1. Plural marking's presupposition fails → singular answer blocked for all PL-marked interrogatives at w1.

theorem AlonsoOvalleMoghiseh2025b.antiUniq_w12 : exhPAntiUniq (hamblinSetRo biDomain) World.w12 = true ∧ exhPAntiUniq (hamblinSetRo ciDomain) World.w12 = true

Anti-uniqueness at w12: both B(t1) and B(t2) true (count = 2 > 1). Plural marking's presupposition holds → plural answers allowed.

inductive AlonsoOvalleMoghiseh2025b.IntType : Type

The seven interrogative configurations from the Farsi paradigm.

• sbi : IntType
• pbi : IntType
• sci : IntType
• pci : IntType
• sbiRo : IntType
• sciRo : IntType
• pciRo : IntType

@[implicit_reducible]

instance AlonsoOvalleMoghiseh2025b.instDecidableEqIntType : DecidableEq IntType

Equations

• AlonsoOvalleMoghiseh2025b.instDecidableEqIntType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def AlonsoOvalleMoghiseh2025b.instBEqIntType.beq : IntType → IntType → Bool

Equations

• AlonsoOvalleMoghiseh2025b.instBEqIntType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance AlonsoOvalleMoghiseh2025b.instBEqIntType : BEq IntType

Equations

• AlonsoOvalleMoghiseh2025b.instBEqIntType = { beq := AlonsoOvalleMoghiseh2025b.instBEqIntType.beq }

def AlonsoOvalleMoghiseh2025b.instReprIntType.repr : IntType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance AlonsoOvalleMoghiseh2025b.instReprIntType : Repr IntType

Equations

• AlonsoOvalleMoghiseh2025b.instReprIntType = { reprPrec := AlonsoOvalleMoghiseh2025b.instReprIntType.repr }

def AlonsoOvalleMoghiseh2025b.predictSg : IntType → Bool

Predicted singular answer availability. For base types, singular = EP holds at w1 (a world where one atom bought). For plural types, additionally requires EXH_P anti-uniqueness.

Equations

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

def AlonsoOvalleMoghiseh2025b.predictPl : IntType → Bool

Predicted plural answer availability. Plural = EP holds at w12 (a world where both atoms bought).

Equations

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

Each prediction derives from the structural lemmas in § 5. The proofs explicitly chain the relevant structural facts via simp only.

### Bare Interrogatives

BIs range over GQs from the FULL entity domain (atoms + pluralities).
Singular marking on BIs is a morphological default (no semantic import). 

theorem AlonsoOvalleMoghiseh2025b.sbi_singular : predictSg IntType.sbi = true

SBI (chi, what.SG): allows singular answers. (ex. 20a) EP holds at w1 by ep_at_singular_world: B(t1) is the strongest true answer in the full GQ Hamblin set.

theorem AlonsoOvalleMoghiseh2025b.sbi_plural : predictPl IntType.sbi = true

SBI: allows plural answers. (ex. 20b) EP holds at w12 by ep_gq_full_w12: ⊓({t1,t2,t12}) produces a conjunction proposition that entails all others.

theorem AlonsoOvalleMoghiseh2025b.pbi_blocks_singular : predictSg IntType.pbi = false

PBI (chi-a, what.PL): blocks singular via EXH_P. (ex. 21a) EP itself holds at w1 (ep_at_singular_world), but EXH_P anti-uniqueness fails: only B(t1) is true among individual propositions at w1 (antiUniq_w1), so count = 1, not > 1.

theorem AlonsoOvalleMoghiseh2025b.pbi_plural : predictPl IntType.pbi = true

PBI: allows plural. (ex. 21b) EP holds at w12 (ep_gq_full_w12) and anti-uniqueness holds (antiUniq_w12): both B(t1) and B(t2) true → count = 2 > 1.

Complex Interrogatives

CIs range over GQs from the ATOM domain ({t1, t2}).
SING restricts the domain to atoms — this is the semantic content
of singular marking on CIs, unlike BIs where it's vacuous. 

theorem AlonsoOvalleMoghiseh2025b.sci_singular : predictSg IntType.sci = true

SCI (che ketab-i, what book.SG.INDEF): allows singular. (ex. 23a) EP holds at w1 by ep_at_singular_world.

theorem AlonsoOvalleMoghiseh2025b.sci_plural : predictPl IntType.sci = true

SCI: allows plural answers — the key Farsi innovation. (ex. 23b) Unlike English SCIs (individual-ranging → independent propositions → EP fails at plural worlds by atoms_independent), Farsi SCIs range over GQs. The conjunction GQ ⊓({t1, t2}) produces B(t1) ∧ B(t2), which entails both atomic propositions (conj_entails_atoms) and the disjunction (conj_entails_disj) → EP holds by ep_gq_atoms_w12.

theorem AlonsoOvalleMoghiseh2025b.pci_blocks_singular : predictSg IntType.pci = false

PCI (che ketab-a-i, what book.PL.INDEF): blocks singular. (ex. 25a) EP holds but anti-uniqueness fails at w1 (antiUniq_w1).

theorem AlonsoOvalleMoghiseh2025b.pci_plural : predictPl IntType.pci = true

PCI: allows plural. (ex. 25b) EP holds at w12 and anti-uniqueness holds (antiUniq_w12).

With Differential Object Marker -ro

*-ro* restricts the selection function to singletons, eliminating
conjunctive and disjunctive GQs. The Hamblin set reduces to
individual propositions {B(e) | e ∈ dom}. 

theorem AlonsoOvalleMoghiseh2025b.sbi_ro_singular : predictSg IntType.sbiRo = true

SBI + -ro (chi ro): allows singular. (ex. 26a) EP holds at w1 by ep_at_singular_world.

theorem AlonsoOvalleMoghiseh2025b.sbi_ro_plural : predictPl IntType.sbiRo = true

SBI + -ro: allows plural. (ex. 26b) BI domain includes t12, so the Hamblin set is {B(t1), B(t2), B(t12)}. B(t12) = B(t1) ∧ B(t2) by distributivity (bought_distributive), so at w12 it entails both → EP holds.

theorem AlonsoOvalleMoghiseh2025b.sci_ro_singular : predictSg IntType.sciRo = true

SCI + -ro (che ketab-i ro): allows singular. (ex. 27a) EP holds at w1 by ep_at_singular_world.

theorem AlonsoOvalleMoghiseh2025b.sci_ro_blocks_plural : predictPl IntType.sciRo = false

SCI + -ro: blocks plural. (ex. 27b) SING restricts domain to atoms {t1, t2}. -ro restricts to singletons, giving Hamblin = {B(t1), B(t2)}. At w12: both true but neither entails the other (atoms_independent) → EP fails (ep_indiv_atoms_w12). This recovers the English SCI pattern, only with -ro.

theorem AlonsoOvalleMoghiseh2025b.pci_ro_blocks_singular : predictSg IntType.pciRo = false

PCI + -ro (che ketab-a-i ro): blocks singular. (ex. 28a) EP holds at w1 but anti-uniqueness fails (antiUniq_w1).

theorem AlonsoOvalleMoghiseh2025b.pci_ro_plural : predictPl IntType.pciRo = true

PCI + -ro: allows plural. (ex. 28b) EP holds at w12 (BI domain includes t12, giving strongest answer) and anti-uniqueness holds (antiUniq_w12).

theorem AlonsoOvalleMoghiseh2025b.full_paradigm : [predictSg IntType.sbi, !predictSg IntType.pbi, predictSg IntType.sci, !predictSg IntType.pci, predictSg IntType.sbiRo, predictSg IntType.sciRo, !predictSg IntType.pciRo, predictPl IntType.sbi, predictPl IntType.pbi, predictPl IntType.sci, predictPl IntType.pci, predictPl IntType.sbiRo, !predictPl IntType.sciRo, predictPl IntType.pciRo].all id = true

All 14 predictions verified in aggregate. Each case is proved individually above via structural lemmas; this theorem confirms they compose correctly into the full paradigm table.

theorem AlonsoOvalleMoghiseh2025b.ciDomain_is_atoms : ciDomain = List.filter (fun (e : Entity) => decide (isAtom e)) allEntities

CI domain = atom filter of all entities. Connects SING (eq. 42) to Features.Number.Category.singular ([+atomic]).

theorem AlonsoOvalleMoghiseh2025b.farsi_vs_english : epHolds (hamblinSet ciDomain) World.w12 = true ∧ epHolds (hamblinSetRo ciDomain) World.w12 = false

The Farsi/English SCI divergence in one theorem. Both use atoms-only domain (SING). The difference: Farsi ranges over GQs (hamblinSet), English over individuals (hamblinSetRo). Only GQ-ranging allows plural answers at w12.

Farsi side: ⊓({t1,t2}) creates B(t1)∧B(t2), which entails both B(t1) and B(t2) (conj_entails_atoms) → strongest answer → EP holds. English side: {B(t1), B(t2)} are independent (atoms_independent) → no strongest answer → EP fails.

theorem AlonsoOvalleMoghiseh2025b.ro_eliminates_disjunction : have disj := fun (w : World) => bought Entity.t1 w || bought Entity.t2 w; ((hamblinSet biDomain).any fun (p : World → Bool) => allWorlds.all fun (w : World) => p w == disj w) = true ∧ ((hamblinSetRo biDomain).any fun (p : World → Bool) => allWorlds.all fun (w : World) => p w == disj w) = false

-ro eliminates disjunctive propositions from the Hamblin set, blocking free choice interpretations (§4, eqs. 62–63).

Full Hamblin set includes ⊔({t1,t2}) = B(t1) ∨ B(t2), which enables free choice readings. -ro restricts to singletons, so only B(t1), B(t2), B(t12) remain — no disjunctions.

theorem AlonsoOvalleMoghiseh2025b.hamblinSet_decomposition (dom : List Entity) (w : World) (p : World → Bool) : p ∈ hamblinSet dom → ∃ X ∈ Core.Quantification.nonemptySubsets dom, (p w = true ↔ Core.Quantification.conjGQ X fun (e : Entity) => bought e w = true) ∨ (p w = true ↔ Core.Quantification.disjGQ X fun (e : Entity) => bought e w = true)

The Hamblin set decomposes into conjGQ and disjGQ applications. Each proposition in hamblinSet dom is conjGQ X (bought · w) or disjGQ X (bought · w) for some non-empty X ⊆ dom. This connects the study's concrete Hamblin set to the lattice-theoretic GQ generators in Core.Logic.Quantification.Generators.

theorem AlonsoOvalleMoghiseh2025b.plurality_via_gq : have bt12 := fun (w : World) => bought Entity.t12 w; have conjt1t2 := fun (w : World) => bought Entity.t1 w && bought Entity.t2 w; (allWorlds.all fun (w : World) => bt12 w == conjt1t2 w) = true

B(t12) is extensionally equivalent to B(t1) ∧ B(t2): the mereological join's predicate equals the conjunction of its parts. This follows from distributivity (bought_distributive) and is how plural answers arise even from the BI individual Hamblin set: the -ro Hamblin set over biDomain includes B(t12), which is the conjunction proposition in disguise.

structure AlonsoOvalleMoghiseh2025b.Datum : Type

Farsi interrogative datum with acceptability judgment.

• farsi : String
• gloss : String
• intType : IntType
• singularOk : Bool
• pluralOk : Bool
• exNum : String

@[implicit_reducible]

instance AlonsoOvalleMoghiseh2025b.instReprDatum : Repr Datum

Equations

• AlonsoOvalleMoghiseh2025b.instReprDatum = { reprPrec := AlonsoOvalleMoghiseh2025b.instReprDatum.repr }

def AlonsoOvalleMoghiseh2025b.instReprDatum.repr : Datum → ℕ → Std.Format

Equations

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

def AlonsoOvalleMoghiseh2025b.data : List Datum

Equations

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

theorem AlonsoOvalleMoghiseh2025b.data_consistent : (data.all fun (d : Datum) => d.singularOk == predictSg d.intType && d.pluralOk == predictPl d.intType) = true

Every datum's acceptability judgment matches the model's prediction. Each per-datum check is verified structurally in § 7; this aggregates them as a single data consistency check.