[Ret15] — Neo-Gricean Account of Evaluativity

[Ret15] [Hor84] [Bie89] [Ken07] [LG17]

Self-contained study of [Ret15] "The Semantics of Evaluativity" Chapters 3–5: theoretical analysis (Q-implicature, Marked Meaning Principle, markedness machinery) plus prediction-matching against the empirical data from Rett2015.lean.

Insight

Evaluativity (the requirement that a degree exceed a contextual standard) is NOT semantically encoded but derived pragmatically via implicature.

Two Implicature Types

1. Quantity implicature (Q-principle):

   • For positive constructions ("John is tall")
   • Without evaluativity, the utterance is uninformative
   • Listener strengthens to evaluative reading

2. Manner implicature (R-principle):

   • For polar-INVARIANT constructions (equatives, questions)
   • "How tall?" and "How short?" have the SAME truth conditions
   • Using marked "short" when unmarked "tall" exists signals something extra
   • That extra is evaluativity (presupposes shortness)

The Asymmetry Explained

Why do equatives show asymmetry (marked antonyms evaluative) but comparatives don't?

Polar variance is key:

• Comparatives: polar-VARIANT ("taller than" ≠ "shorter than") → No equivalent unmarked alternative → No manner implicature → No asymmetry
• Equatives: polar-INVARIANT ("as tall as" = "as short as" semantically) → Unmarked alternative exists → Manner implicature → Asymmetry

File Structure

§1. Polarity, cost, and implicature types §2. Per-construction evaluativity source + derivation §3. Q-implicature for positive constructions (degree tautology) §4. R-implicature / Marked Meaning Principle (MMP) §5. Lexicon-grounded derivation (full pipeline) §6. Rett's core predictions (theorems) §7. Bridge to empirical data (Rett2015.lean)

inductive Rett2015Implicature.Polarity : Type

Polarity of an adjective: positive (unmarked) vs negative (marked).

From [Bie89], [Ken07]:

• Positive-polar (tall, happy, expensive): unmarked, default
• Negative-polar (short, unhappy, cheap): marked, requires more justification

Markedness is reflected in:

• Morphological complexity (happy → un-happy)
• Distributional restrictions ("How tall?" is neutral, "How short?" presupposes)
• Processing cost (marked forms are costlier)

• positive : Polarity
• negative : Polarity

def Rett2015Implicature.instReprPolarity.repr : Polarity → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Rett2015Implicature.instReprPolarity : Repr Polarity

Equations

• Rett2015Implicature.instReprPolarity = { reprPrec := Rett2015Implicature.instReprPolarity.repr }

@[implicit_reducible]

instance Rett2015Implicature.instDecidableEqPolarity : DecidableEq Polarity

Equations

• Rett2015Implicature.instDecidableEqPolarity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Rett2015Implicature.Polarity.IsMarked (p : Polarity) : Prop

Is this polarity marked?

Negative-polar adjectives are marked (require more contextual support).

Equations

• p.IsMarked = (p = Rett2015Implicature.Polarity.negative)

@[implicit_reducible]

instance Rett2015Implicature.instDecidablePredPolarityIsMarked : DecidablePred Polarity.IsMarked

Equations

• Rett2015Implicature.instDecidablePredPolarityIsMarked x✝ = Rett2015Implicature.instDecidablePredPolarityIsMarked._aux_1 x✝

def Rett2015Implicature.Polarity.cost : Polarity → ℚ

Production cost associated with polarity.

Marked forms cost more to produce, licensing manner implicatures. This follows [Hor84]'s Division of Pragmatic Labor.

Equations

• Rett2015Implicature.Polarity.positive.cost = 1
• Rett2015Implicature.Polarity.negative.cost = 2

def Rett2015Implicature.mannerImplicatureApplies : Degree.AdjectivalConstruction → Bool

Does manner implicature apply to this construction?

Manner implicature requires polar INVARIANCE:

• If the two antonyms have the same meaning, using the costlier marked form signals something extra (evaluativity)
• If they have different meanings, no pragmatic competition occurs

Equations

• Rett2015Implicature.mannerImplicatureApplies x✝ = (Implicature.Markedness.polarVariance x✝ == Implicature.Markedness.PolarVariance.invariant)

inductive Rett2015Implicature.EvaluativityImplicature : Type

Types of implicature that can derive evaluativity.

Following [Ret15] Chapter 4-5:

• Quantity (Q): Avoid uninformative utterances → strengthen to evaluative
• Manner (R): Use of costly form signals marked meaning → evaluativity

These correspond to Horn's Q-principle (say enough) and R-principle (don't say more than needed, modulated by form cost).

• quantity : EvaluativityImplicature
• manner : EvaluativityImplicature
• none : EvaluativityImplicature

def Rett2015Implicature.instReprEvaluativityImplicature.repr : EvaluativityImplicature → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Rett2015Implicature.instReprEvaluativityImplicature : Repr EvaluativityImplicature

Equations

• Rett2015Implicature.instReprEvaluativityImplicature = { reprPrec := Rett2015Implicature.instReprEvaluativityImplicature.repr }

@[implicit_reducible]

instance Rett2015Implicature.instDecidableEqEvaluativityImplicature : DecidableEq EvaluativityImplicature

Equations

• Rett2015Implicature.instDecidableEqEvaluativityImplicature x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Rett2015Implicature.evaluativitySource (c : Degree.AdjectivalConstruction) (p : Polarity) : EvaluativityImplicature

Which implicature type derives evaluativity for this construction + polarity?

From [Ret15] Chapter 5:

Construction	Positive-polar	Negative-polar
Positive	Quantity	Quantity
Comparative	None	None
Equative	None	Manner
Degree Question	None	Manner
Measure Phrase	None	N/A (ungramm.)

Key insight: The asymmetry in equatives/questions comes from MANNER implicature, which only applies to marked forms in polar-invariant constructions.

Equations

• Rett2015Implicature.evaluativitySource Degree.AdjectivalConstruction.positive p = Rett2015Implicature.EvaluativityImplicature.quantity
• Rett2015Implicature.evaluativitySource Degree.AdjectivalConstruction.comparative p = Rett2015Implicature.EvaluativityImplicature.none
• Rett2015Implicature.evaluativitySource Degree.AdjectivalConstruction.equative Rett2015Implicature.Polarity.positive = Rett2015Implicature.EvaluativityImplicature.none
• Rett2015Implicature.evaluativitySource Degree.AdjectivalConstruction.equative Rett2015Implicature.Polarity.negative = Rett2015Implicature.EvaluativityImplicature.manner
• Rett2015Implicature.evaluativitySource Degree.AdjectivalConstruction.degreeQuestion Rett2015Implicature.Polarity.positive = Rett2015Implicature.EvaluativityImplicature.none
• Rett2015Implicature.evaluativitySource Degree.AdjectivalConstruction.degreeQuestion Rett2015Implicature.Polarity.negative = Rett2015Implicature.EvaluativityImplicature.manner
• Rett2015Implicature.evaluativitySource Degree.AdjectivalConstruction.measurePhrase p = Rett2015Implicature.EvaluativityImplicature.none

structure Rett2015Implicature.EvaluativityDerivation : Type

Derivation of evaluativity for a construction + polarity combination.

Records:

• Which implicature type applies
• Whether evaluativity is predicted
• The mechanism (Q vs R)

• construction : Degree.AdjectivalConstruction
• polarity : Polarity
• implicatureType : EvaluativityImplicature
• isEvaluative : Bool
• mechanism : String

def Rett2015Implicature.instReprEvaluativityDerivation.repr : EvaluativityDerivation → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Rett2015Implicature.instReprEvaluativityDerivation : Repr EvaluativityDerivation

Equations

• Rett2015Implicature.instReprEvaluativityDerivation = { reprPrec := Rett2015Implicature.instReprEvaluativityDerivation.repr }

def Rett2015Implicature.deriveEvaluativity (c : Degree.AdjectivalConstruction) (p : Polarity) : EvaluativityDerivation

Derive evaluativity for a construction + polarity.

Equations

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

def Rett2015Implicature.positivePolarPredictions : List EvaluativityDerivation

All predictions for positive-polar adjectives.

Equations

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

def Rett2015Implicature.negativePolarPredictions : List EvaluativityDerivation

All predictions for negative-polar adjectives.

Equations

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

def Rett2015Implicature.evaluativityPredictionTable : String

Summary table matching Rett's Table 5.1.

	Positive-polar	Negative-polar
Positive	evaluative (Q)	evaluative (Q)
Comparative	non-eval	non-eval
Equative	non-eval	evaluative (R)
Measure Phrase	non-eval	(ungrammatical)
Degree Question	non-eval	evaluative (R)

Equations

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

theorem Rett2015Implicature.positive_both_evaluative : (deriveEvaluativity Degree.AdjectivalConstruction.positive Polarity.positive).isEvaluative = true ∧ (deriveEvaluativity Degree.AdjectivalConstruction.positive Polarity.negative).isEvaluative = true

Theorem: Positive constructions are evaluative for both polarities

This is derived from Q-implicature (uninformativity avoidance).

theorem Rett2015Implicature.comparative_never_evaluative : (deriveEvaluativity Degree.AdjectivalConstruction.comparative Polarity.positive).isEvaluative = false ∧ (deriveEvaluativity Degree.AdjectivalConstruction.comparative Polarity.negative).isEvaluative = false

Theorem: Comparatives are never evaluative

The comparative morpheme (-er) binds the degree argument, leaving no room for threshold inference.

theorem Rett2015Implicature.equative_asymmetry : (deriveEvaluativity Degree.AdjectivalConstruction.equative Polarity.positive).isEvaluative = false ∧ (deriveEvaluativity Degree.AdjectivalConstruction.equative Polarity.negative).isEvaluative = true

Theorem: Equatives show polarity asymmetry

Positive antonym: not evaluative Negative antonym: evaluative (manner implicature)

theorem Rett2015Implicature.question_asymmetry : (deriveEvaluativity Degree.AdjectivalConstruction.degreeQuestion Polarity.positive).isEvaluative = false ∧ (deriveEvaluativity Degree.AdjectivalConstruction.degreeQuestion Polarity.negative).isEvaluative = true

Theorem: Degree questions show polarity asymmetry

Same pattern as equatives (polar-invariant → manner implicature for marked).

theorem Rett2015Implicature.invariant_shows_asymmetry_equative : (deriveEvaluativity Degree.AdjectivalConstruction.equative Polarity.positive).isEvaluative ≠ (deriveEvaluativity Degree.AdjectivalConstruction.equative Polarity.negative).isEvaluative

Theorem: Polar-invariant constructions show asymmetry

Equatives and degree questions show different evaluativity for positive vs negative polarity.

theorem Rett2015Implicature.invariant_shows_asymmetry_question : (deriveEvaluativity Degree.AdjectivalConstruction.degreeQuestion Polarity.positive).isEvaluative ≠ (deriveEvaluativity Degree.AdjectivalConstruction.degreeQuestion Polarity.negative).isEvaluative

theorem Rett2015Implicature.variant_shows_symmetry_positive : (deriveEvaluativity Degree.AdjectivalConstruction.positive Polarity.positive).isEvaluative = (deriveEvaluativity Degree.AdjectivalConstruction.positive Polarity.negative).isEvaluative

Theorem: Polar-variant constructions show symmetry

Positives and comparatives have the same evaluativity for both polarities.

theorem Rett2015Implicature.variant_shows_symmetry_comparative : (deriveEvaluativity Degree.AdjectivalConstruction.comparative Polarity.positive).isEvaluative = (deriveEvaluativity Degree.AdjectivalConstruction.comparative Polarity.negative).isEvaluative

theorem Rett2015Implicature.manner_requires_marked_and_invariant (c : Degree.AdjectivalConstruction) (p : Polarity) : evaluativitySource c p = EvaluativityImplicature.manner → Implicature.Markedness.polarVariance c = Implicature.Markedness.PolarVariance.invariant ∧ p = Polarity.negative

Theorem: Manner implicature only applies to marked forms in invariant constructions

structure Rett2015Implicature.QImplicatureDerivation : Type

Q-implicature derivation for positive constructions.

Standard Recipe applied to "John is tall":

1. Speaker said "John is tall"
2. Alternative: "John is tall to degree d" (for any d)
3. Without evaluativity, this is true for any d - UNINFORMATIVE
4. Listener strengthens: John's height exceeds contextual standard

This is the same mechanism as scalar implicatures, applied to threshold inference.

• construction : Degree.AdjectivalConstruction
• uninformativeWithout : Bool

  The utterance is uninformative without evaluativity

• informativeWith : Bool

  Evaluativity makes it informative

• evaluativityLicensed : Bool

  Q-implicature licenses evaluativity

@[implicit_reducible]

instance Rett2015Implicature.instReprQImplicatureDerivation : Repr QImplicatureDerivation

Equations

• Rett2015Implicature.instReprQImplicatureDerivation = { reprPrec := Rett2015Implicature.instReprQImplicatureDerivation.repr }

def Rett2015Implicature.instReprQImplicatureDerivation.repr : QImplicatureDerivation → ℕ → Std.Format

Equations

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

def Rett2015Implicature.deriveQImplicature (c : Degree.AdjectivalConstruction) : QImplicatureDerivation

Derive Q-implicature for positive constructions.

Equations

• One or more equations did not get rendered due to their size.
• Rett2015Implicature.deriveQImplicature c = { construction := c, uninformativeWithout := false, informativeWith := false, evaluativityLicensed := false }

structure Rett2015Implicature.RImplicatureDerivation : Type

R-implicature derivation for equatives/questions.

Division of Pragmatic Labor applied to "How short is John?":

1. Speaker used marked form "short" (cost = 2)
2. Unmarked alternative "tall" available (cost = 1)
3. Same truth conditions (polar-invariant)
4. Using costly form must signal something extra
5. That something = evaluativity (presupposes shortness)

• construction : Degree.AdjectivalConstruction
• polarity : Polarity
• unmarkedAlternativeExists : Bool

  Is there an unmarked alternative with same truth conditions?

• formIsMarked : Bool

  Is the current form marked (costly)?

• evaluativityLicensed : Bool

  R-implicature licenses evaluativity

@[implicit_reducible]

instance Rett2015Implicature.instReprRImplicatureDerivation : Repr RImplicatureDerivation

Equations

• Rett2015Implicature.instReprRImplicatureDerivation = { reprPrec := Rett2015Implicature.instReprRImplicatureDerivation.repr }

def Rett2015Implicature.instReprRImplicatureDerivation.repr : RImplicatureDerivation → ℕ → Std.Format

Equations

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

def Rett2015Implicature.deriveRImplicature (c : Degree.AdjectivalConstruction) (p : Polarity) : RImplicatureDerivation

Derive R-implicature for equatives/questions.

Equations

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

structure Rett2015Implicature.MMPDerivation : Type

The Marked Meaning Principle (MMP) derivation record.

From [Ret15] Chapter 5, following [Hor84]:

The MMP states that using a marked form when an unmarked equivalent exists signals that the speaker intends the marked meaning.

For evaluativity: using "as short as" instead of "as tall as" in an equative signals that the speaker presupposes shortness.

• adjForm : String

  The adjective form used

• unmarkedAlternative : Option String

  The unmarked alternative (if any)

• construction : Degree.AdjectivalConstruction

  The construction

• mmpApplies : Bool

  Does MMP apply? (marked form + polar-invariant + alternative exists)

• implicature : Option EvaluativityImplicature

  The resulting evaluativity implicature (if any)

• explanation : String

  Explanation of the derivation

def Rett2015Implicature.instReprMMPDerivation.repr : MMPDerivation → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Rett2015Implicature.instReprMMPDerivation : Repr MMPDerivation

Equations

• Rett2015Implicature.instReprMMPDerivation = { reprPrec := Rett2015Implicature.instReprMMPDerivation.repr }

def Rett2015Implicature.applyMMP (adjForm : String) (construction : Degree.AdjectivalConstruction) (adj1 adj2 : Implicature.Markedness.GradableAdjWithMorphology) : MMPDerivation

Apply the Marked Meaning Principle.

MMP applies when:

1. The form is marked (has higher cost)
2. The construction is polar-invariant (alternatives have same TCs)
3. An unmarked alternative exists

When MMP applies, using the marked form implicates evaluativity.

Equations

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

structure Rett2015Implicature.LexiconGroundedDerivation : Type

Extended evaluativity derivation with lexicon grounding.

This structure records:

1. The adjective and its morphological properties
2. Markedness determination via objective criteria
3. M-alternative generation
4. Q/R implicature derivation
5. Final evaluativity prediction

• adjective : Implicature.Markedness.GradableAdjWithMorphology

  The adjective entry with morphology

• antonym : Implicature.Markedness.GradableAdjWithMorphology

  The antonym entry with morphology

• construction : Degree.AdjectivalConstruction

  The construction

• mAlternatives : Option Implicature.Markedness.MAlternativeSet

  M-alternatives generated (if any)

• mmpDerivation : MMPDerivation

  MMP derivation

• isEvaluative : Bool

  Final evaluativity prediction

• source : EvaluativityImplicature

  Source of evaluativity

@[implicit_reducible]

instance Rett2015Implicature.instReprLexiconGroundedDerivation : Repr LexiconGroundedDerivation

Equations

• Rett2015Implicature.instReprLexiconGroundedDerivation = { reprPrec := Rett2015Implicature.instReprLexiconGroundedDerivation.repr }

def Rett2015Implicature.instReprLexiconGroundedDerivation.repr : LexiconGroundedDerivation → ℕ → Std.Format

Equations

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

def Rett2015Implicature.deriveEvaluativityWithLexicon (adjForm : String) (construction : Degree.AdjectivalConstruction) (adj1 adj2 : Implicature.Markedness.GradableAdjWithMorphology) : LexiconGroundedDerivation

Derive evaluativity with full lexicon grounding.

This is the main entry point for the Neo-Gricean evaluativity derivation. It:

1. Looks up morphological properties of the adjective
2. Computes markedness from objective criteria
3. Generates M-alternatives for polar-invariant constructions
4. Applies Q-implicature (positive) or MMP (equative/question)
5. Returns a fully grounded derivation

Equations

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

structure Rett2015Implicature.DegreeTautologyAnalysis : Type

Degree tautology analysis for positive constructions.

Following [Ret15] Chapter 3:

Without evaluativity, "John is tall" is a degree tautology:

• It asserts that John has SOME degree of height
• This is trivially true for any entity with height

Q-implicature resolves this by strengthening to evaluative reading:

• "John is tall" → John's height exceeds the contextual standard

This explains why positive constructions are evaluative for BOTH polarities.

• construction : Degree.AdjectivalConstruction

  The construction type

• isTautologyWithout : Bool

  Is this a degree tautology without evaluativity?

• qImplicatureResolves : Bool

  Does Q-implicature resolve the tautology?

• explanation : String

  Explanation

def Rett2015Implicature.instReprDegreeTautologyAnalysis.repr : DegreeTautologyAnalysis → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Rett2015Implicature.instReprDegreeTautologyAnalysis : Repr DegreeTautologyAnalysis

Equations

• Rett2015Implicature.instReprDegreeTautologyAnalysis = { reprPrec := Rett2015Implicature.instReprDegreeTautologyAnalysis.repr }

def Rett2015Implicature.analyzeDegreeTautology (c : Degree.AdjectivalConstruction) : DegreeTautologyAnalysis

Analyze degree tautology for a construction.

Equations

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

theorem Rett2015Implicature.mmp_requires_invariance_equative : (applyMMP "short" Degree.AdjectivalConstruction.equative Implicature.Markedness.tall_with_morphology Implicature.Markedness.short_with_morphology).mmpApplies = true → Implicature.Markedness.polarVariance Degree.AdjectivalConstruction.equative = Implicature.Markedness.PolarVariance.invariant

MMP only applies in polar-invariant constructions (equative case).

theorem Rett2015Implicature.mmp_requires_invariance_question : (applyMMP "short" Degree.AdjectivalConstruction.degreeQuestion Implicature.Markedness.tall_with_morphology Implicature.Markedness.short_with_morphology).mmpApplies = true → Implicature.Markedness.polarVariance Degree.AdjectivalConstruction.degreeQuestion = Implicature.Markedness.PolarVariance.invariant

MMP only applies in polar-invariant constructions (question case).

theorem Rett2015Implicature.mmp_not_in_comparative : (applyMMP "short" Degree.AdjectivalConstruction.comparative Implicature.Markedness.tall_with_morphology Implicature.Markedness.short_with_morphology).mmpApplies = false

MMP does not apply in comparative constructions.

theorem Rett2015Implicature.mmp_applies_short_equative : (applyMMP "short" Degree.AdjectivalConstruction.equative Implicature.Markedness.tall_with_morphology Implicature.Markedness.short_with_morphology).mmpApplies = true

MMP applies for "short" in equative constructions.

theorem Rett2015Implicature.mmp_not_for_tall_equative : (applyMMP "tall" Degree.AdjectivalConstruction.equative Implicature.Markedness.tall_with_morphology Implicature.Markedness.short_with_morphology).mmpApplies = false

MMP does not apply for "tall" in equative constructions (not marked).

theorem Rett2015Implicature.equative_asymmetry_from_mmp : Implicature.Markedness.isMarkedForm "short" Implicature.Markedness.tall_with_morphology Implicature.Markedness.short_with_morphology = true ∧ Implicature.Markedness.polarVariance Degree.AdjectivalConstruction.equative = Implicature.Markedness.PolarVariance.invariant → (applyMMP "short" Degree.AdjectivalConstruction.equative Implicature.Markedness.tall_with_morphology Implicature.Markedness.short_with_morphology).implicature = some EvaluativityImplicature.manner ∧ (applyMMP "tall" Degree.AdjectivalConstruction.equative Implicature.Markedness.tall_with_morphology Implicature.Markedness.short_with_morphology).implicature = none

Equative asymmetry emerges from MMP + markedness.

theorem Rett2015Implicature.grounded_matches_simple_tall_positive : (deriveEvaluativityWithLexicon "tall" Degree.AdjectivalConstruction.positive Implicature.Markedness.tall_with_morphology Implicature.Markedness.short_with_morphology).isEvaluative = (deriveEvaluativity Degree.AdjectivalConstruction.positive Polarity.positive).isEvaluative

Lexicon-grounded derivation matches simple derivation for tall.

theorem Rett2015Implicature.grounded_matches_simple_short_equative : (deriveEvaluativityWithLexicon "short" Degree.AdjectivalConstruction.equative Implicature.Markedness.tall_with_morphology Implicature.Markedness.short_with_morphology).isEvaluative = (deriveEvaluativity Degree.AdjectivalConstruction.equative Polarity.negative).isEvaluative

Lexicon-grounded derivation matches simple derivation for short in equative.

These theorems formalize the key empirical predictions from Rett's account:

1. Evaluativity distribution: Which constructions are evaluative?
2. Asymmetry pattern: When do we see polarity asymmetry?
3. Mechanism attribution: Q-implicature vs MMP?
4. Morphological grounding: How does markedness determine asymmetry?

theorem Rett2015Implicature.rett_positive_evaluative : (deriveEvaluativity Degree.AdjectivalConstruction.positive Polarity.positive).isEvaluative = true ∧ (deriveEvaluativity Degree.AdjectivalConstruction.positive Polarity.negative).isEvaluative = true ∧ (deriveEvaluativity Degree.AdjectivalConstruction.positive Polarity.positive).implicatureType = EvaluativityImplicature.quantity ∧ (deriveEvaluativity Degree.AdjectivalConstruction.positive Polarity.negative).implicatureType = EvaluativityImplicature.quantity

Rett Prediction 1: Positive constructions require evaluativity.

"John is tall" asserts that John's height exceeds a contextual standard. This is derived from Q-implicature: without evaluativity, the utterance would be uninformative (a "degree tautology").

theorem Rett2015Implicature.rett_comparative_non_evaluative : (deriveEvaluativity Degree.AdjectivalConstruction.comparative Polarity.positive).isEvaluative = false ∧ (deriveEvaluativity Degree.AdjectivalConstruction.comparative Polarity.negative).isEvaluative = false ∧ (deriveEvaluativity Degree.AdjectivalConstruction.comparative Polarity.positive).implicatureType = EvaluativityImplicature.none ∧ (deriveEvaluativity Degree.AdjectivalConstruction.comparative Polarity.negative).implicatureType = EvaluativityImplicature.none

Rett Prediction 2: Comparatives never require evaluativity.

"John is taller than Mary" is true even if both are short. The comparative morpheme (-er) binds the degree argument, leaving no threshold to be inferred.

theorem Rett2015Implicature.rett_equative_asymmetry : (deriveEvaluativity Degree.AdjectivalConstruction.equative Polarity.positive).isEvaluative = false ∧ (deriveEvaluativity Degree.AdjectivalConstruction.equative Polarity.negative).isEvaluative = true ∧ (deriveEvaluativity Degree.AdjectivalConstruction.equative Polarity.positive).implicatureType = EvaluativityImplicature.none ∧ (deriveEvaluativity Degree.AdjectivalConstruction.equative Polarity.negative).implicatureType = EvaluativityImplicature.manner

Rett Prediction 3: Equatives show polarity asymmetry.

"John is as tall as Mary" — no evaluativity (unmarked form) "John is as short as Mary" — evaluative (marked form triggers MMP)

The asymmetry arises from the Marked Meaning Principle.

theorem Rett2015Implicature.rett_question_asymmetry : (deriveEvaluativity Degree.AdjectivalConstruction.degreeQuestion Polarity.positive).isEvaluative = false ∧ (deriveEvaluativity Degree.AdjectivalConstruction.degreeQuestion Polarity.negative).isEvaluative = true ∧ (deriveEvaluativity Degree.AdjectivalConstruction.degreeQuestion Polarity.positive).implicatureType = EvaluativityImplicature.none ∧ (deriveEvaluativity Degree.AdjectivalConstruction.degreeQuestion Polarity.negative).implicatureType = EvaluativityImplicature.manner

Rett Prediction 4: Degree questions show polarity asymmetry.

"How tall is John?" — neutral question (unmarked form) "How short is John?" — presupposes shortness (marked form triggers MMP)

Same pattern as equatives: polar-invariant → MMP for marked forms.

theorem Rett2015Implicature.asymmetry_requires_polar_invariance : (Implicature.Markedness.polarVariance Degree.AdjectivalConstruction.equative = Implicature.Markedness.PolarVariance.invariant ∧ (deriveEvaluativity Degree.AdjectivalConstruction.equative Polarity.positive).isEvaluative ≠ (deriveEvaluativity Degree.AdjectivalConstruction.equative Polarity.negative).isEvaluative) ∧ (Implicature.Markedness.polarVariance Degree.AdjectivalConstruction.degreeQuestion = Implicature.Markedness.PolarVariance.invariant ∧ (deriveEvaluativity Degree.AdjectivalConstruction.degreeQuestion Polarity.positive).isEvaluative ≠ (deriveEvaluativity Degree.AdjectivalConstruction.degreeQuestion Polarity.negative).isEvaluative) ∧ Implicature.Markedness.polarVariance Degree.AdjectivalConstruction.comparative = Implicature.Markedness.PolarVariance.variant ∧ (deriveEvaluativity Degree.AdjectivalConstruction.comparative Polarity.positive).isEvaluative = (deriveEvaluativity Degree.AdjectivalConstruction.comparative Polarity.negative).isEvaluative

Core Insight: Asymmetry requires polar invariance.

Constructions where antonyms have the SAME truth conditions (polar-invariant) show asymmetry. Constructions where antonyms differ (polar-variant) don't.

This is because MMP only applies when an unmarked alternative EXISTS with the same meaning.

theorem Rett2015Implicature.polar_invariance_enables_m_alternatives : Implicature.Markedness.polarVariance Degree.AdjectivalConstruction.equative = Implicature.Markedness.PolarVariance.invariant ∧ Implicature.Markedness.polarVariance Degree.AdjectivalConstruction.degreeQuestion = Implicature.Markedness.PolarVariance.invariant ∧ Implicature.Markedness.polarVariance Degree.AdjectivalConstruction.comparative = Implicature.Markedness.PolarVariance.variant ∧ Implicature.Markedness.polarVariance Degree.AdjectivalConstruction.positive = Implicature.Markedness.PolarVariance.variant

Polar invariance is the key to M-alternative availability.

theorem Rett2015Implicature.q_implicature_for_positive : evaluativitySource Degree.AdjectivalConstruction.positive Polarity.positive = EvaluativityImplicature.quantity ∧ evaluativitySource Degree.AdjectivalConstruction.positive Polarity.negative = EvaluativityImplicature.quantity

Q-implicature mechanism: Positive constructions use Quantity.

Q-implicature resolves the "degree tautology" of positive constructions. Without evaluativity, "John is tall" is trivially true for anyone with height.

theorem Rett2015Implicature.mmp_for_marked_in_invariant : evaluativitySource Degree.AdjectivalConstruction.equative Polarity.negative = EvaluativityImplicature.manner ∧ evaluativitySource Degree.AdjectivalConstruction.degreeQuestion Polarity.negative = EvaluativityImplicature.manner ∧ evaluativitySource Degree.AdjectivalConstruction.equative Polarity.positive = EvaluativityImplicature.none ∧ evaluativitySource Degree.AdjectivalConstruction.degreeQuestion Polarity.positive = EvaluativityImplicature.none

MMP mechanism: Equatives and questions use Manner for marked forms.

The Marked Meaning Principle (MMP) derives evaluativity from using a marked form when an unmarked equivalent exists.

theorem Rett2015Implicature.no_mechanism_for_comparative : evaluativitySource Degree.AdjectivalConstruction.comparative Polarity.positive = EvaluativityImplicature.none ∧ evaluativitySource Degree.AdjectivalConstruction.comparative Polarity.negative = EvaluativityImplicature.none

No mechanism for comparatives: They're never evaluative.

theorem Rett2015Implicature.marked_triggers_mmp : Implicature.Markedness.isMarkedForm "short" Implicature.Markedness.tall_with_morphology Implicature.Markedness.short_with_morphology = true ∧ Implicature.Markedness.isMarkedForm "tall" Implicature.Markedness.tall_with_morphology Implicature.Markedness.short_with_morphology = false ∧ (applyMMP "short" Degree.AdjectivalConstruction.equative Implicature.Markedness.tall_with_morphology Implicature.Markedness.short_with_morphology).mmpApplies = true ∧ (applyMMP "tall" Degree.AdjectivalConstruction.equative Implicature.Markedness.tall_with_morphology Implicature.Markedness.short_with_morphology).mmpApplies = false

Markedness determines asymmetry direction.

The marked form (higher cost) triggers MMP, not the unmarked form.

theorem Rett2015Implicature.marked_costs_more : Implicature.Markedness.productionCost "short" Implicature.Markedness.tall_with_morphology Implicature.Markedness.short_with_morphology > Implicature.Markedness.productionCost "tall" Implicature.Markedness.tall_with_morphology Implicature.Markedness.short_with_morphology

Cost differential: Marked forms cost more to produce.

theorem Rett2015Implicature.morphological_markedness : Implicature.Markedness.isMarkedForm "unhappy" Implicature.Markedness.happy_with_morphology Implicature.Markedness.unhappy_with_morphology = true ∧ Implicature.Markedness.isMarkedForm "happy" Implicature.Markedness.happy_with_morphology Implicature.Markedness.unhappy_with_morphology = false

Morphological complexity determines markedness for happy/unhappy.

theorem Rett2015Implicature.complete_derivation_as_short_as : Implicature.Markedness.short_with_morphology.isPositivePole = false ∧ Implicature.Markedness.isMarkedForm "short" Implicature.Markedness.tall_with_morphology Implicature.Markedness.short_with_morphology = true ∧ Implicature.Markedness.polarVariance Degree.AdjectivalConstruction.equative = Implicature.Markedness.PolarVariance.invariant ∧ (applyMMP "short" Degree.AdjectivalConstruction.equative Implicature.Markedness.tall_with_morphology Implicature.Markedness.short_with_morphology).mmpApplies = true ∧ (applyMMP "short" Degree.AdjectivalConstruction.equative Implicature.Markedness.tall_with_morphology Implicature.Markedness.short_with_morphology).implicature = some EvaluativityImplicature.manner ∧ (deriveEvaluativityWithLexicon "short" Degree.AdjectivalConstruction.equative Implicature.Markedness.tall_with_morphology Implicature.Markedness.short_with_morphology).isEvaluative = true

Complete derivation for "as short as": From morphology to evaluativity.

This theorem traces the full derivation:

1. "short" has negative pole → marked by scale direction
2. Equative is polar-invariant → M-alternatives exist
3. Using marked "short" when unmarked "tall" exists → MMP applies
4. MMP → manner implicature → evaluativity

theorem Rett2015Implicature.complete_derivation_as_tall_as : Implicature.Markedness.tall_with_morphology.isPositivePole = true ∧ Implicature.Markedness.isMarkedForm "tall" Implicature.Markedness.tall_with_morphology Implicature.Markedness.short_with_morphology = false ∧ Implicature.Markedness.polarVariance Degree.AdjectivalConstruction.equative = Implicature.Markedness.PolarVariance.invariant ∧ (applyMMP "tall" Degree.AdjectivalConstruction.equative Implicature.Markedness.tall_with_morphology Implicature.Markedness.short_with_morphology).mmpApplies = false ∧ (applyMMP "tall" Degree.AdjectivalConstruction.equative Implicature.Markedness.tall_with_morphology Implicature.Markedness.short_with_morphology).implicature = none ∧ (deriveEvaluativityWithLexicon "tall" Degree.AdjectivalConstruction.equative Implicature.Markedness.tall_with_morphology Implicature.Markedness.short_with_morphology).isEvaluative = false

Complete derivation for "as tall as": No evaluativity for unmarked.

1. "tall" has positive pole → unmarked
2. Equative is polar-invariant → M-alternatives exist, but...
3. "tall" is the unmarked form → MMP doesn't apply
4. No implicature → no evaluativity

def Rett2015Implicature.predictedStatus (d : EvaluativityDerivation) : Rett2015.Evaluativity.EvaluativityStatus

Convert this study's derivation prediction to the empirical data format.

Equations

• Rett2015Implicature.predictedStatus d = if d.isEvaluative = true then Rett2015.Evaluativity.EvaluativityStatus.evaluative else Rett2015.Evaluativity.EvaluativityStatus.nonEvaluative

def Rett2015Implicature.predictionMatches (d : EvaluativityDerivation) (datum : Rett2015.Evaluativity.EvaluativityDatum) : Bool

Check if prediction matches an empirical datum.

Equations

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

theorem Rett2015Implicature.matches_positive_tall : predictionMatches (deriveEvaluativity Degree.AdjectivalConstruction.positive Polarity.positive) Rett2015.Evaluativity.positive_tall = true

Theorem: Predictions match positive_tall datum

theorem Rett2015Implicature.matches_comparative_tall : predictionMatches (deriveEvaluativity Degree.AdjectivalConstruction.comparative Polarity.positive) Rett2015.Evaluativity.comparative_tall = true

Theorem: Predictions match comparative_tall datum

theorem Rett2015Implicature.matches_equative_tall : predictionMatches (deriveEvaluativity Degree.AdjectivalConstruction.equative Polarity.positive) Rett2015.Evaluativity.equative_tall = true

Theorem: Predictions match equative_tall datum

theorem Rett2015Implicature.matches_equative_short : predictionMatches (deriveEvaluativity Degree.AdjectivalConstruction.equative Polarity.negative) Rett2015.Evaluativity.equative_short = true

Theorem: Predictions match equative_short datum

theorem Rett2015Implicature.matches_question_tall : predictionMatches (deriveEvaluativity Degree.AdjectivalConstruction.degreeQuestion Polarity.positive) Rett2015.Evaluativity.question_tall = true

Theorem: Predictions match question_tall datum

theorem Rett2015Implicature.matches_question_short : predictionMatches (deriveEvaluativity Degree.AdjectivalConstruction.degreeQuestion Polarity.negative) Rett2015.Evaluativity.question_short = true

Theorem: Predictions match question_short datum