Linglib.Theories.Pragmatics.Implicature.Evaluativity

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

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

Instances For

source

inductive Implicature.Evaluativity.EvaluativityImplicature :

Type

Types of implicature that can derive evaluativity.

Following @cite{rett-2015} 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).

Instances For

source

def Implicature.Evaluativity.instReprEvaluativityImplicature.repr :

EvaluativityImplicature → ℕ → Std.Format

Equations

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

Instances For

source

instance Implicature.Evaluativity.instReprEvaluativityImplicature :

Repr EvaluativityImplicature

Equations

Implicature.Evaluativity.instReprEvaluativityImplicature = { reprPrec := Implicature.Evaluativity.instReprEvaluativityImplicature.repr }

source

instance Implicature.Evaluativity.instDecidableEqEvaluativityImplicature :

DecidableEq EvaluativityImplicature

Equations

Implicature.Evaluativity.instDecidableEqEvaluativityImplicature x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

instance Implicature.Evaluativity.instBEqEvaluativityImplicature :

BEq EvaluativityImplicature

Equations

Implicature.Evaluativity.instBEqEvaluativityImplicature = { beq := Implicature.Evaluativity.instBEqEvaluativityImplicature.beq }

source

def Implicature.Evaluativity.instBEqEvaluativityImplicature.beq :

EvaluativityImplicature → EvaluativityImplicature → Bool

Equations

Implicature.Evaluativity.instBEqEvaluativityImplicature.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

source

def Implicature.Evaluativity.evaluativitySource (c : Semantics.Degree.AdjectivalConstruction) (p : Polarity) :

EvaluativityImplicature

Which implicature type derives evaluativity for this construction + polarity?

From @cite{rett-2015} 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

Instances For

source

structure Implicature.Evaluativity.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 : Semantics.Degree.AdjectivalConstruction
polarity : Polarity
implicatureType : EvaluativityImplicature
isEvaluative : Bool
mechanism : String

Instances For

source

def Implicature.Evaluativity.instReprEvaluativityDerivation.repr :

EvaluativityDerivation → ℕ → Std.Format

Equations

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

Instances For

source

instance Implicature.Evaluativity.instReprEvaluativityDerivation :

Repr EvaluativityDerivation

Equations

Implicature.Evaluativity.instReprEvaluativityDerivation = { reprPrec := Implicature.Evaluativity.instReprEvaluativityDerivation.repr }

source

def Implicature.Evaluativity.deriveEvaluativity (c : Semantics.Degree.AdjectivalConstruction) (p : Polarity) :

EvaluativityDerivation

Derive evaluativity for a construction + polarity.

Equations

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

Instances For

source

def Implicature.Evaluativity.positivePolarPredictions :

List EvaluativityDerivation

All predictions for positive-polar adjectives.

Equations

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

Instances For

source

def Implicature.Evaluativity.negativePolarPredictions :

List EvaluativityDerivation

All predictions for negative-polar adjectives.

Equations

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

Instances For

source

def Implicature.Evaluativity.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.

Instances For

source

theorem Implicature.Evaluativity.positive_both_evaluative :

(deriveEvaluativity Semantics.Degree.AdjectivalConstruction.positive Polarity.positive).isEvaluative = true ∧ (deriveEvaluativity Semantics.Degree.AdjectivalConstruction.positive Polarity.negative).isEvaluative = true

Theorem: Positive constructions are evaluative for both polarities

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

source

theorem Implicature.Evaluativity.comparative_never_evaluative :

(deriveEvaluativity Semantics.Degree.AdjectivalConstruction.comparative Polarity.positive).isEvaluative = false ∧ (deriveEvaluativity Semantics.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.

source

theorem Implicature.Evaluativity.equative_asymmetry :

(deriveEvaluativity Semantics.Degree.AdjectivalConstruction.equative Polarity.positive).isEvaluative = false ∧ (deriveEvaluativity Semantics.Degree.AdjectivalConstruction.equative Polarity.negative).isEvaluative = true

Theorem: Equatives show polarity asymmetry

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

source

theorem Implicature.Evaluativity.question_asymmetry :

(deriveEvaluativity Semantics.Degree.AdjectivalConstruction.degreeQuestion Polarity.positive).isEvaluative = false ∧ (deriveEvaluativity Semantics.Degree.AdjectivalConstruction.degreeQuestion Polarity.negative).isEvaluative = true

Theorem: Degree questions show polarity asymmetry

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

source

theorem Implicature.Evaluativity.invariant_shows_asymmetry_equative :

(deriveEvaluativity Semantics.Degree.AdjectivalConstruction.equative Polarity.positive).isEvaluative ≠ (deriveEvaluativity Semantics.Degree.AdjectivalConstruction.equative Polarity.negative).isEvaluative

Theorem: Polar-invariant constructions show asymmetry

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

source

theorem Implicature.Evaluativity.invariant_shows_asymmetry_question :

(deriveEvaluativity Semantics.Degree.AdjectivalConstruction.degreeQuestion Polarity.positive).isEvaluative ≠ (deriveEvaluativity Semantics.Degree.AdjectivalConstruction.degreeQuestion Polarity.negative).isEvaluative

source

theorem Implicature.Evaluativity.variant_shows_symmetry_positive :

(deriveEvaluativity Semantics.Degree.AdjectivalConstruction.positive Polarity.positive).isEvaluative = (deriveEvaluativity Semantics.Degree.AdjectivalConstruction.positive Polarity.negative).isEvaluative

Theorem: Polar-variant constructions show symmetry

Positives and comparatives have the same evaluativity for both polarities.

source

theorem Implicature.Evaluativity.variant_shows_symmetry_comparative :

(deriveEvaluativity Semantics.Degree.AdjectivalConstruction.comparative Polarity.positive).isEvaluative = (deriveEvaluativity Semantics.Degree.AdjectivalConstruction.comparative Polarity.negative).isEvaluative

source

theorem Implicature.Evaluativity.manner_requires_marked_and_invariant (c : Semantics.Degree.AdjectivalConstruction) (p : Polarity) :

evaluativitySource c p = EvaluativityImplicature.manner → Markedness.polarVariance c = Markedness.PolarVariance.invariant ∧ p = Polarity.negative

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

source

structure Implicature.Evaluativity.QImplicatureDerivation :

Type

Q-implicature derivation for positive constructions.

Standard Recipe applied to "John is tall":

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

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

construction : Semantics.Degree.AdjectivalConstruction
uninformativeWithout : Bool
The utterance is uninformative without evaluativity
informativeWith : Bool
Evaluativity makes it informative
evaluativityLicensed : Bool
Q-implicature licenses evaluativity

Instances For

source

instance Implicature.Evaluativity.instReprQImplicatureDerivation :

Repr QImplicatureDerivation

Equations

Implicature.Evaluativity.instReprQImplicatureDerivation = { reprPrec := Implicature.Evaluativity.instReprQImplicatureDerivation.repr }

source

def Implicature.Evaluativity.instReprQImplicatureDerivation.repr :

QImplicatureDerivation → ℕ → Std.Format

Equations

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

Instances For

source

def Implicature.Evaluativity.deriveQImplicature (c : Semantics.Degree.AdjectivalConstruction) :

QImplicatureDerivation

Derive Q-implicature for positive constructions.

Equations

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

Instances For

source

structure Implicature.Evaluativity.RImplicatureDerivation :

Type

R-implicature derivation for equatives/questions.

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

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

construction : Semantics.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

Instances For

source

instance Implicature.Evaluativity.instReprRImplicatureDerivation :

Repr RImplicatureDerivation

Equations

Implicature.Evaluativity.instReprRImplicatureDerivation = { reprPrec := Implicature.Evaluativity.instReprRImplicatureDerivation.repr }

source

def Implicature.Evaluativity.instReprRImplicatureDerivation.repr :

RImplicatureDerivation → ℕ → Std.Format

Equations

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

Instances For

source

def Implicature.Evaluativity.deriveRImplicature (c : Semantics.Degree.AdjectivalConstruction) (p : Polarity) :

RImplicatureDerivation

Derive R-implicature for equatives/questions.

Equations

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

Instances For

source

def Implicature.Evaluativity.rsaComparison :

String

How this Neo-Gricean account relates to RSA.

Both derive evaluativity pragmatically, but via different mechanisms:

Neo-Gricean (this module):

Q-implicature: scalar reasoning about informativity
R-implicature: cost-based manner reasoning

RSA:

Joint inference over degree and threshold
Listener models speaker's utility-maximizing behavior
Cost can be built into speaker utility

Key difference: RSA derives thresholds via joint inference, while Neo-Gricean stipulates the mechanism (Q vs R).

The predictions are largely the same, but:

RSA makes graded predictions (probability distributions)
Neo-Gricean makes categorical predictions (evaluative or not)

Equations

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

Instances For

source

structure Implicature.Evaluativity.MMPDerivation :

Type

The Marked Meaning Principle (MMP) derivation record.

From @cite{rett-2015} Chapter 5, following @cite{horn-1984}:

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 : Semantics.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

Instances For

source

def Implicature.Evaluativity.instReprMMPDerivation.repr :

MMPDerivation → ℕ → Std.Format

Equations

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

Instances For

source

instance Implicature.Evaluativity.instReprMMPDerivation :

Repr MMPDerivation

Equations

Implicature.Evaluativity.instReprMMPDerivation = { reprPrec := Implicature.Evaluativity.instReprMMPDerivation.repr }

source

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

MMPDerivation

Apply the Marked Meaning Principle.

MMP applies when:

The form is marked (has higher cost)
The construction is polar-invariant (alternatives have same TCs)
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.

Instances For

source

structure Implicature.Evaluativity.LexiconGroundedDerivation :

Type

Extended evaluativity derivation with lexicon grounding.

This structure records:

The adjective and its morphological properties
Markedness determination via objective criteria
M-alternative generation
Q/R implicature derivation
Final evaluativity prediction

adjective : Markedness.GradableAdjWithMorphology
The adjective entry with morphology
antonym : Markedness.GradableAdjWithMorphology
The antonym entry with morphology
construction : Semantics.Degree.AdjectivalConstruction
The construction
mAlternatives : Option Markedness.MAlternativeSet
M-alternatives generated (if any)
mmpDerivation : MMPDerivation
MMP derivation
isEvaluative : Bool
Final evaluativity prediction
source : EvaluativityImplicature
Source of evaluativity

Instances For

source

instance Implicature.Evaluativity.instReprLexiconGroundedDerivation :

Repr LexiconGroundedDerivation

Equations

Implicature.Evaluativity.instReprLexiconGroundedDerivation = { reprPrec := Implicature.Evaluativity.instReprLexiconGroundedDerivation.repr }

source

def Implicature.Evaluativity.instReprLexiconGroundedDerivation.repr :

LexiconGroundedDerivation → ℕ → Std.Format

Equations

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

Instances For

source

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

LexiconGroundedDerivation

Derive evaluativity with full lexicon grounding.

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

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

Equations

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

Instances For

source

structure Implicature.Evaluativity.DegreeTautologyAnalysis :

Type

Degree tautology analysis for positive constructions.

Following @cite{rett-2015} 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 : Semantics.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

Instances For

source

def Implicature.Evaluativity.instReprDegreeTautologyAnalysis.repr :

DegreeTautologyAnalysis → ℕ → Std.Format

Equations

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

Instances For

source

instance Implicature.Evaluativity.instReprDegreeTautologyAnalysis :

Repr DegreeTautologyAnalysis

Equations

Implicature.Evaluativity.instReprDegreeTautologyAnalysis = { reprPrec := Implicature.Evaluativity.instReprDegreeTautologyAnalysis.repr }

source

def Implicature.Evaluativity.analyzeDegreeTautology (c : Semantics.Degree.AdjectivalConstruction) :

DegreeTautologyAnalysis

Analyze degree tautology for a construction.

Equations

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

Instances For

source

theorem Implicature.Evaluativity.mmp_requires_invariance_equative :

(applyMMP "short" Semantics.Degree.AdjectivalConstruction.equative Markedness.tall_with_morphology Markedness.short_with_morphology).mmpApplies = true → Markedness.polarVariance Semantics.Degree.AdjectivalConstruction.equative = Markedness.PolarVariance.invariant

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

source

theorem Implicature.Evaluativity.mmp_requires_invariance_question :

(applyMMP "short" Semantics.Degree.AdjectivalConstruction.degreeQuestion Markedness.tall_with_morphology Markedness.short_with_morphology).mmpApplies = true → Markedness.polarVariance Semantics.Degree.AdjectivalConstruction.degreeQuestion = Markedness.PolarVariance.invariant

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

source

theorem Implicature.Evaluativity.mmp_not_in_comparative :

(applyMMP "short" Semantics.Degree.AdjectivalConstruction.comparative Markedness.tall_with_morphology Markedness.short_with_morphology).mmpApplies = false

MMP does not apply in comparative constructions.

source

theorem Implicature.Evaluativity.mmp_applies_short_equative :

(applyMMP "short" Semantics.Degree.AdjectivalConstruction.equative Markedness.tall_with_morphology Markedness.short_with_morphology).mmpApplies = true

MMP applies for "short" in equative constructions.

source

theorem Implicature.Evaluativity.mmp_not_for_tall_equative :

(applyMMP "tall" Semantics.Degree.AdjectivalConstruction.equative Markedness.tall_with_morphology Markedness.short_with_morphology).mmpApplies = false

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

source

theorem Implicature.Evaluativity.grounded_matches_simple_tall_positive :

(deriveEvaluativityWithLexicon "tall" Semantics.Degree.AdjectivalConstruction.positive Markedness.tall_with_morphology Markedness.short_with_morphology).isEvaluative = (deriveEvaluativity Semantics.Degree.AdjectivalConstruction.positive Polarity.positive).isEvaluative

Lexicon-grounded derivation matches simple derivation for tall.

source

theorem Implicature.Evaluativity.grounded_matches_simple_short_equative :

(deriveEvaluativityWithLexicon "short" Semantics.Degree.AdjectivalConstruction.equative Markedness.tall_with_morphology Markedness.short_with_morphology).isEvaluative = (deriveEvaluativity Semantics.Degree.AdjectivalConstruction.equative Polarity.negative).isEvaluative

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

source

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").

source

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.

source

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.

source

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.

source

theorem Implicature.Evaluativity.asymmetry_requires_polar_invariance :

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.

source

theorem Implicature.Evaluativity.q_implicature_for_positive :

evaluativitySource Semantics.Degree.AdjectivalConstruction.positive Polarity.positive = EvaluativityImplicature.quantity ∧ evaluativitySource Semantics.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.

source