Farsi Determiner and Indefinite Lexicon

@cite{mirrazi-2024} @cite{alonso-ovalle-moghiseh-2025}

Plain Indefinites (Choice Functions)

Farsi plain indefinites ye (singular), čand-ta (plural classifier "some-CL"), and do-ta (numeral classifier "two-CL") are choice-function indefinites with an independent world/situation variable. @cite{mirrazi-2024} shows that this world variable, when bound by an intensional operator, produces wide pseudo-scope de dicto readings: the indefinite appears to scope above negation (via the ∃-closure over the CF) while remaining de dicto with respect to the intensional operator (via the bound world variable).

EFCI: yek-i

yek-i is an Existential Free Choice Item (EFCI): uniqueness in root, free choice under deontic, modal variation under epistemic. @cite{alonso-ovalle-moghiseh-2025}.

inductive Fragments.Farsi.Determiners.EFCIRescue : Type

EFCI rescue mechanism type. Determines how the item rescues itself from the exhaustification contradiction.

• none : EFCIRescue

  No rescue available (ungrammatical in UE root)

• modalInsertion : EFCIRescue

  Can insert covert epistemic modal

• partialExhaustification : EFCIRescue

  Can do partial exhaustification (prune one alternative type)

• both : EFCIRescue

  Both mechanisms available

@[implicit_reducible]

instance Fragments.Farsi.Determiners.instDecidableEqEFCIRescue : DecidableEq EFCIRescue

Equations

• Fragments.Farsi.Determiners.instDecidableEqEFCIRescue x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Fragments.Farsi.Determiners.instReprEFCIRescue : Repr EFCIRescue

Equations

• Fragments.Farsi.Determiners.instReprEFCIRescue = { reprPrec := Fragments.Farsi.Determiners.instReprEFCIRescue.repr }

def Fragments.Farsi.Determiners.instReprEFCIRescue.repr : EFCIRescue → ℕ → Std.Format

Equations

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

inductive Fragments.Farsi.Determiners.EFCIReading : Type

The reading an EFCI yields in different contexts.

• plainExistential : EFCIReading

  Plain existential (DE contexts)

• uniqueness : EFCIReading

  Exactly one satisfies P (uniqueness)

• freeChoice : EFCIReading

  For each x, it's permitted that P(x)

• modalVariation : EFCIReading

  At least two x's are epistemically possible for P

• epistemicIgnorance : EFCIReading

  Speaker doesn't know/care which x satisfies P

@[implicit_reducible]

instance Fragments.Farsi.Determiners.instDecidableEqEFCIReading : DecidableEq EFCIReading

Equations

• Fragments.Farsi.Determiners.instDecidableEqEFCIReading x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Fragments.Farsi.Determiners.instReprEFCIReading : Repr EFCIReading

Equations

• Fragments.Farsi.Determiners.instReprEFCIReading = { reprPrec := Fragments.Farsi.Determiners.instReprEFCIReading.repr }

def Fragments.Farsi.Determiners.instReprEFCIReading.repr : EFCIReading → ℕ → Std.Format

Equations

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

structure Fragments.Farsi.Determiners.IndefiniteEntry : Type

A Farsi indefinite DP entry.

Captures syntactic and semantic properties including EFCI behavior.

• form : String

  Surface form (Persian script)

• romanization : String

  Romanization

• gloss : String

  Gloss

• isEFCI : Bool

  Is this an EFCI?

• efciRescue : Option EFCIRescue

  EFCI rescue mechanism (if EFCI)

• requiresPartitive : Bool

  Requires partitive 'az' construction?

• allowsMass : Bool

  Can occur with mass nouns?

• speakerIgnorance : Bool

  Conveys speaker ignorance/indifference in root?

• uniqueness : Bool

  Conveys uniqueness in root?

def Fragments.Farsi.Determiners.instReprIndefiniteEntry.repr : IndefiniteEntry → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Fragments.Farsi.Determiners.instReprIndefiniteEntry : Repr IndefiniteEntry

Equations

• Fragments.Farsi.Determiners.instReprIndefiniteEntry = { reprPrec := Fragments.Farsi.Determiners.instReprIndefiniteEntry.repr }

@[implicit_reducible]

instance Fragments.Farsi.Determiners.instBEqIndefiniteEntry : BEq IndefiniteEntry

Equations

• Fragments.Farsi.Determiners.instBEqIndefiniteEntry = { beq := Fragments.Farsi.Determiners.instBEqIndefiniteEntry.beq }

def Fragments.Farsi.Determiners.instBEqIndefiniteEntry.beq : IndefiniteEntry → IndefiniteEntry → Bool

Equations

• One or more equations did not get rendered due to their size.
• Fragments.Farsi.Determiners.instBEqIndefiniteEntry.beq x✝¹ x✝ = false

def Fragments.Farsi.Determiners.yeki : IndefiniteEntry

yek-i: Farsi existential free choice item.

Key properties:

• EFCI with partial exhaustification rescue
• Requires partitive 'az NP' ("one of the NPs")
• Yields uniqueness in root contexts (no modal insertion)
• Yields free choice under deontic modals
• Yields modal variation under epistemic modals
• Plain existential in DE contexts

Equations

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

def Fragments.Farsi.Determiners.yek : IndefiniteEntry

yek (plain numeral): "one"

Not an EFCI - just a numeral. Contrast with yek-i.

Equations

• Fragments.Farsi.Determiners.yek = { form := "یک", romanization := "yek", gloss := "one" }

def Fragments.Farsi.Determiners.indef_i : IndefiniteEntry

Indefinite suffix -i: Indefiniteness marker.

Attaches to nouns to create indefinites.

Equations

• Fragments.Farsi.Determiners.indef_i = { form := "ـی", romanization := "-i", gloss := "-INDF", allowsMass := true }

inductive Fragments.Farsi.Determiners.ModalFlavor : Type

Modal flavor type for context specification.

• deontic : ModalFlavor
• epistemic : ModalFlavor

@[implicit_reducible]

instance Fragments.Farsi.Determiners.instDecidableEqModalFlavor : DecidableEq ModalFlavor

Equations

• Fragments.Farsi.Determiners.instDecidableEqModalFlavor x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Fragments.Farsi.Determiners.instReprModalFlavor.repr : ModalFlavor → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Fragments.Farsi.Determiners.instReprModalFlavor : Repr ModalFlavor

Equations

• Fragments.Farsi.Determiners.instReprModalFlavor = { reprPrec := Fragments.Farsi.Determiners.instReprModalFlavor.repr }

structure Fragments.Farsi.Determiners.EFCIContext : Type

Context for determining EFCI reading.

• isDE : Bool

  Is the context downward-entailing?

• modalFlavor : Option ModalFlavor

  Modal flavor if under a modal

def Fragments.Farsi.Determiners.instReprEFCIContext.repr : EFCIContext → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Fragments.Farsi.Determiners.instReprEFCIContext : Repr EFCIContext

Equations

• Fragments.Farsi.Determiners.instReprEFCIContext = { reprPrec := Fragments.Farsi.Determiners.instReprEFCIContext.repr }

def Fragments.Farsi.Determiners.instBEqEFCIContext.beq : EFCIContext → EFCIContext → Bool

Equations

• Fragments.Farsi.Determiners.instBEqEFCIContext.beq { isDE := a, modalFlavor := a_1 } { isDE := b, modalFlavor := b_1 } = (a == b && a_1 == b_1)
• Fragments.Farsi.Determiners.instBEqEFCIContext.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Fragments.Farsi.Determiners.instBEqEFCIContext : BEq EFCIContext

Equations

• Fragments.Farsi.Determiners.instBEqEFCIContext = { beq := Fragments.Farsi.Determiners.instBEqEFCIContext.beq }

def Fragments.Farsi.Determiners.rootContext : EFCIContext

Root context (no modal, not DE).

Equations

• Fragments.Farsi.Determiners.rootContext = { isDE := false, modalFlavor := none }

def Fragments.Farsi.Determiners.deonticContext : EFCIContext

Deontic modal context.

Equations

• Fragments.Farsi.Determiners.deonticContext = { isDE := false, modalFlavor := some Fragments.Farsi.Determiners.ModalFlavor.deontic }

def Fragments.Farsi.Determiners.epistemicContext : EFCIContext

Epistemic modal context.

Equations

• Fragments.Farsi.Determiners.epistemicContext = { isDE := false, modalFlavor := some Fragments.Farsi.Determiners.ModalFlavor.epistemic }

def Fragments.Farsi.Determiners.deContext : EFCIContext

Downward-entailing context.

Equations

• Fragments.Farsi.Determiners.deContext = { isDE := true, modalFlavor := none }

def Fragments.Farsi.Determiners.getReading (entry : IndefiniteEntry) (ctx : EFCIContext) : Option EFCIReading

Get the reading for an EFCI in a given context.

Equations

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

theorem Fragments.Farsi.Determiners.yeki_root : getReading yeki rootContext = some EFCIReading.uniqueness

Yek-i in root context yields uniqueness

theorem Fragments.Farsi.Determiners.yeki_deontic : getReading yeki deonticContext = some EFCIReading.freeChoice

Yek-i under deontic modal yields free choice

theorem Fragments.Farsi.Determiners.yeki_epistemic : getReading yeki epistemicContext = some EFCIReading.modalVariation

Yek-i under epistemic modal yields modal variation

theorem Fragments.Farsi.Determiners.yeki_de : getReading yeki deContext = some EFCIReading.plainExistential

Yek-i in DE context yields plain existential

def Fragments.Farsi.Determiners.irgendein_de : IndefiniteEntry

German irgendein: EFCI with modal insertion available. Cross-linguistic comparison entry; canonical German entry in Fragments.German.ModalIndefinites. @cite{kratzer-shimoyama-2002}

Equations

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

def Fragments.Farsi.Determiners.vreun_ro : IndefiniteEntry

Romanian vreun: EFCI with no rescue mechanism. Cross-linguistic comparison entry; see @cite{falaus-2014}.

Equations

• Fragments.Farsi.Determiners.vreun_ro = { form := "vreun", romanization := "vreun", gloss := "VREUN", isEFCI := true, efciRescue := some Fragments.Farsi.Determiners.EFCIRescue.none }

theorem Fragments.Farsi.Determiners.irgendein_root : getReading irgendein_de rootContext = some EFCIReading.epistemicIgnorance

Irgendein in root yields epistemic ignorance (via modal insertion). @cite{kratzer-shimoyama-2002}

theorem Fragments.Farsi.Determiners.vreun_root_ungrammatical : getReading vreun_ro rootContext = none

Vreun in root is ungrammatical (no rescue).

structure Fragments.Farsi.Determiners.PlainIndefiniteEntryextends Fragments.Farsi.Determiners.IndefiniteEntry : Type

Farsi plain indefinite entry, extending IndefiniteEntry with choice-function properties relevant to @cite{mirrazi-2024}.

• form : String
• romanization : String
• gloss : String
• isEFCI : Bool
• efciRescue : Option EFCIRescue
• requiresPartitive : Bool
• allowsMass : Bool
• speakerIgnorance : Bool
• uniqueness : Bool
• indefType : Semantics.Quantification.ChoiceFunction.IndefType

  Semantic analysis: choice function or ∃-quantifier.

• hasWorldVar : Bool

  Does this determiner carry an independent world/situation variable? @cite{schwarz-2012}: cross-linguistic parameter — some determiners combine with a world pronoun, others do not.

• isPlural : Bool

  Number: singular or plural.

@[implicit_reducible]

instance Fragments.Farsi.Determiners.instReprPlainIndefiniteEntry : Repr PlainIndefiniteEntry

Equations

• Fragments.Farsi.Determiners.instReprPlainIndefiniteEntry = { reprPrec := Fragments.Farsi.Determiners.instReprPlainIndefiniteEntry.repr }

def Fragments.Farsi.Determiners.instReprPlainIndefiniteEntry.repr : PlainIndefiniteEntry → ℕ → Std.Format

Equations

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

def Fragments.Farsi.Determiners.ye : PlainIndefiniteEntry

ye: Farsi singular indefinite determiner.

Takes wide pseudo-scope de dicto under negated intensional operators. @cite{mirrazi-2024} exx. (1), (4): under negated think, the indefinite is interpreted de dicto (under think) but above negation.

Equations

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

def Fragments.Farsi.Determiners.candTa : PlainIndefiniteEntry

čand-ta: Farsi plural classifier indefinite ("some-CL").

Same scope behavior as ye: wide pseudo-scope de dicto available. @cite{mirrazi-2024} exx. (1), (4): čand-ta alternates with ye in the key examples.

Equations

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

def Fragments.Farsi.Determiners.doTa : PlainIndefiniteEntry

do-ta: Farsi numeral classifier indefinite ("two-CL").

Numeral indefinites behave like other indefinites in their scope-taking properties. @cite{mirrazi-2024} exx. (8a), (9a): under negated necessary and can, do-ta gets wide pseudo-scope de dicto readings.

Equations

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

theorem Fragments.Farsi.Determiners.ye_is_cf : ye.indefType = Semantics.Quantification.ChoiceFunction.IndefType.choiceFunction

All Farsi plain indefinites are choice-functional.

theorem Fragments.Farsi.Determiners.candTa_is_cf : candTa.indefType = Semantics.Quantification.ChoiceFunction.IndefType.choiceFunction

theorem Fragments.Farsi.Determiners.doTa_is_cf : doTa.indefType = Semantics.Quantification.ChoiceFunction.IndefType.choiceFunction

theorem Fragments.Farsi.Determiners.ye_has_world_var : ye.hasWorldVar = true

All Farsi plain indefinites carry a world variable.

theorem Fragments.Farsi.Determiners.candTa_has_world_var : candTa.hasWorldVar = true

theorem Fragments.Farsi.Determiners.doTa_has_world_var : doTa.hasWorldVar = true

def Fragments.Farsi.Determiners.allIndefinites : List IndefiniteEntry

All Farsi indefinite entries

Equations

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

def Fragments.Farsi.Determiners.lookup (romanization : String) : Option IndefiniteEntry

Lookup by romanization

Equations

• Fragments.Farsi.Determiners.lookup romanization = List.find? (fun (e : Fragments.Farsi.Determiners.IndefiniteEntry) => e.romanization == romanization) Fragments.Farsi.Determiners.allIndefinites