structure Phenomena.FreeChoice.FarsiYekI.YekIDatum : Type

A judgment about a Farsi yek-i DP sentence.

• farsi : String

  The Farsi sentence

• gloss : String

  English gloss

• translation : String

  English translation

• contextType : String

  The context type

• modalFlavor : Option String

  The modal flavor (if any)

• primaryReading : String

  Primary reading

• freeChoiceAvailable : Bool

  Is free choice available?

• modalVariationAvailable : Bool

  Is modal variation available?

• uniqueness : Bool

  Is uniqueness conveyed?

• exampleNum : String

  Source example number

instance Phenomena.FreeChoice.FarsiYekI.instReprYekIDatum : Repr YekIDatum

Equations

• Phenomena.FreeChoice.FarsiYekI.instReprYekIDatum = { reprPrec := Phenomena.FreeChoice.FarsiYekI.instReprYekIDatum.repr }

def Phenomena.FreeChoice.FarsiYekI.instReprYekIDatum.repr : YekIDatum → Nat → Std.Format

Equations

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

Root Contexts: Uniqueness

In root contexts without modals, yek-i DPs convey uniqueness: "exactly one individual satisfies the predicate"

This is not a free choice reading; there's no permission or epistemic possibility. The uniqueness is part of the core meaning.

Alonso-Ovalle & Moghiseh argue this comes from exhaustification of domain alternatives (pre-exhaustified), conveying that for most individuals, the predicate does not hold.

def Phenomena.FreeChoice.FarsiYekI.rootUniqueness : YekIDatum

Example (15): Root context with uniqueness

Equations

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

Deontic Modals: Free Choice Effect

Under deontic modals (permission), yek-i DPs yield free choice: "for each individual, it is permitted to VP"

Example: "You may take one of the apples" Reading: You may take this apple, you may take that apple, etc.

def Phenomena.FreeChoice.FarsiYekI.deonticFreeChoice : YekIDatum

Example (17): Deontic free choice

Equations

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

def Phenomena.FreeChoice.FarsiYekI.deonticBooks : YekIDatum

Deontic context with books

Equations

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

Epistemic Modals: Modal Variation Effect

Under epistemic modals, yek-i DPs yield modal variation: "at least two individuals are epistemically possible"

Example: "One of the students might have stolen the book" Reading: It's possible it was this student, it's possible it was that student...

This is weaker than free choice: not every individual is a possibility, but at least two are.

def Phenomena.FreeChoice.FarsiYekI.epistemicModalVariation : YekIDatum

Example (22): Epistemic modal variation

Equations

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

def Phenomena.FreeChoice.FarsiYekI.epistemicExplicit : YekIDatum

Epistemic with explicit modal

Equations

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

DE Contexts: Plain Existential

In downward-entailing contexts (negation, antecedent of conditional), yek-i DPs behave as plain existentials (like English "any"):

"I didn't see one of the students" = "I didn't see any student"

def Phenomena.FreeChoice.FarsiYekI.deNegation : YekIDatum

DE context: negation

Equations

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

def Phenomena.FreeChoice.FarsiYekI.deConditional : YekIDatum

DE context: conditional antecedent

Equations

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

Cross-linguistic Contrast: Yek-i vs Irgendein

An empirical contrast from the paper:

German irgendein in root contexts has a modal component:

• "Irgendjemand hat angerufen" = "Somebody (or other) called"
• Speaker conveys epistemic uncertainty/indifference

Farsi yek-i in root contexts has no modal component:

• "Yek-i zæng zæd" = "Exactly one person called"
• No epistemic uncertainty, just uniqueness

This contrast motivates the typology of rescue mechanisms:

• Irgendein: can insert covert epistemic modal → rescues in root
• Yek-i: cannot insert covert modal → uniqueness only

structure Phenomena.FreeChoice.FarsiYekI.EFCIContrastDatum : Type

EFCI contrast data

• language : String

  The language

• item : String

  The EFCI item

• sentence : String

  Example sentence

• rootReading : String

  Root context reading

• hasModalInRoot : Bool

  Has modal component in root?

• source : String

  Source

def Phenomena.FreeChoice.FarsiYekI.instReprEFCIContrastDatum.repr : EFCIContrastDatum → Nat → Std.Format

Equations

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

instance Phenomena.FreeChoice.FarsiYekI.instReprEFCIContrastDatum : Repr EFCIContrastDatum

Equations

• Phenomena.FreeChoice.FarsiYekI.instReprEFCIContrastDatum = { reprPrec := Phenomena.FreeChoice.FarsiYekI.instReprEFCIContrastDatum.repr }

def Phenomena.FreeChoice.FarsiYekI.irgendeinRoot : EFCIContrastDatum

German irgendein: modal component

Equations

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

def Phenomena.FreeChoice.FarsiYekI.yekiRoot : EFCIContrastDatum

Farsi yek-i: no modal component

Equations

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

def Phenomena.FreeChoice.FarsiYekI.vreunRoot : EFCIContrastDatum

Romanian vreun: ungrammatical in root

Equations

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

Embedded Uniqueness

A distinctive feature of yek-i: uniqueness is preserved even under modals.

"You may take one of the apples" conveys:

1. Free choice: for each apple, you may take it.
2. Uniqueness: but only take one apple total.

This embedded uniqueness comes from exhaustification happening below the modal.

def Phenomena.FreeChoice.FarsiYekI.embeddedUniqueness : YekIDatum

Embedded uniqueness with explicit continuation

Equations

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

def Phenomena.FreeChoice.FarsiYekI.allYekIData : List YekIDatum

All yek-i examples

Equations

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

def Phenomena.FreeChoice.FarsiYekI.efciContrastData : List EFCIContrastDatum

All EFCI contrast data

Equations

• Phenomena.FreeChoice.FarsiYekI.efciContrastData = [Phenomena.FreeChoice.FarsiYekI.irgendeinRoot, Phenomena.FreeChoice.FarsiYekI.yekiRoot, Phenomena.FreeChoice.FarsiYekI.vreunRoot]

inductive Phenomena.FreeChoice.FarsiYekI.EFCIType : Type

EFCI rescue mechanism typology from @cite{alonso-ovalle-moghiseh-2025}.

• vreun : EFCIType

  Neither rescue mechanism (e.g., Romanian vreun)

• irgendein : EFCIType

  Modal insertion available (e.g., German irgendein)

• yeki : EFCIType

  Partial exhaustification available (e.g., Farsi yek-i)

instance Phenomena.FreeChoice.FarsiYekI.instDecidableEqEFCIType : DecidableEq EFCIType

Equations

• Phenomena.FreeChoice.FarsiYekI.instDecidableEqEFCIType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.FreeChoice.FarsiYekI.instBEqEFCIType : BEq EFCIType

Equations

• Phenomena.FreeChoice.FarsiYekI.instBEqEFCIType = { beq := Phenomena.FreeChoice.FarsiYekI.instBEqEFCIType.beq }

def Phenomena.FreeChoice.FarsiYekI.instBEqEFCIType.beq : EFCIType → EFCIType → Bool

Equations

• Phenomena.FreeChoice.FarsiYekI.instBEqEFCIType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.FreeChoice.FarsiYekI.instReprEFCIType.repr : EFCIType → Nat → Std.Format

Equations

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

instance Phenomena.FreeChoice.FarsiYekI.instReprEFCIType : Repr EFCIType

Equations

• Phenomena.FreeChoice.FarsiYekI.instReprEFCIType = { reprPrec := Phenomena.FreeChoice.FarsiYekI.instReprEFCIType.repr }

structure Phenomena.FreeChoice.FarsiYekI.EFCITypologyDatum : Type

EFCI typology data

• efciType : EFCIType

  The EFCI type

• language : String

  Example language

• item : String

  The item

• canInsertModal : Bool

  Can insert covert modal?

• canPartialExh : Bool

  Can do partial exhaustification?

• grammaticalInRoot : Bool

  Grammatical in root contexts?

• rootReading : String

  Root context reading

def Phenomena.FreeChoice.FarsiYekI.instReprEFCITypologyDatum.repr : EFCITypologyDatum → Nat → Std.Format

Equations

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

instance Phenomena.FreeChoice.FarsiYekI.instReprEFCITypologyDatum : Repr EFCITypologyDatum

Equations

• Phenomena.FreeChoice.FarsiYekI.instReprEFCITypologyDatum = { reprPrec := Phenomena.FreeChoice.FarsiYekI.instReprEFCITypologyDatum.repr }

def Phenomena.FreeChoice.FarsiYekI.vreunTypology : EFCITypologyDatum

vreun-type: neither rescue

Equations

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

def Phenomena.FreeChoice.FarsiYekI.irgendeinTypology : EFCITypologyDatum

irgendein-type: modal insertion

Equations

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

def Phenomena.FreeChoice.FarsiYekI.yekiTypology : EFCITypologyDatum

yek-i-type: partial exhaustification only

Equations

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

def Phenomena.FreeChoice.FarsiYekI.efciTypology : List EFCITypologyDatum

Full EFCI typology

Equations

• Phenomena.FreeChoice.FarsiYekI.efciTypology = [Phenomena.FreeChoice.FarsiYekI.vreunTypology, Phenomena.FreeChoice.FarsiYekI.irgendeinTypology, Phenomena.FreeChoice.FarsiYekI.yekiTypology]