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.

inductive Phenomena.Polarity.Studies.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

instance Phenomena.Polarity.Studies.Lahiri1998.instDecidableEqBhiiReading : DecidableEq BhiiReading

Equations

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

def Phenomena.Polarity.Studies.Lahiri1998.instReprBhiiReading.repr : BhiiReading → ℕ → Std.Format

Equations

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

instance Phenomena.Polarity.Studies.Lahiri1998.instReprBhiiReading : Repr BhiiReading

Equations

• Phenomena.Polarity.Studies.Lahiri1998.instReprBhiiReading = { reprPrec := Phenomena.Polarity.Studies.Lahiri1998.instReprBhiiReading.repr }

structure Phenomena.Polarity.Studies.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

def Phenomena.Polarity.Studies.Lahiri1998.instReprNPIDecomposition.repr : NPIDecomposition → ℕ → Std.Format

Equations

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

instance Phenomena.Polarity.Studies.Lahiri1998.instReprNPIDecomposition : Repr NPIDecomposition

Equations

• Phenomena.Polarity.Studies.Lahiri1998.instReprNPIDecomposition = { reprPrec := Phenomena.Polarity.Studies.Lahiri1998.instReprNPIDecomposition.repr }

def Phenomena.Polarity.Studies.Lahiri1998.ekBhii : NPIDecomposition

Equations

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

def Phenomena.Polarity.Studies.Lahiri1998.koiiBhiiD : NPIDecomposition

Equations

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

def Phenomena.Polarity.Studies.Lahiri1998.kuchBhii : NPIDecomposition

Equations

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

def Phenomena.Polarity.Studies.Lahiri1998.zaraaBhii : NPIDecomposition

Equations

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

def Phenomena.Polarity.Studies.Lahiri1998.kabhiiBhii : NPIDecomposition

Equations

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

def Phenomena.Polarity.Studies.Lahiri1998.kahiiNBhii : NPIDecomposition

Equations

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

def Phenomena.Polarity.Studies.Lahiri1998.hindiNPIs : List NPIDecomposition

Equations

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

theorem Phenomena.Polarity.Studies.Lahiri1998.all_share_bhii : (hindiNPIs.all fun (d : NPIDecomposition) => d.npiForm.endsWith "bhii") = true

All Hindi NPIs share the particle bhii — the morphological uniformity that motivates the compositional analysis.

def Phenomena.Polarity.Studies.Lahiri1998.alternativeTypeOf (d : NPIDecomposition) : Core.Lexical.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 Phenomena.Polarity.Studies.Lahiri1998.atLeastOne : BProp Semantics.Entailment.World

At least one entity satisfies the VP. True at w0, w1, w2.

Equations

• Phenomena.Polarity.Studies.Lahiri1998.atLeastOne w = (w != Semantics.Entailment.World.w3)

def Phenomena.Polarity.Studies.Lahiri1998.atLeastTwo : BProp Semantics.Entailment.World

At least two entities satisfy the VP. True at w0, w1.

Equations

• Phenomena.Polarity.Studies.Lahiri1998.atLeastTwo w = (w == Semantics.Entailment.World.w0 || w == Semantics.Entailment.World.w1)

def Phenomena.Polarity.Studies.Lahiri1998.atLeastThree : BProp Semantics.Entailment.World

At least three entities satisfy the VP. True at w0 only.

Equations

• Phenomena.Polarity.Studies.Lahiri1998.atLeastThree w = (w == Semantics.Entailment.World.w0)

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 Phenomena.Polarity.Studies.Lahiri1998.two_entails_one : Semantics.Entailment.entails atLeastTwo atLeastOne = true

theorem Phenomena.Polarity.Studies.Lahiri1998.three_entails_one : Semantics.Entailment.entails atLeastThree atLeastOne = true

theorem Phenomena.Polarity.Studies.Lahiri1998.three_entails_two : Semantics.Entailment.entails atLeastThree atLeastTwo = true

theorem Phenomena.Polarity.Studies.Lahiri1998.one_not_entails_two : Semantics.Entailment.entails atLeastOne atLeastTwo = false

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

theorem Phenomena.Polarity.Studies.Lahiri1998.one_not_entails_three : Semantics.Entailment.entails atLeastOne atLeastThree = false

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 Phenomena.Polarity.Studies.Lahiri1998.ue_alt_entails_assertion : Semantics.Entailment.entails atLeastTwo atLeastOne = true ∧ Semantics.Entailment.entails atLeastThree atLeastOne = true

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

theorem Phenomena.Polarity.Studies.Lahiri1998.de_assertion_entails_alt : Semantics.Entailment.entails (Semantics.Entailment.pnot atLeastOne) (Semantics.Entailment.pnot atLeastTwo) = true ∧ Semantics.Entailment.entails (Semantics.Entailment.pnot atLeastOne) (Semantics.Entailment.pnot atLeastThree) = true

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

theorem Phenomena.Polarity.Studies.Lahiri1998.ue_not_reverse : Semantics.Entailment.entails atLeastOne atLeastTwo = false ∧ Semantics.Entailment.entails atLeastOne atLeastThree = false

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

theorem Phenomena.Polarity.Studies.Lahiri1998.de_not_reverse : Semantics.Entailment.entails (Semantics.Entailment.pnot atLeastTwo) (Semantics.Entailment.pnot atLeastOne) = false ∧ Semantics.Entailment.entails (Semantics.Entailment.pnot atLeastThree) (Semantics.Entailment.pnot atLeastOne) = false

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 Phenomena.Polarity.Studies.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 Phenomena.Polarity.Studies.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 Phenomena.Polarity.Studies.Lahiri1998.ekBhii_even_clash_UE (lt le : BProp Semantics.Entailment.World → BProp Semantics.Entailment.World → Prop) (hMono : Semantics.FocusParticles.LikelihoodMonotone le) (hCompat : ∀ (a b : BProp Semantics.Entailment.World), lt a b → le b a → False) (alt : BProp Semantics.Entailment.World) (hAlt : alt = atLeastTwo ∨ alt = atLeastThree) (hEven : lt atLeastOne 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 Phenomena.Polarity.Studies.Lahiri1998.ekBhii_even_ok_DE : Semantics.Entailment.entails (Semantics.Entailment.pnot atLeastOne) (Semantics.Entailment.pnot atLeastTwo) = true ∧ Semantics.Entailment.entails (Semantics.Entailment.pnot atLeastOne) (Semantics.Entailment.pnot atLeastThree) = true

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 Phenomena.Polarity.Studies.Lahiri1998.even_clash_abstract {W : Type} (lt le : BProp W → BProp W → Prop) (hMono : ∀ (p q : BProp W), (∀ (w : W), p w = true → q w = true) → le p q) (hCompat : ∀ (a b : BProp W), lt a b → le b a → False) (assertion alt : BProp W) (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 `NPIDatum` from `Phenomena.Polarity.NPIs`. 

def Phenomena.Polarity.Studies.Lahiri1998.koiiBhii_neg : NPIs.NPIDatum

Equations

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

def Phenomena.Polarity.Studies.Lahiri1998.koiiBhii_pos : NPIs.NPIDatum

Equations

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

def Phenomena.Polarity.Studies.Lahiri1998.ekBhii_neg : NPIs.NPIDatum

Equations

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

def Phenomena.Polarity.Studies.Lahiri1998.ekBhii_pos : NPIs.NPIDatum

Equations

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

def Phenomena.Polarity.Studies.Lahiri1998.kuchBhii_neg : NPIs.NPIDatum

Equations

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

def Phenomena.Polarity.Studies.Lahiri1998.kuchBhii_pos : NPIs.NPIDatum

Equations

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

def Phenomena.Polarity.Studies.Lahiri1998.zaraaBhii_neg : NPIs.NPIDatum

Equations

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

def Phenomena.Polarity.Studies.Lahiri1998.zaraaBhii_pos : NPIs.NPIDatum

Equations

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

def Phenomena.Polarity.Studies.Lahiri1998.koiiBhii_obj_neg : NPIs.NPIDatum

Equations

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

def Phenomena.Polarity.Studies.Lahiri1998.koiiBhii_obj_pos : NPIs.NPIDatum

Equations

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

def Phenomena.Polarity.Studies.Lahiri1998.npi_cond_protasis : NPIs.NPIDatum

Equations

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

def Phenomena.Polarity.Studies.Lahiri1998.npi_cond_apodosis : NPIs.NPIDatum

Equations

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

def Phenomena.Polarity.Studies.Lahiri1998.npi_univ_restrictor : NPIs.NPIDatum

Equations

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

def Phenomena.Polarity.Studies.Lahiri1998.npi_exist_restrictor : NPIs.NPIDatum

Equations

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

def Phenomena.Polarity.Studies.Lahiri1998.npi_adversative_surprise_ek : NPIs.NPIDatum

Equations

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

def Phenomena.Polarity.Studies.Lahiri1998.npi_adversative_surprise_koii : NPIs.NPIDatum

Equations

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

def Phenomena.Polarity.Studies.Lahiri1998.npi_prohibition_obj : NPIs.NPIDatum

Equations

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

def Phenomena.Polarity.Studies.Lahiri1998.npi_prohibition_subj : NPIs.NPIDatum

Equations

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

def Phenomena.Polarity.Studies.Lahiri1998.npi_glad_bad : NPIs.NPIDatum

Equations

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

def Phenomena.Polarity.Studies.Lahiri1998.npi_glad_settle : NPIs.NPIDatum

Equations

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

def Phenomena.Polarity.Studies.Lahiri1998.npi_before : NPIs.NPIDatum

Equations

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

def Phenomena.Polarity.Studies.Lahiri1998.npi_question : NPIs.NPIDatum

Equations

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

def Phenomena.Polarity.Studies.Lahiri1998.npi_subject_hindi : NPIs.NPIDatum

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 Phenomena.Polarity.Studies.Lahiri1998.FCDatum : Type

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

def Phenomena.Polarity.Studies.Lahiri1998.instReprFCDatum.repr : FCDatum → ℕ → Std.Format

Equations

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

instance Phenomena.Polarity.Studies.Lahiri1998.instReprFCDatum : Repr FCDatum

Equations

• Phenomena.Polarity.Studies.Lahiri1998.instReprFCDatum = { reprPrec := Phenomena.Polarity.Studies.Lahiri1998.instReprFCDatum.repr }

def Phenomena.Polarity.Studies.Lahiri1998.fc_generic_koii : FCDatum

Equations

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

def Phenomena.Polarity.Studies.Lahiri1998.fc_generic_owl : FCDatum

Equations

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

def Phenomena.Polarity.Studies.Lahiri1998.fc_generic_ek : FCDatum

Equations

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

def Phenomena.Polarity.Studies.Lahiri1998.fc_generic_zaraa : FCDatum

Equations

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

def Phenomena.Polarity.Studies.Lahiri1998.fc_possibility_ek : FCDatum

Equations

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

def Phenomena.Polarity.Studies.Lahiri1998.fc_possibility_koii : FCDatum

Equations

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

def Phenomena.Polarity.Studies.Lahiri1998.fc_possibility_kabhii : FCDatum

Equations

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

def Phenomena.Polarity.Studies.Lahiri1998.fc_necessity_kisii : FCDatum

Equations

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

def Phenomena.Polarity.Studies.Lahiri1998.fc_necessity_ek : FCDatum

Equations

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

def Phenomena.Polarity.Studies.Lahiri1998.fc_imperative_kuch : FCDatum

Equations

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

def Phenomena.Polarity.Studies.Lahiri1998.fc_imperative_koii : FCDatum

Equations

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

def Phenomena.Polarity.Studies.Lahiri1998.fc_imperative_zaraa_odd : FCDatum

Equations

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

def Phenomena.Polarity.Studies.Lahiri1998.fc_imperative_ek_odd : FCDatum

Equations

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

def Phenomena.Polarity.Studies.Lahiri1998.allFCData : List FCDatum

Equations

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

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

Generics and possibility modals license FC readings.

theorem Phenomena.Polarity.Studies.Lahiri1998.necessity_blocks : ((List.filter (fun (d : FCDatum) => d.contextType == "modal_necessity") 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 Phenomena.Polarity.Studies.Lahiri1998.EkKoiiContrastDatum : Type

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

def Phenomena.Polarity.Studies.Lahiri1998.instReprEkKoiiContrastDatum.repr : EkKoiiContrastDatum → ℕ → Std.Format

Equations

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

instance Phenomena.Polarity.Studies.Lahiri1998.instReprEkKoiiContrastDatum : Repr EkKoiiContrastDatum

Equations

• Phenomena.Polarity.Studies.Lahiri1998.instReprEkKoiiContrastDatum = { reprPrec := Phenomena.Polarity.Studies.Lahiri1998.instReprEkKoiiContrastDatum.repr }

def Phenomena.Polarity.Studies.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 Phenomena.Polarity.Studies.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 Phenomena.Polarity.Studies.Lahiri1998.numeral_contrast_asymmetry : numeral_contrast.ekGrammatical = false ∧ numeral_contrast.koiiGrammatical = true

theorem Phenomena.Polarity.Studies.Lahiri1998.alternative_type_predicts_contrast : alternativeTypeOf ekBhii = Core.Lexical.PolarityItem.AlternativeType.cardinality ∧ alternativeTypeOf koiiBhiiD = Core.Lexical.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 Phenomena.Polarity.Studies.Lahiri1998.allHindiNPIData : List NPIs.NPIDatum

Equations

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

theorem Phenomena.Polarity.Studies.Lahiri1998.licensing_context_iff_grammatical : List.Forall (fun (d : NPIs.NPIDatum) => (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 Phenomena.Polarity.Studies.Lahiri1998.isDEOrQuestion : NPIs.LicensingContext → Bool

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

Equations

• Phenomena.Polarity.Studies.Lahiri1998.isDEOrQuestion Phenomena.Polarity.NPIs.LicensingContext.sententialNegation = true
• Phenomena.Polarity.Studies.Lahiri1998.isDEOrQuestion Phenomena.Polarity.NPIs.LicensingContext.conditional = true
• Phenomena.Polarity.Studies.Lahiri1998.isDEOrQuestion Phenomena.Polarity.NPIs.LicensingContext.universalRestrictor = true
• Phenomena.Polarity.Studies.Lahiri1998.isDEOrQuestion Phenomena.Polarity.NPIs.LicensingContext.beforeClause = true
• Phenomena.Polarity.Studies.Lahiri1998.isDEOrQuestion Phenomena.Polarity.NPIs.LicensingContext.question = true
• Phenomena.Polarity.Studies.Lahiri1998.isDEOrQuestion Phenomena.Polarity.NPIs.LicensingContext.adversative = true
• Phenomena.Polarity.Studies.Lahiri1998.isDEOrQuestion Phenomena.Polarity.NPIs.LicensingContext.denyVerb = true
• Phenomena.Polarity.Studies.Lahiri1998.isDEOrQuestion x✝ = false

theorem Phenomena.Polarity.Studies.Lahiri1998.grammatical_contexts_are_de : ((List.filter (fun (x : NPIs.NPIDatum) => x.grammatical) allHindiNPIData).all fun (d : NPIs.NPIDatum) => match d.context with | some ctx => isDEOrQuestion ctx | none => false) = true

@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 Phenomena.Polarity.Studies.Lahiri1998.SubjectNPIContrast : Type

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

def Phenomena.Polarity.Studies.Lahiri1998.instReprSubjectNPIContrast.repr : SubjectNPIContrast → ℕ → Std.Format

Equations

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

instance Phenomena.Polarity.Studies.Lahiri1998.instReprSubjectNPIContrast : Repr SubjectNPIContrast

Equations

• Phenomena.Polarity.Studies.Lahiri1998.instReprSubjectNPIContrast = { reprPrec := Phenomena.Polarity.Studies.Lahiri1998.instReprSubjectNPIContrast.repr }

def Phenomena.Polarity.Studies.Lahiri1998.subjectNPI : SubjectNPIContrast

Equations

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

theorem Phenomena.Polarity.Studies.Lahiri1998.hindi_allows_subject_npi : subjectNPI.hindiGrammatical = true

theorem Phenomena.Polarity.Studies.Lahiri1998.english_blocks_subject_npi : subjectNPI.englishGrammatical = false

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 Phenomena.Polarity.Studies.Lahiri1998.koiiBhii_is_fci : Fragments.Hindi.PolarityItems.koiiBhii.polarityType = Core.Lexical.PolarityItem.PolarityType.fci

theorem Phenomena.Polarity.Studies.Lahiri1998.koiiNahiin_is_npi : Fragments.Hindi.PolarityItems.koiiNahiin.polarityType = Core.Lexical.PolarityItem.PolarityType.npiWeak

theorem Phenomena.Polarity.Studies.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 Phenomena.Polarity.Studies.Lahiri1998.fragment_morphology_matches : Fragments.Hindi.PolarityItems.koiiBhii.morphology = Core.Lexical.PolarityItem.NPIMorphology.indefPlusEven ∧ Fragments.Hindi.PolarityItems.koiiNahiin.morphology = Core.Lexical.PolarityItem.NPIMorphology.indefPlusNeg

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

theorem Phenomena.Polarity.Studies.Lahiri1998.fragment_alternativeType_matches : Fragments.Hindi.PolarityItems.koiiBhii.alternativeType = Core.Lexical.PolarityItem.AlternativeType.contextualProperty ∧ alternativeTypeOf koiiBhiiD = Core.Lexical.PolarityItem.AlternativeType.contextualProperty

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