Farsi Determiner and Indefinite Lexicon

yek-i as EFCI: uniqueness in root, free choice under deontic, modal variation under epistemic.

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

instance Fragments.Farsi.Determiners.instDecidableEqEFCIRescue : DecidableEq EFCIRescue

Equations

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

def Fragments.Farsi.Determiners.instBEqEFCIRescue.beq : EFCIRescue → EFCIRescue → Bool

Equations

• Fragments.Farsi.Determiners.instBEqEFCIRescue.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.Farsi.Determiners.instBEqEFCIRescue : BEq EFCIRescue

Equations

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

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

instance Fragments.Farsi.Determiners.instDecidableEqEFCIReading : DecidableEq EFCIReading

Equations

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

instance Fragments.Farsi.Determiners.instBEqEFCIReading : BEq EFCIReading

Equations

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

def Fragments.Farsi.Determiners.instBEqEFCIReading.beq : EFCIReading → EFCIReading → Bool

Equations

• Fragments.Farsi.Determiners.instBEqEFCIReading.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

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?

instance Fragments.Farsi.Determiners.instReprIndefiniteEntry : Repr IndefiniteEntry

Equations

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

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

Equations

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

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

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.instBEqModalFlavor.beq : ModalFlavor → ModalFlavor → Bool

Equations

• Fragments.Farsi.Determiners.instBEqModalFlavor.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.Farsi.Determiners.instBEqModalFlavor : BEq ModalFlavor

Equations

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

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

Equations

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

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

instance Fragments.Farsi.Determiners.instReprEFCIContext : Repr EFCIContext

Equations

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

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

Equations

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

instance Fragments.Farsi.Determiners.instBEqEFCIContext : BEq EFCIContext

Equations

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

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

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.

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.

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.uniqueness

Irgendein in root yields epistemic ignorance (or uniqueness with partial exh).

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

Vreun in root is ungrammatical (no rescue).

def Fragments.Farsi.Determiners.allIndefinites : List IndefiniteEntry

All Farsi indefinite entries

Equations

• Fragments.Farsi.Determiners.allIndefinites = [Fragments.Farsi.Determiners.yeki, Fragments.Farsi.Determiners.yek, Fragments.Farsi.Determiners.indef_i]

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

def Fragments.Farsi.Determiners.uniquenessSemantics : String

The uniqueness component of yek-i.

In root contexts, yek-i conveys: ∃!x. P(x) = "exactly one x satisfies P"

This comes from partial exhaustification of pre-exhaustified domain alternatives.

Equations

• Fragments.Farsi.Determiners.uniquenessSemantics = "∃x. P(x) ∧ ∀y. y ≠ x → ¬P(y)"

def Fragments.Farsi.Determiners.freeChoiceSemantics : String

The free choice component under deontic modals.

Under ◇_deo, yek-i conveys: ∀x. ◇_deo[P(x) ∧ ∀y≠x. ¬P(y)] "For each x, you may uniquely satisfy P with x"

Equations

• Fragments.Farsi.Determiners.freeChoiceSemantics = "∀x ∈ D. ◇_deo[P(x) ∧ ∀y ∈ D. y ≠ x → ¬P(y)]"

def Fragments.Farsi.Determiners.modalVariationSemantics : String

The modal variation component under epistemic modals.

Under ◇_epi, yek-i conveys: |{x : ◇_epi[P(x) ∧ ∀y≠x. ¬P(y)]}| ≥ 2 "At least two individuals are epistemic possibilities for uniquely satisfying P"

Equations

• Fragments.Farsi.Determiners.modalVariationSemantics = "|{x ∈ D : ◇_epi[P(x) ∧ ∀y ∈ D. y ≠ x → ¬P(y)]}| ≥ 2"