Lahiri 1998 — Focus and negative polarity in Hindi

Hindi NPIs (koii bhii 'anyone', ek bhii 'even one', kuch bhii 'anything', zaraa bhii 'even a little') are morphologically an indefinite plus the focus particle bhii 'even' (paper (1), p. 58). [Lah98] derives their distribution — as NPIs and as free-choice items — compositionally: bhii contributes the scalar implicature ([KP79]) that the assertion is least likely among the focus alternatives, and the weak indefinite sits at the bottom of the entailment scale. In UE contexts every alternative entails the assertion, making it the most likely — the implicature is contradicted (§7.4). In DE contexts entailment reverses and the implicature is satisfiable. Free-choice readings arise where the implicature is satisfiable in generic and possibility-modal contexts (§5, §7.6); ek bhii's cardinality alternatives vs koii bhii's contextual-property alternatives explain their contrasts (§8). The judged stimuli live in Data/Examples/Lahiri1998.json (Examples.ex6a, …).

Morphological decomposition (paper (1), p. 58)

Every item in the paradigm is a weak indefinite plus bhii. The kind of alternatives an item activates (cardinality vs contextually salient properties, §8) is a lexical property, stored on the fragment entries in Hindi.PolarityItems. (kahiiN bhii's licensed uses in the paper are correlatives, §4.4, an environment not modeled here.)

structure Lahiri1998.NPIDecomposition : Type

A row of the paper's decomposition table (1): base indefinite and the bhii-compound, with the paper's glosses.

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

@[instance_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.hindiNPIs : List NPIDecomposition

The paper's decomposition table ((1), p. 58).

Equations

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

theorem Lahiri1998.npiForm_eq_base_bhii (d : NPIDecomposition) : d ∈ hindiNPIs → d.npiForm = d.base ++ " bhii"

Morphological uniformity: every NPI form is its base plus bhii.

The cardinality model

The scale ∃x[n(x) ∧ VP(x)] over a four-world model (Fin 4): world 0 = at least three entities satisfy the VP, 1 = exactly two, 2 = exactly one, 3 = none.

def Lahiri1998.atLeastOneB : Fin 4 → Bool

At least one entity satisfies the VP (Bool form).

Equations

• Lahiri1998.atLeastOneB w = (w != 3)

def Lahiri1998.atLeastTwoB : Fin 4 → Bool

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

Equations

• Lahiri1998.atLeastTwoB w = (w == 0 || w == 1)

def Lahiri1998.atLeastThreeB : Fin 4 → Bool

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

Equations

• Lahiri1998.atLeastThreeB w = (w == 0)

def Lahiri1998.atLeastOne : Set (Fin 4)

At least one entity satisfies the VP. True at 0, 1, 2.

Equations

• Lahiri1998.atLeastOne = {w : Fin 4 | Lahiri1998.atLeastOneB w = true}

def Lahiri1998.atLeastTwo : Set (Fin 4)

At least two entities satisfy the VP. True at 0, 1.

Equations

• Lahiri1998.atLeastTwo = {w : Fin 4 | Lahiri1998.atLeastTwoB w = true}

def Lahiri1998.atLeastThree : Set (Fin 4)

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

Equations

• Lahiri1998.atLeastThree = {w : Fin 4 | Lahiri1998.atLeastThreeB w = true}

Weakness of one (§7.4, eq. 70)

one is the weakest cardinality predicate: every atLeastN proposition entails atLeastOne, and not conversely.

theorem Lahiri1998.two_entails_one : atLeastTwo ⊆ atLeastOne

theorem Lahiri1998.three_entails_one : atLeastThree ⊆ atLeastOne

theorem Lahiri1998.three_entails_two : atLeastThree ⊆ atLeastTwo

theorem Lahiri1998.one_not_entails_two : ¬atLeastOne ⊆ atLeastTwo

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

theorem Lahiri1998.one_not_entails_three : ¬atLeastOne ⊆ atLeastThree

The implicature clash (§7.4, eqs. 66–79)

In UE, each alternative the ⊆ assertion, so a monotone likelihood ordering makes the assertion most likely — but EVEN demands it be least likely. Under negation the entailments reverse and EVEN is satisfiable.

theorem Lahiri1998.ue_alt_entails_assertion : atLeastTwo ⊆ atLeastOne ∧ atLeastThree ⊆ atLeastOne

UE pattern: all alternatives entail the assertion — fatal for EVEN.

theorem Lahiri1998.de_assertion_entails_alt : atLeastOneᶜ ⊆ atLeastTwoᶜ ∧ atLeastOneᶜ ⊆ atLeastThreeᶜ

DE pattern: the assertion all ⊆ alternatives — EVEN is satisfiable.

theorem Lahiri1998.ue_not_reverse : ¬atLeastOne ⊆ atLeastTwo ∧ ¬atLeastOne ⊆ atLeastThree

In UE the assertion does NOT entail the alternatives.

theorem Lahiri1998.de_not_reverse : ¬atLeastTwoᶜ ⊆ atLeastOneᶜ ∧ ¬atLeastThreeᶜ ⊆ atLeastOneᶜ

In DE the alternatives do NOT entail the assertion.

The clash through the EVEN presupposition

theorem Lahiri1998.even_clash_abstract {W : Type u_1} (lt le : Set W → Set W → Prop) (hMono : Focus.Particles.LikelihoodMonotone le) (hCompat : ∀ (a b : Set W), lt a b → le b a → False) {assertion alt : Set W} (hEntails : alt ⊆ assertion) (hEven : lt assertion alt) : False

An EVEN scalar implicature is contradicted whenever the assertion is entailed by an alternative: the alternative is then at most as likely, but EVEN requires the assertion to be strictly less likely.

theorem Lahiri1998.ekBhii_even_clash_UE (lt le : Set (Fin 4) → Set (Fin 4) → Prop) (hMono : Focus.Particles.LikelihoodMonotone le) (hCompat : ∀ (a b : Set (Fin 4)), lt a b → le b a → False) (hEven : Focus.Particles.evenPresup lt atLeastOne [atLeastTwo, atLeastThree]) : False

In UE, the EVEN presupposition for ek bhii is contradicted (§7.4, eqs. 68–71).

theorem Lahiri1998.ekBhii_even_ok_DE : atLeastOneᶜ ⊆ atLeastTwoᶜ ∧ atLeastOneᶜ ⊆ atLeastThreeᶜ

In DE, the EVEN presupposition for ek bhii nahiiN is satisfiable: the negated assertion each ⊆ negated alternative (§7.4, eqs. 76–79).

NPI data (§4, §6)

Licensing judgments from [Lah98] §4 and §6 (stimuli in Data/Examples/Lahiri1998.json), paired with this study's analysis of each environment: bhii + indefinite is licensed in DE contexts and blocked in UE contexts. The adversative rescue in (31b) is [KL93]'s "settle for less".

structure Lahiri1998.HindiNPIDatum : Type

A judged example paired with the licensing context of the analysis (none = unlicensed environment).

• ex : Data.Examples.LinguisticExample
• context : Option Polarity.LicensingContext

def Lahiri1998.allHindiNPIData : List HindiNPIDatum

The §4/§6 judgment data with per-environment analyses.

Equations

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

@[reducible, inline]

abbrev Lahiri1998.isDEOrQuestion (c : Polarity.LicensingContext) : Prop

A DE-or-question licenser, derived from LicensingContext.properties: the context's Strawson row supplies Zwarts strength, or it licenses by entropy (questions license via negative bias rather than pure DE).

Equations

• Lahiri1998.isDEOrQuestion c = (c.properties.strawsonSignature.toDEStrength.isSome = true ∨ c.properties.mechanism = Polarity.LicensingMechanism.byEntropy)

def Lahiri1998.hasDELicenser (d : HindiNPIDatum) : Prop

The datum's context is some DE-or-question licenser.

Equations

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

@[instance_reducible]

instance Lahiri1998.instDecidablePredHindiNPIDatumHasDELicenser : DecidablePred hasDELicenser

Equations

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

theorem Lahiri1998.licensed_iff_acceptable (d : HindiNPIDatum) : d ∈ allHindiNPIData → (d.context.isSome = true ↔ d.ex.judgment = Features.Judgment.acceptable)

The analysis licenses exactly the acceptable data: a datum has a licensing context iff the paper judges its example acceptable.

theorem Lahiri1998.grammatical_contexts_are_de (d : HindiNPIDatum) : d ∈ allHindiNPIData → d.ex.judgment = Features.Judgment.acceptable → hasDELicenser d

Every acceptable datum's licensing context is DE (or a question): the distribution follows the implicature-clash prediction.

Free choice in generic and modal contexts (§5)

Hindi NPIs are free-choice items in generic sentences and under possibility modals, but not under necessity modals; the GEN restriction is a strengthening environment, so the EVEN implicature is satisfiable there (§7.6, eqs. 95–98).

structure Lahiri1998.FCDatum : Type

A judged free-choice example paired with the environment tested.

• ex : Data.Examples.LinguisticExample
• contextType : Polarity.LicensingContext

def Lahiri1998.allFCData : List FCDatum

The §5 free-choice data.

Equations

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

theorem Lahiri1998.generic_and_possibility_license (d : FCDatum) : d ∈ allFCData → d.contextType = Polarity.LicensingContext.generic ∨ d.contextType = Polarity.LicensingContext.modalPossibility → d.ex.judgment = Features.Judgment.acceptable

Generics and possibility modals license FC readings.

theorem Lahiri1998.necessity_blocks (d : FCDatum) : d ∈ allFCData → d.contextType = Polarity.LicensingContext.modalNecessity → d.ex.judgment ≠ Features.Judgment.acceptable

Necessity modals block FC readings.

The ek bhii / koii bhii contrast (§8)

The first approximation treats koii bhii and ek bhii as equivalent, but ek activates cardinality alternatives (other numerals) while koii activates contextually salient properties — only the latter yield free-choice readings ((99), repeating Examples.ex36a/ex36b), and cardinality alternatives clash with explicit numerals ((100)).

theorem Lahiri1998.numeral_contrast : Examples.ex100a.judgment = Features.Judgment.acceptable ∧ Examples.ex100b.judgment ≠ Features.Judgment.acceptable

With an explicit numeral, koii bhii is fine and ek bhii is blocked ((100a) vs (100b)).

theorem Lahiri1998.contrast_is_lexical : Hindi.PolarityItems.ekBhii.alternativeType = Polarity.AlternativeType.cardinality ∧ Hindi.PolarityItems.koiiBhii.alternativeType = Polarity.AlternativeType.contextualProperty

§8's contrast is lexical: the fragment's ek bhii activates cardinality alternatives, koii bhii contextual properties.

theorem Lahiri1998.cardinality_items_resist_imperatives (i : Polarity.Item) : i ∈ Hindi.PolarityItems.bhiiItems → i.alternativeType = Polarity.AlternativeType.cardinality → Polarity.LicensingContext.imperative ∉ i.licensingContexts

The imperative asymmetry ((39) vs (40)): the cardinality-alternative items are exactly the ones whose attested contexts exclude imperatives.

Fragment grounding

The fragment entries in Hindi.PolarityItems store the distribution this study derives: DE environments for NPI readings, generic/modal environments for FC readings, necessity modals excluded ((36d)).

theorem Lahiri1998.koiiBhii_fragment_grounded : Hindi.PolarityItems.koiiBhii.licensor = some Polarity.DEStrength.weak ∧ Hindi.PolarityItems.koiiBhii.freeChoice = true ∧ Hindi.PolarityItems.koiiBhii.morphology = Polarity.NPIMorphology.indefPlusEven ∧ Polarity.LicensingContext.negation ∈ Hindi.PolarityItems.koiiBhii.licensingContexts ∧ Polarity.LicensingContext.generic ∈ Hindi.PolarityItems.koiiBhii.licensingContexts ∧ Polarity.LicensingContext.modalNecessity ∉ Hindi.PolarityItems.koiiBhii.licensingContexts

The fragment's koii bhii matches the analysis: a dual NPI/FC item with indefinite + even morphology, licensed under negation ((6b)) and in generics ((35a)) but not under necessity modals ((36d)).

theorem Lahiri1998.koiiNahiin_fragment_grounded : Hindi.PolarityItems.koiiNahiin.licensor = some Polarity.DEStrength.weak ∧ Hindi.PolarityItems.koiiNahiin.morphology = Polarity.NPIMorphology.indefPlusNeg

The fragment's koii nahiiN is a strength-licensed NPI with indefinite + negation morphology — the non-bhii route.