Documentation

Studies.Chierchia2013

Chierchia (2013): Logic in Grammar #

This file formalizes the opening chapter of Chierchia's book, where the preferred reading of or and the distribution of any and ever are shown to track one logical property of a position. Or is exclusive in an upward-entailing position and inclusive in a downward-entailing one, because Maximize Strength adds the not-both implicature only where it strengthens, and an implicature strengthens under a monotone embedding and weakens under an antitone one. Any and ever are grammatical in the downward-entailing positions and out elsewhere, because their subdomain alternatives are obligatorily active and must be exhaustified: under an antitone context every subdomain alternative is entailed and exhaustification is vacuous, while at the existential itself no witness is entailed and exhaustification is a contradiction. Any alone extends to the free-choice positions, a possibility modal or an imperative, the divide between it and ever and between Italian qualsiasi and alcuno. The positions are the paper's easy and hard columns, the hard column being the licensing contexts whose licensers fix their polarity, and the readings and judgments are rows: the theorems derive each reading from Maximize Strength and each judgment from the licensing relation applied to the Fragment entries, and every row must name its position.

References #

Maximize Strength #

source
inductive Chierchia2013.DisjunctionReading :
Type

Or has an inclusive and an exclusive reading.

Instances For
    source
    @[instance_reducible]
    instance Chierchia2013.instDecidableEqDisjunctionReading :
    DecidableEq DisjunctionReading
    Equations
    source
    def Chierchia2013.instReprDisjunctionReading.repr :
    DisjunctionReading → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[instance_reducible]
      instance Chierchia2013.instReprDisjunctionReading :
      Repr DisjunctionReading
      Equations
      source
      def Chierchia2013.DisjunctionReading.denotation {W : Type u_1} (p q : Set W) :
      DisjunctionReading → Set W

      A reading assigns to p or q the disjunction, or the disjunction with the not-both implicature added.

      Equations
      Instances For
        source
        def Chierchia2013.DisjunctionReading.key :
        DisjunctionReading → String

        The name of a reading in the example rows.

        Equations
        Instances For
          source
          theorem Chierchia2013.exclusive_subset_inclusive {W : Type u_1} (p q : Set W) :
          DisjunctionReading.denotation p q DisjunctionReading.exclusive ⊆ DisjunctionReading.denotation p q DisjunctionReading.inclusive

          The not-both implicature strengthens the disjunction.

          source
          def Chierchia2013.IsStrongest {W : Type u_1} (p q : Set W) (C : Set W → Set W) (r : DisjunctionReading) :
          Prop

          By Maximize Strength a reading is preferred in a position when the position's embedding of it is at least as strong as its embedding of the other reading.

          Equations
          Instances For
            source
            theorem Chierchia2013.isStrongest_exclusive {W : Type u_1} (p q : Set W) {C : Set W → Set W} (hC : Monotone C) :
            IsStrongest p q C DisjunctionReading.exclusive

            Under a monotone embedding the implicature still strengthens, so the exclusive reading is preferred.

            source
            theorem Chierchia2013.isStrongest_inclusive {W : Type u_1} (p q : Set W) {C : Set W → Set W} (hC : Antitone C) :
            IsStrongest p q C DisjunctionReading.inclusive

            Under an antitone embedding the implicature weakens, so the inclusive reading is preferred.

            source
            def Chierchia2013.maximizeStrength :
            SignType → Option DisjunctionReading

            The reading Maximize Strength selects from the polarity of a position; a non-monotone position selects neither.

            Equations
            Instances For
              source
              theorem Chierchia2013.isStrongest_maximizeStrength {W : Type u_1} (p q : Set W) {φ : NaturalLogic.Signature} {C : Set W → Set W} (hφ : φ.SoundFor C) (r : DisjunctionReading) :
              r ∈ maximizeStrength φ.sign → IsStrongest p q C r

              Under an embedding with a signature of the position's polarity, the reading Maximize Strength selects is the strongest.

              Exhaustifying obligatory subdomain alternatives #

              source
              theorem Chierchia2013.exh_antitone_eq {W : Type u_1} {E : Type u_2} (D : Finset E) (P : E → Set W) {C : Set W → Set W} (hC : Antitone C) :
              Exhaustification.exh (C '' supClosure (P '' ↑D)) (C (⋃ a ∈ D, P a)) = C (⋃ a ∈ D, P a)

              Under an antitone context the existential entails each of its subdomain alternatives, so any in a downward-entailing position is exhaustified vacuously, leaving a plain existential.

              source
              theorem Chierchia2013.exh_supClosure_eq_empty {W : Type u_1} {E : Type u_2} (D : Finset E) (P : E → Set W) (h : ∀ a ∈ D, ¬⋃ b ∈ D, P b ⊆ P a) :
              Exhaustification.exh (supClosure (P '' ↑D)) (⋃ a ∈ D, P a) = ∅

              At the existential itself, where no witness is entailed, exhaustifying the obligatory alternatives negates every singleton alternative and is a contradiction, which is the source of the deviance of any in a positive episodic sentence.

              The positions #

              source
              inductive Chierchia2013.Position :
              Type

              The paper's positions. In the easy column or is exclusive and any is out, in the hard column of [Lad79]'s licensing contexts or is inclusive and any is in, and in the free-choice positions any alone survives.

              • matrix : Position

                A positive sentence.

              • conditionalConsequent : Position

                The consequent of a conditional.

              • everyScope : Position

                The second argument of every.

              • positiveQuantifierScope : Position

                The scope of a positive quantifier such as somebody.

              • conditionalAntecedent : Position
              • universalRestrictor : Position

                The first argument of every.

              • negation : Position
              • nobody : Position
              • doubtVerb : Position

                The complement of doubt.

              • modalPossibility : Position
              • imperative : Position
              Instances For
                source
                @[instance_reducible]
                instance Chierchia2013.instDecidableEqPosition :
                DecidableEq Position
                Equations
                source
                def Chierchia2013.instReprPosition.repr :
                Position → ℕ → Std.Format
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  @[instance_reducible]
                  instance Chierchia2013.instReprPosition :
                  Repr Position
                  Equations
                  source
                  def Chierchia2013.Position.context :
                  Position → Option PolarityItem.LicensingContext

                  The licensing context a position is, if it is one.

                  Equations
                  Instances For
                    source
                    theorem Chierchia2013.carries_weak_conditionalAntecedent :
                    PolarityItem.LicensingContext.conditionalAntecedent.licenser.Carries PolarityItem.DEStrength.weak

                    The licensers of the downward-entailing positions carry weak strength, those of the modal positions do not.

                    source
                    theorem Chierchia2013.carries_weak_universalRestrictor :
                    PolarityItem.LicensingContext.universalRestrictor.licenser.Carries PolarityItem.DEStrength.weak
                    source
                    theorem Chierchia2013.carries_weak_negation :
                    PolarityItem.LicensingContext.negation.licenser.Carries PolarityItem.DEStrength.weak
                    source
                    theorem Chierchia2013.carries_weak_nobody :
                    PolarityItem.LicensingContext.nobody.licenser.Carries PolarityItem.DEStrength.weak
                    source
                    theorem Chierchia2013.carries_weak_doubtVerb :
                    PolarityItem.LicensingContext.doubtVerb.licenser.Carries PolarityItem.DEStrength.weak
                    source
                    theorem Chierchia2013.not_carries_weak_modalPossibility :
                    ¬PolarityItem.LicensingContext.modalPossibility.licenser.Carries PolarityItem.DEStrength.weak
                    source
                    theorem Chierchia2013.not_carries_weak_imperative :
                    ¬PolarityItem.LicensingContext.imperative.licenser.Carries PolarityItem.DEStrength.weak
                    source
                    def Chierchia2013.Position.Downward (p : Position) :
                    Prop

                    A position is downward entailing when it is a licensing context whose licenser carries weak strength.

                    Equations
                    Instances For
                      source
                      @[instance_reducible]
                      instance Chierchia2013.instDecidablePredPositionDownward :
                      DecidablePred Position.Downward
                      Equations
                      source
                      def Chierchia2013.Position.polarity (p : Position) :
                      SignType

                      A downward-entailing position is antitone, any other upward entailing.

                      Equations
                      Instances For
                        source
                        def Chierchia2013.Position.Licenses (p : Position) (e : PolarityItem) :
                        Prop

                        A position licenses an item when it is a licensing context that licenses it.

                        Equations
                        Instances For
                          source
                          theorem Chierchia2013.Position.licenses_iff {p : Position} {c : PolarityItem.LicensingContext} (h : p.context = some c) {e : PolarityItem} :
                          p.Licenses e ↔ c.licenser.Licenses e
                          source
                          @[instance_reducible]
                          instance Chierchia2013.instDecidablePredPolarityItemLicenses (p : Position) :
                          DecidablePred p.Licenses
                          Equations
                          source
                          theorem Chierchia2013.licenses_ever_of_downward (pos : Position) (h : pos.polarity = -1) :
                          pos.Licenses English.PolarityItems.ever

                          Every downward-entailing position licenses ever, so the hard column of the readings of or is the column where the pure negative-polarity item is grammatical.

                          source
                          theorem Chierchia2013.licenses_any_not_ever_iff (c : PolarityItem.LicensingContext) :
                          c.licenser.Licenses English.PolarityItems.any ∧ ¬c.licenser.Licenses English.PolarityItems.ever ↔ c.licenser.LicensesFreeChoice

                          Any parts ways with ever exactly where the context licenses free choice, as a possibility modal, an imperative or a generic does.

                          The rows #

                          source
                          def Chierchia2013.Position.ofKey :
                          String → Option Position

                          The position a row names.

                          Equations
                          Instances For
                            source
                            noncomputable def Chierchia2013.item :
                            String → Option PolarityItem

                            The Fragment entry a row names.

                            Equations
                            Instances For
                              source
                              theorem Chierchia2013.or_rows (e : Datum) :
                              e ∈ Examples.all → e.feature? "item" = some "or" → e.feature? "forced" = none → ∃ pos ∈ (e.feature? "position").bind Position.ofKey, e.feature? "reading" = Option.map DisjunctionReading.key (maximizeStrength pos.polarity)

                              Every unforced row on or names a position, and its reading is the one Maximize Strength selects from the polarity of that position.

                              source
                              theorem Chierchia2013.exclusive_under_nobody_forced :
                              ∃ e ∈ Examples.all, e.feature? "forced" = some "true" ∧ e.feature? "position" = some "nobody" ∧ e.feature? "reading" = some "exclusive"

                              The exclusive reading is available under nobody, but only forced by the context.

                              source
                              theorem Chierchia2013.polarity_rows (e : Datum) :
                              e ∈ Examples.all → e.feature? "item" ≠ some "or" → ∃ i ∈ (e.feature? "item").bind item, ∃ pos ∈ (e.feature? "position").bind Position.ofKey, e.judgment = Judgment.acceptable ↔ pos.Licenses i

                              Every row on another item names a Fragment entry and a position, and is judged acceptable exactly when the position licenses the entry.