Lahiri (1998): Focus and Negative Polarity in Hindi

@cite{lahiri-1998} @cite{kadmon-landman-1993} @cite{lee-horn-1994}

Hindi NPIs (koii bhii 'anyone', ek bhii 'even one', kuch bhii 'anything', zaraa bhii 'even a little') are morphologically composed of a weak indefinite plus the focus particle bhii ('even'). @cite{lahiri-1998} shows that their distribution — both as NPIs and as free-choice items — follows from the compositional semantics of these parts.

The implicature clash mechanism

1. bhii in focused contexts contributes a conventional implicature (@cite{karttunen-peters-1979}), reanalyzed by Lahiri as scalar, that the assertion is the LEAST LIKELY among focus-induced alternatives
2. Weak indefinites as bottom of scale: ek ('one') denotes the weakest cardinality predicate — true of everything that exists
3. In UE contexts: every alternative entails the assertion (because 'one' is weakest), so the assertion is the MOST likely. The scalar implicature requires the opposite. Contradiction → unacceptable.
4. In DE contexts: entailment reverses, so the assertion is genuinely the LEAST likely. The scalar implicature is satisfiable → acceptable.

The ek bhii / koii bhii distinction (§8)

ek bhii introduces cardinality alternatives {one, two, three, ...}. koii bhii introduces contextually salient property alternatives. This explains why koii bhii has free-choice readings in generic contexts (the alternatives are contextual, not entailment-ordered) while ek bhii does not.

structure Lahiri1998.HindiNPIDatum : Type

A judged Hindi NPI sentence, paired with the licensing context (if any).

• sentence : String

  The sentence

• npiItem : String

  The NPI item

• grammatical : Bool

  Grammaticality judgment (true = OK, false = bad)

• context : Option Features.LicensingContext

  Type of licensing context (if grammatical)

• notes : String

  Notes

def Lahiri1998.instReprHindiNPIDatum.repr : HindiNPIDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Lahiri1998.instReprHindiNPIDatum : Repr HindiNPIDatum

Equations

• Lahiri1998.instReprHindiNPIDatum = { reprPrec := Lahiri1998.instReprHindiNPIDatum.repr }

inductive Lahiri1998.BhiiReading : Type

The two readings of the Hindi particle bhii, disambiguated by focus. In non-focused contexts bhii means 'also'; in focus-affected contexts (including all NPI uses) it means 'even'.

• even : BhiiReading
• also : BhiiReading

@[implicit_reducible]

instance Lahiri1998.instDecidableEqBhiiReading : DecidableEq BhiiReading

Equations

• Lahiri1998.instDecidableEqBhiiReading x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Lahiri1998.instReprBhiiReading.repr : BhiiReading → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Lahiri1998.instReprBhiiReading : Repr BhiiReading

Equations

• Lahiri1998.instReprBhiiReading = { reprPrec := Lahiri1998.instReprBhiiReading.repr }

structure Lahiri1998.NPIDecomposition : Type

Morphological decomposition of a Hindi NPI. All items in the paradigm share the structure: base indefinite + bhii.

• base : String
• baseGloss : String
• npiForm : String
• npiGloss : String

@[implicit_reducible]

instance Lahiri1998.instReprNPIDecomposition : Repr NPIDecomposition

Equations

• Lahiri1998.instReprNPIDecomposition = { reprPrec := Lahiri1998.instReprNPIDecomposition.repr }

def Lahiri1998.instReprNPIDecomposition.repr : NPIDecomposition → ℕ → Std.Format

Equations

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

def Lahiri1998.ekBhii : NPIDecomposition

Equations

• Lahiri1998.ekBhii = { base := "ek", baseGloss := "one", npiForm := "ek bhii", npiGloss := "any, even one" }

def Lahiri1998.koiiBhiiD : NPIDecomposition

Equations

• Lahiri1998.koiiBhiiD = { base := "koii", baseGloss := "someone", npiForm := "koii bhii", npiGloss := "anyone" }

def Lahiri1998.kuchBhii : NPIDecomposition

Equations

• Lahiri1998.kuchBhii = { base := "kuch", baseGloss := "something (mass)", npiForm := "kuch bhii", npiGloss := "anything" }

def Lahiri1998.zaraaBhii : NPIDecomposition

Equations

• Lahiri1998.zaraaBhii = { base := "zaraa", baseGloss := "a little", npiForm := "zaraa bhii", npiGloss := "even a little" }

def Lahiri1998.kabhiiBhii : NPIDecomposition

Equations

• Lahiri1998.kabhiiBhii = { base := "kabhii", baseGloss := "sometime", npiForm := "kabhii bhii", npiGloss := "ever, anytime" }

def Lahiri1998.kahiiNBhii : NPIDecomposition

Equations

• Lahiri1998.kahiiNBhii = { base := "kahiiN", baseGloss := "somewhere", npiForm := "kahiiN bhii", npiGloss := "anywhere" }

def Lahiri1998.hindiNPIs : List NPIDecomposition

All Hindi NPIs share the particle bhii — the morphological uniformity that motivates the compositional analysis. Visible by inspection of the npiForm field of every entry below.

Equations

• Lahiri1998.hindiNPIs = [Lahiri1998.ekBhii, Lahiri1998.koiiBhiiD, Lahiri1998.kuchBhii, Lahiri1998.zaraaBhii, Lahiri1998.kabhiiBhii, Lahiri1998.kahiiNBhii]

def Lahiri1998.alternativeTypeOf (d : NPIDecomposition) : Typology.PolarityItem.AlternativeType

ek and zaraa introduce cardinality/measure alternatives; koii and kuch introduce contextual property alternatives.

This distinction is stored in the lexicon (§8): the kind of alternatives a lexical item allows is part of its lexical entry.

Equations

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

We model the cardinality scale using the existing 4-world semantics from Semantics.Entailment.Basic.

World assignment:
- w0: ≥3 entities satisfy the VP
- w1: exactly 2 satisfy the VP
- w2: exactly 1 satisfies the VP
- w3: 0 satisfy the VP

The propositions `∃x[n(x) ∧ VP(x)]` then have clear truth values,
and their entailment relations model the cardinality scale. 

def Lahiri1998.atLeastOneB : Semantics.Entailment.World → Bool

At least one entity satisfies the VP (Bool form for likelihood/EVEN API).

Equations

• Lahiri1998.atLeastOneB w = (w != Semantics.Entailment.World.w3)

def Lahiri1998.atLeastTwoB : Semantics.Entailment.World → Bool

At least two entities satisfy the VP (Bool form).

Equations

• Lahiri1998.atLeastTwoB w = (w == Semantics.Entailment.World.w0 || w == Semantics.Entailment.World.w1)

def Lahiri1998.atLeastThreeB : Semantics.Entailment.World → Bool

At least three entities satisfy the VP (Bool form).

Equations

• Lahiri1998.atLeastThreeB w = (w == Semantics.Entailment.World.w0)

def Lahiri1998.atLeastOne : Set Semantics.Entailment.World

At least one entity satisfies the VP (Set form for entails). True at w0, w1, w2.

Equations

• Lahiri1998.atLeastOne = {w : Semantics.Entailment.World | Lahiri1998.atLeastOneB w = true}

def Lahiri1998.atLeastTwo : Set Semantics.Entailment.World

At least two entities satisfy the VP (Set form). True at w0, w1.

Equations

• Lahiri1998.atLeastTwo = {w : Semantics.Entailment.World | Lahiri1998.atLeastTwoB w = true}

def Lahiri1998.atLeastThree : Set Semantics.Entailment.World

At least three entities satisfy the VP (Set form). True at w0 only.

Equations

• Lahiri1998.atLeastThree = {w : Semantics.Entailment.World | Lahiri1998.atLeastThreeB w = true}

The central semantic property: one is the weakest cardinality predicate. For any cardinality predicate P: ∃x[P(x) ∧ VP(x)] → ∃x[one(x) ∧ VP(x)].

In the 4-world model, this means every `atLeastN` proposition entails
`atLeastOne`, but not vice versa. This is eq. (70) in the paper:
∀x(P(x) → one(x)). 

theorem Lahiri1998.two_entails_one : Semantics.Entailment.entails atLeastTwo atLeastOne

theorem Lahiri1998.three_entails_one : Semantics.Entailment.entails atLeastThree atLeastOne

theorem Lahiri1998.three_entails_two : Semantics.Entailment.entails atLeastThree atLeastTwo

theorem Lahiri1998.one_not_entails_two : ¬Semantics.Entailment.entails atLeastOne atLeastTwo

The entailment is strict: atLeastOne does not entail stronger predicates.

theorem Lahiri1998.one_not_entails_three : ¬Semantics.Entailment.entails atLeastOne atLeastThree

The paper's core result (§7.4, eqs. 66–79).

**UE (positive context)**: "*koii bhii aayaa" ('*Anyone came')
- Assertion: `atLeastOne` (= ∃x[one(x) ∧ came(x)])
- Alternatives: `atLeastTwo`, `atLeastThree`
- Each alternative entails the assertion (`two_entails_one`, `three_entails_one`)
- By likelihood monotonicity (eq. 71): likelihood(alt) ≤ likelihood(assertion)
- EVEN requires (eq. 69): likelihood(assertion) < likelihood(alt)
- Contradiction: can't have both

**DE (under negation)**: "koii bhii nahiiN aayaa" ('No one came')
- Assertion: `pnot atLeastOne` (= ¬∃x[one(x) ∧ came(x)])
- Alternatives: `pnot atLeastTwo`, `pnot atLeastThree`
- The assertion entails each alternative (negation reverses, eq. 78)
- By likelihood monotonicity (eq. 79): likelihood(assertion) ≤ likelihood(alt)
- EVEN requires (eq. 77): likelihood(assertion) < likelihood(alt)
- Compatible: `assertion ≤ alt` is consistent with `assertion < alt` 

theorem Lahiri1998.ue_alt_entails_assertion : Semantics.Entailment.entails atLeastTwo atLeastOne ∧ Semantics.Entailment.entails atLeastThree atLeastOne

UE pattern: all alternatives entail the assertion. This makes the assertion the MOST likely — fatal for EVEN.

theorem Lahiri1998.de_assertion_entails_alt : Semantics.Entailment.entails (Semantics.Entailment.pnot atLeastOne) (Semantics.Entailment.pnot atLeastTwo) ∧ Semantics.Entailment.entails (Semantics.Entailment.pnot atLeastOne) (Semantics.Entailment.pnot atLeastThree)

DE pattern: the assertion entails all alternatives. Negation reverses the entailment direction. This makes the assertion the LEAST likely — satisfying EVEN.

theorem Lahiri1998.ue_not_reverse : ¬Semantics.Entailment.entails atLeastOne atLeastTwo ∧ ¬Semantics.Entailment.entails atLeastOne atLeastThree

The asymmetry: in UE the assertion does NOT entail alternatives.

theorem Lahiri1998.de_not_reverse : ¬Semantics.Entailment.entails (Semantics.Entailment.pnot atLeastTwo) (Semantics.Entailment.pnot atLeastOne) ∧ ¬Semantics.Entailment.entails (Semantics.Entailment.pnot atLeastThree) (Semantics.Entailment.pnot atLeastOne)

The asymmetry: in DE the alternatives do NOT entail the assertion.

We build TraditionalEven instances for ek bhii in UE and DE contexts, connecting the cardinality model to the Particles.lean API.

In UE: `atLeastOne` is the prejacent, `[atLeastTwo, atLeastThree]` are
alternatives. The presupposition requires `atLeastOne` to be less likely
than each alternative — but since each alternative entails `atLeastOne`,
the opposite holds under any monotone likelihood ordering.

In DE: `pnot atLeastOne` is the prejacent. The assertion entails each
negated alternative, so the prejacent IS the least likely. 

def Lahiri1998.ekBhiiEvenUE : Semantics.FocusParticles.TraditionalEven

EVEN instance for *ek bhii aayaa ('*Even one came') in UE context.

Equations

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

def Lahiri1998.ekBhiiEvenDE : Semantics.FocusParticles.TraditionalEven

EVEN instance for ek bhii nahiiN aayaa ('Not even one came') in DE.

Equations

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

theorem Lahiri1998.ekBhii_even_clash_UE (lt le : (Semantics.Entailment.World → Bool) → (Semantics.Entailment.World → Bool) → Prop) (hMono : Semantics.FocusParticles.LikelihoodMonotone le) (hCompat : ∀ (a b : Semantics.Entailment.World → Bool), lt a b → le b a → False) (alt : Semantics.Entailment.World → Bool) (hAlt : alt = atLeastTwoB ∨ alt = atLeastThreeB) (hEven : lt atLeastOneB alt) : False

In UE, the EVEN presupposition for ek bhii is contradicted: every alternative entails the assertion, so under any monotone likelihood ordering the assertion cannot be strictly less likely than its alternatives.

This is the abstract version of the paper's argument (§7.4, eqs. 68–71).

theorem Lahiri1998.ekBhii_even_ok_DE : Semantics.Entailment.entails (Semantics.Entailment.pnot atLeastOne) (Semantics.Entailment.pnot atLeastTwo) ∧ Semantics.Entailment.entails (Semantics.Entailment.pnot atLeastOne) (Semantics.Entailment.pnot atLeastThree)

In DE, the EVEN presupposition for ek bhii nahiiN is satisfiable: the negated assertion entails each negated alternative, so the assertion IS the least likely under a monotone ordering.

This is the paper's argument (§7.4, eqs. 76–79).

theorem Lahiri1998.even_clash_abstract {W : Type} (lt le : (W → Bool) → (W → Bool) → Prop) (hMono : ∀ (p q : W → Bool), (∀ (w : W), p w = true → q w = true) → le p q) (hCompat : ∀ (a b : W → Bool), lt a b → le b a → False) (assertion alt : W → Bool) (hEntails : ∀ (w : W), alt w = true → assertion w = true) (hEven : lt assertion alt) : False

An EVEN scalar implicature is CONTRADICTED when the assertion is entailed by all alternatives. Under LikelihoodMonotone, each alternative is then at most as likely as the assertion, but EVEN requires the assertion to be strictly less likely than each alternative.

Licensing judgments from @cite{lahiri-1998} §4. Each datum demonstrates the compositional prediction: bhii + indefinite is licensed in DE contexts and blocked in UE contexts.

Uses the local `HindiNPIDatum` defined above. 

def Lahiri1998.koiiBhii_neg : HindiNPIDatum

Equations

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

def Lahiri1998.koiiBhii_pos : HindiNPIDatum

Equations

• Lahiri1998.koiiBhii_pos = { sentence := "*koii bhii aayaa", npiItem := "koii bhii", grammatical := false, context := none, notes := "(6a) '*Anyone came.' Positive is UE → clash" }

def Lahiri1998.ekBhii_neg : HindiNPIDatum

Equations

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

def Lahiri1998.ekBhii_pos : HindiNPIDatum

Equations

• Lahiri1998.ekBhii_pos = { sentence := "*ek bhii aadmii aayaa", npiItem := "ek bhii", grammatical := false, context := none, notes := "(7a) '*Any man came.' UE → clash" }

def Lahiri1998.kuchBhii_neg : HindiNPIDatum

Equations

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

def Lahiri1998.kuchBhii_pos : HindiNPIDatum

Equations

• Lahiri1998.kuchBhii_pos = { sentence := "*maiN-ne kuch bhii khaayaa", npiItem := "kuch bhii", grammatical := false, context := none, notes := "(8a) '*I ate anything.' UE → clash" }

def Lahiri1998.zaraaBhii_neg : HindiNPIDatum

Equations

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

def Lahiri1998.zaraaBhii_pos : HindiNPIDatum

Equations

• Lahiri1998.zaraaBhii_pos = { sentence := "*maiN-ne zaraa bhii khaanaa khaayaa", npiItem := "zaraa bhii", grammatical := false, context := none, notes := "(9a) '*I ate any food.' UE → clash" }

def Lahiri1998.koiiBhii_obj_neg : HindiNPIDatum

Equations

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

def Lahiri1998.koiiBhii_obj_pos : HindiNPIDatum

Equations

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

def Lahiri1998.npi_cond_protasis : HindiNPIDatum

Equations

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

def Lahiri1998.npi_cond_apodosis : HindiNPIDatum

Equations

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

def Lahiri1998.npi_univ_restrictor : HindiNPIDatum

Equations

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

def Lahiri1998.npi_exist_restrictor : HindiNPIDatum

Equations

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

def Lahiri1998.npi_adversative_surprise_ek : HindiNPIDatum

Equations

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

def Lahiri1998.npi_adversative_surprise_koii : HindiNPIDatum

Equations

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

def Lahiri1998.npi_prohibition_obj : HindiNPIDatum

Equations

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

def Lahiri1998.npi_prohibition_subj : HindiNPIDatum

Equations

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

def Lahiri1998.npi_glad_bad : HindiNPIDatum

Equations

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

def Lahiri1998.npi_glad_settle : HindiNPIDatum

Equations

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

def Lahiri1998.npi_before : HindiNPIDatum

Equations

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

def Lahiri1998.npi_question : HindiNPIDatum

Equations

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

def Lahiri1998.npi_subject_hindi : HindiNPIDatum

Equations

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

@cite{lahiri-1998} §5: Hindi NPIs also behave as free-choice items in generic and modal contexts. The environments are:

1. Generic sentences (§5.1): *koii bhii aadmii is mez-ko uThaa letaa hai*
   'Any man lifts this table'
2. Modals of possibility (§5.2): *ek bhii aadmii is mez-ko uThaa saktaa hai*
   'Even one person can lift this table'
3. **NOT** modals of necessity (§5.2): **kisii-ko bhii ghar jaanaa caahiye*
   '*Anyone must go home'

The unified account: in generic contexts, indefinites are bound by
the GEN operator. The restriction of GEN is a strengthening environment
(§7.6, eqs. 95–98), so the EVEN implicature is satisfiable. Modals
of possibility pattern with generics; necessity modals do not. 

structure Lahiri1998.FCDatum : Type

• sentence : String
• npiItem : String
• contextType : String
• grammatical : Bool
• notes : String

@[implicit_reducible]

instance Lahiri1998.instReprFCDatum : Repr FCDatum

Equations

• Lahiri1998.instReprFCDatum = { reprPrec := Lahiri1998.instReprFCDatum.repr }

def Lahiri1998.instReprFCDatum.repr : FCDatum → ℕ → Std.Format

Equations

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

def Lahiri1998.fc_generic_koii : FCDatum

Equations

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

def Lahiri1998.fc_generic_owl : FCDatum

Equations

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

def Lahiri1998.fc_generic_ek : FCDatum

Equations

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

def Lahiri1998.fc_generic_zaraa : FCDatum

Equations

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

def Lahiri1998.fc_possibility_ek : FCDatum

Equations

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

def Lahiri1998.fc_possibility_koii : FCDatum

Equations

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

def Lahiri1998.fc_possibility_kabhii : FCDatum

Equations

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

def Lahiri1998.fc_necessity_kisii : FCDatum

Equations

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

def Lahiri1998.fc_necessity_ek : FCDatum

Equations

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

def Lahiri1998.fc_imperative_kuch : FCDatum

Equations

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

def Lahiri1998.fc_imperative_koii : FCDatum

Equations

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

def Lahiri1998.fc_imperative_zaraa_odd : FCDatum

Equations

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

def Lahiri1998.fc_imperative_ek_odd : FCDatum

Equations

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

def Lahiri1998.allFCData : List FCDatum

Equations

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

theorem Lahiri1998.generic_and_possibility_license : ((List.filter (fun (d : FCDatum) => d.contextType == "generic" || d.contextType == "modalPossibility") allFCData).all fun (x : FCDatum) => x.grammatical) = true

Generics and possibility modals license FC readings.

theorem Lahiri1998.necessity_blocks : ((List.filter (fun (d : FCDatum) => d.contextType == "modalNecessity") allFCData).all fun (x : FCDatum) => !x.grammatical) = true

Necessity modals block FC readings.

@cite{lahiri-1998} §8: The first approximation (§7) treats koii bhii and ek bhii as semantically equivalent, but they differ:

(99a) *ek bhii aadmii is mez-ko uThaa saktaa hai*
      'Even one person can lift this table.'
      Implicature: more people lifting is MORE likely.
(99b) *koii bhii aadmii is mez-ko uThaa saktaa hai*
      'Anyone can lift this table.'
      No cardinality implicature; FC reading.

(100a) *koii bhii tiin log is mez-ko uThaa sakte haiN*
       'Any three people can lift this table.' ✓
(100b) **ek bhii tiin log is mez-ko uThaa sakte haiN*
       '*Even one three people can lift this table.' ✗

The explanation: *ek* introduces CARDINALITY alternatives (other
numerals), while *koii* introduces CONTEXTUAL PROPERTY alternatives
(pragmatically salient properties like 'not sick', 'strong', etc.).
Only contextual alternatives give rise to FC readings. 

structure Lahiri1998.EkKoiiContrastDatum : Type

• ekSentence : String
• koiiSentence : String
• contextType : String
• ekGrammatical : Bool
• koiiGrammatical : Bool
• notes : String

def Lahiri1998.instReprEkKoiiContrastDatum.repr : EkKoiiContrastDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Lahiri1998.instReprEkKoiiContrastDatum : Repr EkKoiiContrastDatum

Equations

• Lahiri1998.instReprEkKoiiContrastDatum = { reprPrec := Lahiri1998.instReprEkKoiiContrastDatum.repr }

def Lahiri1998.numeral_contrast : EkKoiiContrastDatum

In generic contexts with numerals, koii bhii is fine but ek bhii is blocked (100a vs 100b).

Equations

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

def Lahiri1998.generic_contrast : EkKoiiContrastDatum

In generic contexts, both are fine but carry different implicatures (99).

Equations

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

theorem Lahiri1998.numeral_contrast_asymmetry : numeral_contrast.ekGrammatical = false ∧ numeral_contrast.koiiGrammatical = true

theorem Lahiri1998.alternative_type_predicts_contrast : alternativeTypeOf ekBhii = Typology.PolarityItem.AlternativeType.cardinality ∧ alternativeTypeOf koiiBhiiD = Typology.PolarityItem.AlternativeType.contextualProperty

The alternative type distinction predicts the contrast: cardinality alternatives clash with explicit numerals (one ≠ three), while contextual property alternatives are compatible.

def Lahiri1998.allHindiNPIData : List HindiNPIDatum

Equations

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

theorem Lahiri1998.licensing_context_iff_grammatical : List.Forall (fun (d : HindiNPIDatum) => (d.grammatical = true → d.context.isSome = true) ∧ (¬d.grammatical = true → d.context.isNone = true)) allHindiNPIData

Every grammatical datum has a licensing context; every ungrammatical one does not.

def Lahiri1998.isDEOrQuestion : Features.LicensingContext → Prop

All licensing contexts in the grammatical data are DE environments (or questions, which license via negative bias rather than pure DE).

Equations

• Lahiri1998.isDEOrQuestion Features.LicensingContext.negation = True
• Lahiri1998.isDEOrQuestion Features.LicensingContext.conditionalAntecedent = True
• Lahiri1998.isDEOrQuestion Features.LicensingContext.universalRestrictor = True
• Lahiri1998.isDEOrQuestion Features.LicensingContext.beforeClause = True
• Lahiri1998.isDEOrQuestion Features.LicensingContext.question = True
• Lahiri1998.isDEOrQuestion Features.LicensingContext.adversative = True
• Lahiri1998.isDEOrQuestion Features.LicensingContext.denyVerb = True
• Lahiri1998.isDEOrQuestion x✝ = False

@[implicit_reducible]

instance Lahiri1998.instDecidablePredLicensingContextIsDEOrQuestion : DecidablePred isDEOrQuestion

Equations

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

def Lahiri1998.hasDELicenser (d : HindiNPIDatum) : Prop

Predicate: a datum's context is some DE-or-question licenser.

Equations

• Lahiri1998.hasDELicenser d = match d.context with | none => False | some c => Lahiri1998.isDEOrQuestion c

@[implicit_reducible]

instance Lahiri1998.instDecidablePredHindiNPIDatumHasDELicenser : DecidablePred hasDELicenser

Equations

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

theorem Lahiri1998.grammatical_contexts_are_de : List.Forall hasDELicenser (List.filter (fun (x : HindiNPIDatum) => x.grammatical) allHindiNPIData)

@cite{lahiri-1998} §6: Hindi allows subject NPIs under clausemate negation, unlike English.

Hindi: "koi bhii aadmii nahiiN aayaa" ('No one came') ✓
English: "*Anyone didn't come" ✗

The paper's explanation: in Hindi, negation can take wide scope over
the subject indefinite (NegP > IP), placing the NPI in the semantic
scope of negation at LF. In English, the subject is outside NegP's
c-command domain at S-structure, and reconstruction is restricted.

This difference is *independent* of the implicature clash mechanism —
both languages have the same EVEN + weak predicate semantics, but
differ in whether the syntactic configuration allows the NPI to be
in the semantic scope of negation. 

structure Lahiri1998.SubjectNPIContrast : Type

• hindiSentence : String
• hindiGrammatical : Bool
• englishSentence : String
• englishGrammatical : Bool
• notes : String

def Lahiri1998.instReprSubjectNPIContrast.repr : SubjectNPIContrast → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Lahiri1998.instReprSubjectNPIContrast : Repr SubjectNPIContrast

Equations

• Lahiri1998.instReprSubjectNPIContrast = { reprPrec := Lahiri1998.instReprSubjectNPIContrast.repr }

def Lahiri1998.subjectNPI : SubjectNPIContrast

Equations

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

The fragment entry Fragments.Hindi.PolarityItems.koiiBhii stores licensing contexts as a list. @cite{lahiri-1998}'s contribution is showing that these contexts are not arbitrary — they are exactly the DE environments (for NPI readings) and generic/modal environments (for FC readings) where the EVEN implicature is satisfiable.

The study file derives this; the fragment file stores it.
A future refactoring should make the fragment derive from the theory. 

theorem Lahiri1998.koiiBhii_is_fci : Fragments.Hindi.PolarityItems.koiiBhii.polarityType = Typology.PolarityItem.PolarityType.fci

theorem Lahiri1998.koiiNahiin_is_npi : Fragments.Hindi.PolarityItems.koiiNahiin.polarityType = Typology.PolarityItem.PolarityType.npiWeak

theorem Lahiri1998.decomposition_matches_fragment : koiiBhiiD.npiForm = "koii bhii" ∧ Fragments.Hindi.PolarityItems.koiiBhii.form = "koii bhii"

The decomposition in this study matches the fragment entry.

theorem Lahiri1998.fragment_morphology_matches : Fragments.Hindi.PolarityItems.koiiBhii.morphology = Typology.PolarityItem.NPIMorphology.indefPlusEven ∧ Fragments.Hindi.PolarityItems.koiiNahiin.morphology = Typology.PolarityItem.NPIMorphology.indefPlusNeg

The morphology classification in the fragment entry matches the decomposition analysis: koii bhii is indefinite + even.

theorem Lahiri1998.fragment_alternativeType_matches : Fragments.Hindi.PolarityItems.koiiBhii.alternativeType = Typology.PolarityItem.AlternativeType.contextualProperty ∧ alternativeTypeOf koiiBhiiD = Typology.PolarityItem.AlternativeType.contextualProperty

The alternative type in the fragment matches the study's prediction: koii bhii introduces contextual property alternatives.