Documentation

Studies.Rett2015

Rett (2015): The semantics of evaluativity #

Rett derives the distribution of evaluativity across degree constructions, her Table 3.1, from two Neo-Gricean implicatures. A Quantity implicature strengthens the otherwise tautological positive construction, and the Marked Meaning Principle, after Horn's division of pragmatic labor, makes the marked, negative antonym evaluative in exactly the polar-invariant constructions, the equatives and degree questions in which its unmarked antonym has the same truth conditions.

Main results #

Implementation notes #

Antonym polarity is the adjective's Adjective.polarity, which acts on the comparison of its equative and comparative through the order dual, Polarity.negative • c = c.dual; negative antonyms are the marked members of their pairs (Bierwisch, Kennedy). The positive construction and the measure phrase have no polarity-parametrized semantics in the substrate, so their rows of IsPolarInvariant are the book's classification.

References #

Polar (in)variance and markedness #

source
def Rett2015.IsPolarInvariant :
Degree.Construction → Prop

A construction is polar-invariant, in Rett's sense, when the two antonyms yield the same truth conditions in it, so that the marked antonym has an unmarked competitor. Equatives and degree questions are polar-invariant; positives, comparatives, and measure phrases are not.

Equations
Instances For
    source
    @[instance_reducible]
    instance Rett2015.instDecidablePredConstructionIsPolarInvariant :
    DecidablePred IsPolarInvariant
    Equations
    source
    def Rett2015.IsMarked (p : Polarity) :
    Prop

    Negative antonyms are the marked members of their pairs.

    Equations
    Instances For
      source
      @[instance_reducible]
      instance Rett2015.instDecidablePredPolarityIsMarked :
      DecidablePred IsMarked
      Equations

      The implicature derivation #

      source
      inductive Rett2015.Implicature :
      Type

      Evaluativity is derived by a Quantity implicature (Chapter 3's degree tautology) or a Manner implicature (Chapter 5's Marked Meaning Principle).

      Instances For
        source
        @[instance_reducible]
        instance Rett2015.instDecidableEqImplicature :
        DecidableEq Implicature
        Equations
        source
        @[instance_reducible]
        instance Rett2015.instReprImplicature :
        Repr Implicature
        Equations
        source
        def Rett2015.instReprImplicature.repr :
        Implicature → ℕ → Std.Format
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Rett2015.implicature (c : Degree.Construction) (p : Polarity) :
          Option Implicature

          The implicature deriving evaluativity for a construction and antonym polarity, if any, is Quantity for the positive construction with either antonym, and Manner, by the Marked Meaning Principle, for the marked antonym of a polar-invariant construction.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Rett2015.Evaluative (c : Degree.Construction) (p : Polarity) :
            Prop

            A construction–polarity pair is evaluative iff some implicature derives it.

            Equations
            Instances For
              source
              @[instance_reducible]
              instance Rett2015.instDecidableEvaluative (c : Degree.Construction) (p : Polarity) :
              Decidable (Evaluative c p)
              Equations
              source
              theorem Rett2015.implicature_eq_manner_iff (c : Degree.Construction) (p : Polarity) :
              implicature c p = some Implicature.manner ↔ IsPolarInvariant c ∧ IsMarked p

              The Marked Meaning Principle makes evaluativity Manner-derived exactly for the marked antonym in a polar-invariant construction.

              source
              theorem Rett2015.implicature_eq_quantity_iff (c : Degree.Construction) (p : Polarity) :
              implicature c p = some Implicature.quantity ↔ c = Degree.Construction.positive

              Quantity-derived evaluativity is the positive construction's alone.

              source
              theorem Rett2015.evaluative_iff (c : Degree.Construction) (p : Polarity) :
              Evaluative c p ↔ c = Degree.Construction.positive ∨ IsPolarInvariant c ∧ IsMarked p

              Evaluativity is the positive construction or the Marked Meaning Principle.

              The book's contrasts #

              Chapter 1's How short is Adam? and Adam is as short as Doug are evaluative; their positive-antonym counterparts are not.

              source
              def Rett2015.evaluativity (a : Degree.GradableAdjective) (c : Degree.Construction) :
              Option Implicature

              The implicature deriving evaluativity for a fragment adjective in a construction, read off its lexicalized polarity.

              Equations
              Instances For
                source
                theorem Rett2015.as_short_as :
                evaluativity English.Adjectives.short Degree.Construction.equative = some Implicature.manner
                source
                theorem Rett2015.as_tall_as :
                evaluativity English.Adjectives.tall Degree.Construction.equative = none
                source
                theorem Rett2015.how_short :
                evaluativity English.Adjectives.short Degree.Construction.degreeQuestion = some Implicature.manner

                Polar variance grounded in the comparison semantics #

                [Ret15] reduces polar (in)variance to mutual entailment of the antonyms' non-evaluative readings: the strengthened ("exactly") equatives of the two antonyms share truth conditions, so a truth-conditionally equivalent unmarked alternative exists and the Marked Meaning Principle can fire; the antonym comparatives exclude each other, so no such alternative exists. Degree questions pattern with the equative — both antonyms' true answers are the subject's actual measure.

                source
                theorem Rett2015.exact_equative_iff_eq {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (a b : Entity) (p : Polarity) :
                a ∈ μ ⁻¹' (p • Degree.Comparison.ge).interval (μ b) ∧ a ∉ μ ⁻¹' (p • Degree.Comparison.gt).interval (μ b) ↔ μ a = μ b

                The strengthened equative of an adjective of either polarity, as tall as and not taller than or as short as and not shorter than, holds exactly when the two measures are equal.

                source
                theorem Rett2015.exact_equative_antonym_invariant {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (a b : Entity) (p : Polarity) :
                a ∈ μ ⁻¹' (p • Degree.Comparison.ge).interval (μ b) ∧ a ∉ μ ⁻¹' (p • Degree.Comparison.gt).interval (μ b) ↔ a ∈ μ ⁻¹' ((Polarity.negative * p) • Degree.Comparison.ge).interval (μ b) ∧ a ∉ μ ⁻¹' ((Polarity.negative * p) • Degree.Comparison.gt).interval (μ b)

                The strengthened equatives of two antonyms, exactly as tall as and exactly as short as, are mutually entailing.

                source
                theorem Rett2015.comparative_antonyms_exclusive {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (a b : Entity) (p : Polarity) (h : a ∈ μ ⁻¹' (p • Degree.Comparison.gt).interval (μ b)) :
                a ∉ μ ⁻¹' ((Polarity.negative * p) • Degree.Comparison.gt).interval (μ b)

                The antonym comparatives exclude each other, so A is taller than B and A is shorter than B cannot both hold.

                source
                theorem Rett2015.comparative_antonym_variant {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (a b : Entity) (p : Polarity) (h : μ a ≠ μ b) :
                a ∈ μ ⁻¹' (p • Degree.Comparison.gt).interval (μ b) ↔ a ∉ μ ⁻¹' ((Polarity.negative * p) • Degree.Comparison.gt).interval (μ b)

                Wherever the antonyms could differ, μ a ≠ μ b, their comparatives are complementary, so no truth-conditionally equivalent unmarked alternative exists.

                Table 3.1 #

                source
                def Rett2015.datum (e : Datum) :
                Option (Degree.Construction × Polarity × Bool)

                A Table 3.1 judgment records the construction, the antonym polarity, and whether the sentence is evaluative. The ungrammatical negative-antonym measure phrase carries no judgment.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  def Rett2015.data :
                  List (Degree.Construction × Polarity × Bool)

                  The Table 3.1 judgments.

                  Equations
                  Instances For
                    source
                    theorem Rett2015.evaluative_iff_observed (d : Degree.Construction × Polarity × Bool) :
                    d ∈ data → (Evaluative d.1 d.2.1 ↔ d.2.2 = true)

                    The predictions match every Table 3.1 judgment.