Rett (2015): evaluativity as implicature

[Ret15] derives the distribution of evaluativity across degree constructions (the book's Table 3.1) from two Neo-Gricean implicatures: a Quantity implicature strengthens the otherwise tautological positive construction (Chapter 3), and the Marked Meaning Principle (Chapter 5, after [Hor84]'s division of pragmatic labor) makes the marked, negative antonym evaluative in exactly the polar-invariant constructions — equatives and degree questions — where its unmarked antonym has the same truth conditions. Antonym polarity is the adjective's Adjective.polarity, the ScalePolarity that Degree.equativeSem and Degree.comparativeSem already take as their direction; negative antonyms are the marked members of their pairs ([Bie89], [Ken07]).

Main definitions

• IsPolarInvariant: Rett's classification of constructions.
• implicature, Evaluative: the implicature route, if any, deriving evaluativity for a construction and polarity.
• evaluativity: the same for a fragment adjective, read off its lexicalized polarity.

Main results

• implicature_eq_manner_iff: the Marked Meaning Principle — Manner-derived evaluativity exactly for the marked antonym in a polar-invariant construction.
• exact_equative_antonym_invariant, comparative_antonym_variant: the equative and comparative rows of IsPolarInvariant derived from Degree.equativeSem and Degree.comparativeSem.
• evaluative_iff_observed: the predictions match every Table 3.1 judgment.

Polar (in)variance and markedness

def Rett2015.IsPolarInvariant : Degree.Construction → Prop

Rett's polar (in)variance: in a polar-invariant construction the two antonyms yield the same truth conditions, so the marked antonym has an unmarked competitor. Equatives and degree questions are polar-invariant; positives, comparatives, and measure phrases are not.

Equations

• Rett2015.IsPolarInvariant Degree.Construction.equative = True
• Rett2015.IsPolarInvariant Degree.Construction.degreeQuestion = True
• Rett2015.IsPolarInvariant Degree.Construction.positive = False
• Rett2015.IsPolarInvariant Degree.Construction.comparative = False
• Rett2015.IsPolarInvariant Degree.Construction.measurePhrase = False

@[instance_reducible]

instance Rett2015.instDecidablePredConstructionIsPolarInvariant : DecidablePred IsPolarInvariant

Equations

• Rett2015.instDecidablePredConstructionIsPolarInvariant Degree.Construction.equative = isTrue trivial
• Rett2015.instDecidablePredConstructionIsPolarInvariant Degree.Construction.degreeQuestion = isTrue trivial
• Rett2015.instDecidablePredConstructionIsPolarInvariant Degree.Construction.positive = isFalse Rett2015.instDecidablePredConstructionIsPolarInvariant._proof_1
• Rett2015.instDecidablePredConstructionIsPolarInvariant Degree.Construction.comparative = isFalse Rett2015.instDecidablePredConstructionIsPolarInvariant._proof_2
• Rett2015.instDecidablePredConstructionIsPolarInvariant Degree.Construction.measurePhrase = isFalse Rett2015.instDecidablePredConstructionIsPolarInvariant._proof_3

def Rett2015.IsMarked : Core.Order.ScalePolarity → Prop

Negative antonyms are the marked members of their pairs.

Equations

• Rett2015.IsMarked Core.Order.ScalePolarity.negative = True
• Rett2015.IsMarked Core.Order.ScalePolarity.positive = False

@[instance_reducible]

instance Rett2015.instDecidablePredScalePolarityIsMarked : DecidablePred IsMarked

Equations

• Rett2015.instDecidablePredScalePolarityIsMarked Core.Order.ScalePolarity.negative = isTrue trivial
• Rett2015.instDecidablePredScalePolarityIsMarked Core.Order.ScalePolarity.positive = isFalse Rett2015.instDecidablePredScalePolarityIsMarked._proof_1

The implicature derivation

inductive Rett2015.Implicature : Type

The implicature route deriving evaluativity: Quantity (Chapter 3's degree tautology) or Manner (Chapter 5's Marked Meaning Principle).

• quantity : Implicature
• manner : Implicature

@[instance_reducible]

instance Rett2015.instDecidableEqImplicature : DecidableEq Implicature

Equations

• Rett2015.instDecidableEqImplicature x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Rett2015.instReprImplicature.repr : Implicature → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Rett2015.instReprImplicature : Repr Implicature

Equations

• Rett2015.instReprImplicature = { reprPrec := Rett2015.instReprImplicature.repr }

def Rett2015.implicature : Degree.Construction → Core.Order.ScalePolarity → Option Implicature

The implicature deriving evaluativity for a construction and antonym polarity, if any: positives are strengthened by Quantity for both antonyms, and polar-invariant constructions get Manner-derived evaluativity for the marked antonym only.

Equations

• Rett2015.implicature Degree.Construction.positive x✝ = some Rett2015.Implicature.quantity
• Rett2015.implicature Degree.Construction.equative Core.Order.ScalePolarity.negative = some Rett2015.Implicature.manner
• Rett2015.implicature Degree.Construction.degreeQuestion Core.Order.ScalePolarity.negative = some Rett2015.Implicature.manner
• Rett2015.implicature x✝¹ x✝ = none

def Rett2015.Evaluative (c : Degree.Construction) (p : Core.Order.ScalePolarity) : Prop

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

Equations

• Rett2015.Evaluative c p = (Rett2015.implicature c p ≠ none)

@[instance_reducible]

instance Rett2015.instDecidableEvaluative (c : Degree.Construction) (p : Core.Order.ScalePolarity) : Decidable (Evaluative c p)

Equations

• Rett2015.instDecidableEvaluative c p = Rett2015.instDecidableEvaluative._aux_1 c p

theorem Rett2015.implicature_eq_manner_iff (c : Degree.Construction) (p : Core.Order.ScalePolarity) : implicature c p = some Implicature.manner ↔ IsPolarInvariant c ∧ IsMarked p

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

theorem Rett2015.implicature_eq_quantity_iff (c : Degree.Construction) (p : Core.Order.ScalePolarity) : implicature c p = some Implicature.quantity ↔ c = Degree.Construction.positive

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

theorem Rett2015.evaluative_iff (c : Degree.Construction) (p : Core.Order.ScalePolarity) : 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.

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

• Rett2015.evaluativity a c = a.polarity.bind (Rett2015.implicature c)

theorem Rett2015.as_short_as : evaluativity English.Predicates.Adjectival.short Degree.Construction.equative = some Implicature.manner

theorem Rett2015.as_tall_as : evaluativity English.Predicates.Adjectival.tall Degree.Construction.equative = none

theorem Rett2015.how_short : evaluativity English.Predicates.Adjectival.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.

theorem Rett2015.exact_equative_antonym_invariant {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (a b : Entity) : Degree.equativeSem μ a b Core.Order.ScalePolarity.positive ∧ ¬Degree.comparativeSem μ a b Core.Order.ScalePolarity.positive ↔ Degree.equativeSem μ a b Core.Order.ScalePolarity.negative ∧ ¬Degree.comparativeSem μ a b Core.Order.ScalePolarity.negative

"A is exactly as tall as B" and "A is exactly as short as B" are mutually entailing: each strengthened equative reduces to μ a = μ b.

theorem Rett2015.exact_equative_eq_strengthened {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (a b : Entity) : Degree.equativeSem μ a b Core.Order.ScalePolarity.positive ∧ ¬Degree.comparativeSem μ a b Core.Order.ScalePolarity.positive ↔ Degree.equativeStrengthened μ a b

Both strengthened antonym equatives are the "exactly" reading Degree.equativeStrengthened.

theorem Rett2015.comparative_antonyms_exclusive {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (a b : Entity) : Degree.comparativeSem μ a b Core.Order.ScalePolarity.positive → ¬Degree.comparativeSem μ a b Core.Order.ScalePolarity.negative

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

theorem Rett2015.comparative_antonym_variant {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (a b : Entity) (h : μ a ≠ μ b) : Degree.comparativeSem μ a b Core.Order.ScalePolarity.positive ↔ ¬Degree.comparativeSem μ a b Core.Order.ScalePolarity.negative

Whenever the antonyms could differ (μ a ≠ μ b), they do: the antonym comparatives have complementary truth conditions, so no truth-conditionally equivalent unmarked alternative exists.

Table 3.1

def Rett2015.datum (e : Data.Examples.LinguisticExample) : Option (Degree.Construction × Core.Order.ScalePolarity × Bool)

A Table 3.1 judgment: construction, 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.

def Rett2015.data : List (Degree.Construction × Core.Order.ScalePolarity × Bool)

The Table 3.1 judgments.

Equations

• Rett2015.data = List.filterMap Rett2015.datum Rett2015.Examples.all

theorem Rett2015.evaluative_iff_observed (d : Degree.Construction × Core.Order.ScalePolarity × Bool) : d ∈ data → (Evaluative d.1 d.2.1 ↔ d.2.2 = true)

The predictions match every Table 3.1 judgment.