Linglib.Theories.Pragmatics.NeoGricean.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

NeoGricean.Evaluativity.mannerImplicatureApplies x✝ = (NeoGricean.Evaluativity.polarVariance x✝ == NeoGricean.Evaluativity.PolarVariance.invariant)

Instances For

source

inductive NeoGricean.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

instance NeoGricean.Evaluativity.instReprEvaluativityImplicature :

Repr EvaluativityImplicature

Equations

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

source

def NeoGricean.Evaluativity.instReprEvaluativityImplicature.repr :

EvaluativityImplicature → ℕ → Std.Format

Equations

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

Instances For

source

instance NeoGricean.Evaluativity.instDecidableEqEvaluativityImplicature :

DecidableEq EvaluativityImplicature

Equations

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

source

instance NeoGricean.Evaluativity.instBEqEvaluativityImplicature :

BEq EvaluativityImplicature

Equations

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

source

def NeoGricean.Evaluativity.instBEqEvaluativityImplicature.beq :

EvaluativityImplicature → EvaluativityImplicature → Bool

Equations

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

Instances For

source

def NeoGricean.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 NeoGricean.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 NeoGricean.Evaluativity.instReprEvaluativityDerivation.repr :

EvaluativityDerivation → ℕ → Std.Format

Equations

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

Instances For

source

instance NeoGricean.Evaluativity.instReprEvaluativityDerivation :

Repr EvaluativityDerivation

Equations

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

source

def NeoGricean.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 NeoGricean.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 NeoGricean.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 NeoGricean.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 NeoGricean.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 NeoGricean.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 NeoGricean.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 NeoGricean.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 NeoGricean.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 NeoGricean.Evaluativity.invariant_shows_asymmetry_question :

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

source

theorem NeoGricean.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 NeoGricean.Evaluativity.variant_shows_symmetry_comparative :

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

source

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

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

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

source

structure NeoGricean.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

def NeoGricean.Evaluativity.instReprQImplicatureDerivation.repr :

QImplicatureDerivation → ℕ → Std.Format

Equations

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

Instances For

source

instance NeoGricean.Evaluativity.instReprQImplicatureDerivation :

Repr QImplicatureDerivation

Equations

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

source

def NeoGricean.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.
NeoGricean.Evaluativity.deriveQImplicature c = { construction := c, uninformativeWithout := false, informativeWith := false, evaluativityLicensed := false }

Instances For

source

structure NeoGricean.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

def NeoGricean.Evaluativity.instReprRImplicatureDerivation.repr :

RImplicatureDerivation → ℕ → Std.Format

Equations

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

Instances For

source

instance NeoGricean.Evaluativity.instReprRImplicatureDerivation :

Repr RImplicatureDerivation

Equations

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

source

def NeoGricean.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 NeoGricean.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 NeoGricean.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

instance NeoGricean.Evaluativity.instReprMMPDerivation :

Repr MMPDerivation

Equations

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

source

def NeoGricean.Evaluativity.instReprMMPDerivation.repr :

MMPDerivation → ℕ → Std.Format

Equations

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

Instances For

source

def NeoGricean.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 NeoGricean.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 Alternatives.MAlternativeSet
M-alternatives generated (if any)
mmpDerivation : MMPDerivation
MMP derivation
isEvaluative : Bool
Final evaluativity prediction
source : EvaluativityImplicature
Source of evaluativity

Instances For

source

instance NeoGricean.Evaluativity.instReprLexiconGroundedDerivation :

Repr LexiconGroundedDerivation

Equations

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

source

def NeoGricean.Evaluativity.instReprLexiconGroundedDerivation.repr :

LexiconGroundedDerivation → ℕ → Std.Format

Equations

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

Instances For

source

def NeoGricean.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 NeoGricean.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 NeoGricean.Evaluativity.instReprDegreeTautologyAnalysis.repr :

DegreeTautologyAnalysis → ℕ → Std.Format

Equations

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

Instances For

source

instance NeoGricean.Evaluativity.instReprDegreeTautologyAnalysis :

Repr DegreeTautologyAnalysis

Equations

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

source

def NeoGricean.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 NeoGricean.Evaluativity.mmp_requires_invariance_equative :

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

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

source

theorem NeoGricean.Evaluativity.mmp_requires_invariance_question :

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

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

source

theorem NeoGricean.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 NeoGricean.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 NeoGricean.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 NeoGricean.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 NeoGricean.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 NeoGricean.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 NeoGricean.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