Documentation

Studies.Lahiri1998

Lahiri (1998): Focus and negative polarity in Hindi #

This file formalizes the paper's account of the Hindi negative polarity items, each a weak indefinite plus the focus particle bhii 'even' (HindiUrdu.PolarityItems). The scalar presupposition of even, that the prejacent is less likely than every focus alternative, clashes with an entailment-monotone likelihood exactly when an alternative entails the prejacent (Focus.Particles.not_evenPresup_of_subset). The indefinite is the weakest predicate, so in an upward-entailing context every alternative entails the assertion and the presupposition is contradictory (ue_clash), while a downward-entailing operator reverses the entailments and leaves it satisfiable (de_presup); the restriction of a generic, read as a universal under the paper's background assumption, is such a slot (generic_presup), as are the negative-expectation reading of a question and the permission reading of an imperative. Clausemate negation takes scope over a Hindi subject indefinite, which is why Hindi licenses subject NPIs where English does not (clausemate_negation). The judgments of the paper's survey are rows, which analysis_matches_judgments reads as the analysis predicts, apart from the numeral and measure items ek bhii and zaraa bhii in imperatives and with numerals, whose cardinality alternatives the paper distinguishes from the contextual alternatives of koii bhii and kuch bhii and whose exclusion it leaves open (cardinality_exceptions).

Implementation notes #

A likelihood is a monotone map from propositions into a partial order, and the alternatives an item introduces are a list of predicates, cardinalities or contextual properties, each at most as strong as the weakest predicate ⊤, the paper's one. The generic operator is read as a universal quantifier, which the paper grants on the background assumption that the exceptions the alternatives tolerate are exceptions the assertion tolerates too; the permission analysis of imperatives and the two implicature sets of a question are instances of de_presup and ue_clash and are not restated. The environments of the survey are classified as the analysis classifies them, downward entailing, generic, or neither; necessity modals and the episodic readings of possibility modals and the future are among the last, which the paper reports without deriving. The oblique forms kisii-ko, kisii-se, and kisiike are koii's.

References #

The implicature clash (§7, §8) #

source
def Lahiri1998.exist {World : Type u_1} {Ent : Type u_2} (P : Ent → Prop) (φ : World → Ent → Prop) :
Set World

exist P φ is the existential assertion of an indefinite restricted by P, true where some P-entity satisfies φ.

Equations
Instances For
    source
    def Lahiri1998.restrict {World : Type u_1} {Ent : Type u_2} (P : Ent → Prop) (φ : World → Ent → Prop) :
    Set World

    restrict P φ is the universal reading of a generic restricted by P, true where every P-entity satisfies φ.

    Equations
    Instances For
      source
      theorem Lahiri1998.exist_mono {World : Type u_1} {Ent : Type u_2} {φ : World → Ent → Prop} :
      Monotone fun (x : Ent → Prop) => exist x φ
      source
      theorem Lahiri1998.restrict_anti {World : Type u_1} {Ent : Type u_2} {φ : World → Ent → Prop} :
      Antitone fun (x : Ent → Prop) => restrict x φ
      source
      theorem Lahiri1998.exist_subset_exist_top {World : Type u_1} {Ent : Type u_2} {φ : World → Ent → Prop} (P : Ent → Prop) :
      exist P φ ⊆ exist ⊤ φ

      The weakest predicate is true of everything, so every alternative entails the existential assertion.

      source
      theorem Lahiri1998.restrict_top_subset {World : Type u_1} {Ent : Type u_2} {φ : World → Ent → Prop} (P : Ent → Prop) :
      restrict ⊤ φ ⊆ restrict P φ

      The universal assertion on the weakest predicate entails every alternative.

      source
      def Lahiri1998.alternatives {World : Type u_1} {Ent : Type u_2} (Ps : Set (Ent → Prop)) (φ : World → Ent → Prop) :
      Set (Set World)

      The focus alternatives bhii induces from alternative predicates.

      Equations
      Instances For
        source
        theorem Lahiri1998.ue_clash {World : Type u_1} {Ent : Type u_2} {α : Type u_3} [PartialOrder α] {μ : Set World → α} {φ : World → Ent → Prop} {Ps : Set (Ent → Prop)} (hμ : Monotone μ) (hPs : Ps.Nonempty) :
        ¬Focus.Particles.evenPresup μ (exist ⊤ φ) (alternatives Ps φ)

        In an upward-entailing context the presupposition of bhii is contradictory as soon as there is an alternative, cardinality or contextual property, since each entails the assertion and so is at least as likely.

        source
        theorem Lahiri1998.de_presup {World : Type u_1} {Ent : Type u_2} {α : Type u_3} [PartialOrder α] {μ : Set World → α} {φ : World → Ent → Prop} {Ps : Set (Ent → Prop)} (hμ : Monotone μ) {Q : Set World → Set World} (hQ : Antitone Q) :
        Focus.Particles.evenPresup μ (Q (exist ⊤ φ)) (Q '' alternatives Ps φ) ↔ ∀ P ∈ Ps, μ (Q (exist ⊤ φ)) ≠ μ (Q (exist P φ))

        A downward-entailing operator reverses the entailments, so under it the presupposition asks only that no alternative be exactly as likely; negation, the complement of a prohibition verb, and the permission an imperative grants are such operators.

        source
        theorem Lahiri1998.clausemate_negation {World : Type u_1} {Ent : Type u_2} {α : Type u_3} [PartialOrder α] {μ : Set World → α} {φ : World → Ent → Prop} {Ps : Set (Ent → Prop)} (hμ : Monotone μ) (hPs : Ps.Nonempty) :
        ¬Focus.Particles.evenPresup μ (exist ⊤ φ) (alternatives Ps φ) ∧ (Focus.Particles.evenPresup μ (exist ⊤ φ)ᶜ (compl '' alternatives Ps φ) ↔ ∀ P ∈ Ps, μ (exist ⊤ φ)ᶜ ≠ μ (exist P φ)ᶜ) ∧ ¬Focus.Particles.evenPresup μ (exist ⊤ fun (w : World) (x : Ent) => ¬φ w x) (alternatives Ps fun (w : World) (x : Ent) => ¬φ w x)

        Of koii bhii aayaa and koii bhii nahiiN aayaa, and of the two implicature sets of a yes-no question, the positive reading clashes and the negative one is satisfiable. Negation inside the existential, the only scope English gives a subject indefinite, is again a positive context, which is why English lacks the subject NPIs that Hindi licenses.

        source
        theorem Lahiri1998.generic_presup {World : Type u_1} {Ent : Type u_2} {α : Type u_3} [PartialOrder α] {μ : Set World → α} {φ : World → Ent → Prop} {Ps : Set (Ent → Prop)} (hμ : Monotone μ) :
        Focus.Particles.evenPresup μ (restrict ⊤ φ) ((fun (x : Ent → Prop) => restrict x φ) '' Ps) ↔ ∀ P ∈ Ps, μ (restrict ⊤ φ) ≠ μ (restrict P φ)

        In the restriction of a generic the assertion entails every alternative, so the presupposition is satisfiable and the free-choice reading licensed.

        The survey (§4–§6, §8–§10) #

        source
        inductive Lahiri1998.Environment :
        Type

        The environments of the survey.

        Instances For
          source
          @[instance_reducible]
          instance Lahiri1998.instDecidableEqEnvironment :
          DecidableEq Environment
          Equations
          source
          def Lahiri1998.instReprEnvironment.repr :
          Environment → ℕ → Std.Format
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[instance_reducible]
            instance Lahiri1998.instReprEnvironment :
            Repr Environment
            Equations
            source
            def Lahiri1998.Environment.Licensed :
            Environment → Prop

            The analysis licenses an indefinite plus bhii in the downward-entailing environments, in questions on their negative-expectation reading, and in the generic environments, which are generics with or without a numeral, generically read possibility modals and futures, and imperatives read as permissions.

            Equations
            Instances For
              source
              @[instance_reducible]
              instance Lahiri1998.instDecidablePredEnvironmentLicensed :
              DecidablePred Environment.Licensed
              Equations
              source
              inductive Lahiri1998.Alternatives :
              Type

              An indefinite plus bhii introduces other cardinality or measure predicates as its alternatives for ek 'one' and zaraa 'a little', and a contextually specified set of properties for koii and kuch (§8).

              Instances For
                source
                @[instance_reducible]
                instance Lahiri1998.instDecidableEqAlternatives :
                DecidableEq Alternatives
                Equations
                source
                @[instance_reducible]
                instance Lahiri1998.instReprAlternatives :
                Repr Alternatives
                Equations
                source
                def Lahiri1998.instReprAlternatives.repr :
                Alternatives → ℕ → Std.Format
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  structure Lahiri1998.Row :
                  Type

                  A row is a judged example, recording its environment, the fragment entry of its item with the alternatives it introduces, and the judgment.

                  Instances For
                    source
                    noncomputable def Lahiri1998.item? (r : Datum) :
                    Option (PolarityItem × Alternatives)

                    The fragment entry of a row's item, with its alternatives; the paper does not classify kabhii bhii 'ever', read here with the property alternatives of koii and kuch.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      noncomputable def Lahiri1998.Row.ofDatum (r : Datum) :
                      Option Row

                      A row of the survey.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        noncomputable def Lahiri1998.data :
                        List Row

                        The survey.

                        Equations
                        Instances For
                          source
                          theorem Lahiri1998.analysis_matches_judgments (d : Row) :
                          d ∈ data → d.alternatives = Alternatives.property ∨ d.env ≠ Environment.imperative ∧ d.env ≠ Environment.numeralGeneric → (d.judgment = Judgment.acceptable ↔ d.env.Licensed)

                          Setting aside the cardinality items in imperatives and with numerals, an indefinite plus bhii in the survey is acceptable exactly in the environments the analysis licenses.

                          source
                          theorem Lahiri1998.cardinality_exceptions (d : Row) :
                          d ∈ data → d.alternatives = Alternatives.cardinality → d.env = Environment.imperative ∨ d.env = Environment.numeralGeneric → d.judgment ≠ Judgment.acceptable

                          The numeral and measure items, whose alternatives are cardinalities, are out with a numeral and odd in imperatives, where the analysis predicts them licensed; the paper leaves the imperative case open.