Farsi Determiner and Indefinite Lexicon

[Mir24] [AOM25a]

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. [Mir24] 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. [AOM25a].

inductive 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 Farsi.Determiners.instDecidableEqEFCIRescue : DecidableEq EFCIRescue

Equations

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

@[implicit_reducible]

instance Farsi.Determiners.instReprEFCIRescue : Repr EFCIRescue

Equations

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

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

Equations

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

inductive 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 Farsi.Determiners.instDecidableEqEFCIReading : DecidableEq EFCIReading

Equations

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

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

Equations

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

@[implicit_reducible]

instance Farsi.Determiners.instReprEFCIReading : Repr EFCIReading

Equations

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

structure Farsi.Determiners.IndefiniteDeterminer : 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?

@[implicit_reducible]

instance Farsi.Determiners.instReprIndefiniteDeterminer : Repr IndefiniteDeterminer

Equations

• Farsi.Determiners.instReprIndefiniteDeterminer = { reprPrec := Farsi.Determiners.instReprIndefiniteDeterminer.repr }

def Farsi.Determiners.instReprIndefiniteDeterminer.repr : IndefiniteDeterminer → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Farsi.Determiners.instBEqIndefiniteDeterminer : BEq IndefiniteDeterminer

Equations

• Farsi.Determiners.instBEqIndefiniteDeterminer = { beq := Farsi.Determiners.instBEqIndefiniteDeterminer.beq }

def Farsi.Determiners.instBEqIndefiniteDeterminer.beq : IndefiniteDeterminer → IndefiniteDeterminer → Bool

Equations

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

def Farsi.Determiners.yeki : IndefiniteDeterminer

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 Farsi.Determiners.yek : IndefiniteDeterminer

yek (plain numeral): "one"

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

Equations

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

def Farsi.Determiners.indef_i : IndefiniteDeterminer

Indefinite suffix -i: Indefiniteness marker.

Attaches to nouns to create indefinites.

Equations

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

structure Farsi.Determiners.EFCIContext : Type

Context for determining EFCI reading. Uses the project-canonical Semantics.Modality.ModalFlavor; [AOM25a] only distinguishes deontic (free choice) from epistemic (modal variation), so the other canonical flavors are not licensing-relevant here (see getReading).

• isDE : Bool

  Is the context downward-entailing?

• modalFlavor : Option Semantics.Modality.ModalFlavor

  Modal flavor if under a modal

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

Equations

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

@[implicit_reducible]

instance Farsi.Determiners.instReprEFCIContext : Repr EFCIContext

Equations

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

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

Equations

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

@[implicit_reducible]

instance Farsi.Determiners.instBEqEFCIContext : BEq EFCIContext

Equations

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

def Farsi.Determiners.rootContext : EFCIContext

Root context (no modal, not DE).

Equations

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

def Farsi.Determiners.deonticContext : EFCIContext

Deontic modal context.

Equations

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

def Farsi.Determiners.epistemicContext : EFCIContext

Epistemic modal context.

Equations

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

def Farsi.Determiners.deContext : EFCIContext

Downward-entailing context.

Equations

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

def Farsi.Determiners.getReading (entry : IndefiniteDeterminer) (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 Farsi.Determiners.yeki_root : getReading yeki rootContext = some EFCIReading.uniqueness

Yek-i in root context yields uniqueness

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

Yek-i under deontic modal yields free choice

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

Yek-i under epistemic modal yields modal variation

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

Yek-i in DE context yields plain existential

def Farsi.Determiners.irgendein_de : IndefiniteDeterminer

German irgendein: EFCI with modal insertion available. Cross-linguistic comparison entry; canonical German entry in German.ModalIndefinites. [KS17]

Equations

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

def Farsi.Determiners.vreun_ro : IndefiniteDeterminer

Romanian vreun: EFCI with no rescue mechanism. Cross-linguistic comparison entry; see [Fal14].

Equations

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

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

Irgendein in root yields epistemic ignorance (via modal insertion). [KS17]

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

Vreun in root is ungrammatical (no rescue).

structure Farsi.Determiners.PlainIndefiniteEntryextends Farsi.Determiners.IndefiniteDeterminer : Type

Farsi plain indefinite entry, extending IndefiniteDeterminer with choice-function properties relevant to [Mir24].

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

  Semantic analysis: choice function or ∃-quantifier.

• hasWorldVar : Bool

  Does this determiner carry an independent world/situation variable? [Sch12c]: cross-linguistic parameter — some determiners combine with a world pronoun, others do not.

• isPlural : Bool

  Number: singular or plural.

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

Equations

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

@[implicit_reducible]

instance Farsi.Determiners.instReprPlainIndefiniteEntry : Repr PlainIndefiniteEntry

Equations

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

def Farsi.Determiners.ye : PlainIndefiniteEntry

ye: Farsi singular indefinite determiner.

Takes wide pseudo-scope de dicto under negated intensional operators. [Mir24] exx. (1), (4): under negated think, the indefinite is interpreted de dicto (under think) but above negation.

Equations

• Farsi.Determiners.ye = { form := "یه", romanization := "ye", gloss := "some", indefType := Quantification.ChoiceFunction.IndefType.choiceFunction, hasWorldVar := true, isPlural := false }

def Farsi.Determiners.candTa : PlainIndefiniteEntry

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

Same scope behavior as ye: wide pseudo-scope de dicto available. [Mir24] 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 Farsi.Determiners.doTa : PlainIndefiniteEntry

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

Numeral indefinites behave like other indefinites in their scope-taking properties. [Mir24] 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 Farsi.Determiners.ye_is_cf : ye.indefType = Quantification.ChoiceFunction.IndefType.choiceFunction

All Farsi plain indefinites are choice-functional.

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

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

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

All Farsi plain indefinites carry a world variable.

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

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

def Farsi.Determiners.allIndefinites : List IndefiniteDeterminer

All Farsi indefinite entries

Equations

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

def Farsi.Determiners.lookup (romanization : String) : Option IndefiniteDeterminer

Lookup by romanization

Equations

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