Gricean Maxims of Conversation

@cite{grice-1975}

Logic and Conversation. In P. Cole & J.L. Morgan (eds.), Syntax and Semantics 3: Speech Acts, 41–58. Academic Press.

Design

The Cooperative Principle and four maxims are formalized as types, not as behavioral predictions. Behavioral predictions (e.g., "speakers maximize informativity") belong in the implementing frameworks — RSA formalizes Quantity via s1Score, NeoGricean via the Standard Recipe, Dale & Reiter via incremental attribute selection. Study files that test the maxims directly (e.g., @cite{engelhardt-etal-2006}) import this module.

Linking theorems connecting maxims to specific frameworks belong in Comparisons/.

The Quantity Maxim

Grice's Quantity maxim has two sub-maxims:

1. Q1: "Make your contribution as informative as is required (for the current purposes of the exchange)."
2. Q2: "Do not make your contribution more informative than is required."

@cite{engelhardt-etal-2006} showed these behave asymmetrically: Q1 violations (under-description) are penalized in both production and explicit judgment; Q2 violations (over-description) are produced frequently, tolerated explicitly, but detected implicitly via processing costs.

inductive Pragmatics.GriceanMaxims.Maxim : Type

The four Gricean maxims of conversation.

• quantity : Maxim

  Make your contribution as informative as is required; do not make it more informative than is required.

• quality : Maxim

  Do not say what you believe to be false; do not say that for which you lack adequate evidence.

• relation : Maxim

  Be relevant.

• manner : Maxim

  Avoid obscurity of expression; avoid ambiguity; be brief; be orderly.

@[implicit_reducible]

instance Pragmatics.GriceanMaxims.instDecidableEqMaxim : DecidableEq Maxim

Equations

• Pragmatics.GriceanMaxims.instDecidableEqMaxim x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Pragmatics.GriceanMaxims.instReprMaxim.repr : Maxim → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Pragmatics.GriceanMaxims.instReprMaxim : Repr Maxim

Equations

• Pragmatics.GriceanMaxims.instReprMaxim = { reprPrec := Pragmatics.GriceanMaxims.instReprMaxim.repr }

inductive Pragmatics.GriceanMaxims.QuantitySubmaxim : Type

The Quantity maxim decomposes into two independent sub-maxims. Grice (1975) states both; @cite{engelhardt-etal-2006} showed empirically that they are independently violable.

• Q1 : QuantitySubmaxim

  "Make your contribution as informative as is required (for the current purposes of the exchange)."

• Q2 : QuantitySubmaxim

  "Do not make your contribution more informative than is required."

@[implicit_reducible]

instance Pragmatics.GriceanMaxims.instDecidableEqQuantitySubmaxim : DecidableEq QuantitySubmaxim

Equations

• Pragmatics.GriceanMaxims.instDecidableEqQuantitySubmaxim x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Pragmatics.GriceanMaxims.instReprQuantitySubmaxim : Repr QuantitySubmaxim

Equations

• Pragmatics.GriceanMaxims.instReprQuantitySubmaxim = { reprPrec := Pragmatics.GriceanMaxims.instReprQuantitySubmaxim.repr }

def Pragmatics.GriceanMaxims.instReprQuantitySubmaxim.repr : QuantitySubmaxim → Nat → Std.Format

Equations

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

inductive Pragmatics.GriceanMaxims.QuantityViolation : Type

Direction of a Quantity violation.

• underInformative : QuantityViolation

  Too little information (violates Q1). E.g., "the apple" when two apples are present.

• overInformative : QuantityViolation

  Too much information (violates Q2). E.g., "the red apple" when only one apple is present.

@[implicit_reducible]

instance Pragmatics.GriceanMaxims.instDecidableEqQuantityViolation : DecidableEq QuantityViolation

Equations

• Pragmatics.GriceanMaxims.instDecidableEqQuantityViolation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Pragmatics.GriceanMaxims.instReprQuantityViolation.repr : QuantityViolation → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Pragmatics.GriceanMaxims.instReprQuantityViolation : Repr QuantityViolation

Equations

• Pragmatics.GriceanMaxims.instReprQuantityViolation = { reprPrec := Pragmatics.GriceanMaxims.instReprQuantityViolation.repr }

def Pragmatics.GriceanMaxims.QuantityViolation.submaxim : QuantityViolation → QuantitySubmaxim

Which sub-maxim a violation direction targets.

Equations

• Pragmatics.GriceanMaxims.QuantityViolation.underInformative.submaxim = Pragmatics.GriceanMaxims.QuantitySubmaxim.Q1
• Pragmatics.GriceanMaxims.QuantityViolation.overInformative.submaxim = Pragmatics.GriceanMaxims.QuantitySubmaxim.Q2

theorem Pragmatics.GriceanMaxims.violations_independent : QuantityViolation.underInformative.submaxim ≠ QuantityViolation.overInformative.submaxim

The two violation directions target different sub-maxims.

inductive Pragmatics.GriceanMaxims.MannerSubmaxim : Type

The four Manner sub-maxims (@cite{grice-1975} p.46). @cite{martin-schaefer-kastner-2025} show that M2 (avoid ambiguity) and its counterpart (maintain ambiguity) drive the distribution of French anticausative se.

• avoidObscurity : MannerSubmaxim

  M1: "Avoid obscurity of expression."

• avoidAmbiguity : MannerSubmaxim

  M2: "Avoid ambiguity." Formalized as a parse-blocking predicate in Theories.Pragmatics.AvoidAmbiguity.Blocked (@cite{jeretic-bassi-gonzalez-yatsushiro-meyer-sauerland-2025} eq 37).

• beBrief : MannerSubmaxim

  M3: "Be brief (avoid unnecessary prolixity)."

• beOrderly : MannerSubmaxim

  M4: "Be orderly."

@[implicit_reducible]

instance Pragmatics.GriceanMaxims.instDecidableEqMannerSubmaxim : DecidableEq MannerSubmaxim

Equations

• Pragmatics.GriceanMaxims.instDecidableEqMannerSubmaxim x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Pragmatics.GriceanMaxims.instReprMannerSubmaxim : Repr MannerSubmaxim

Equations

• Pragmatics.GriceanMaxims.instReprMannerSubmaxim = { reprPrec := Pragmatics.GriceanMaxims.instReprMannerSubmaxim.repr }

def Pragmatics.GriceanMaxims.instReprMannerSubmaxim.repr : MannerSubmaxim → Nat → Std.Format

Equations

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

inductive Pragmatics.GriceanMaxims.MannerViolation : Type

Direction of a Manner violation.

• obscure : MannerViolation

  Unnecessarily obscure expression (violates M1).

• ambiguous : MannerViolation

  Ambiguous when an unambiguous alternative exists (violates M2).

• verbose : MannerViolation

  Unnecessarily verbose (violates M3).

• disordered : MannerViolation

  Disordered presentation (violates M4).

@[implicit_reducible]

instance Pragmatics.GriceanMaxims.instDecidableEqMannerViolation : DecidableEq MannerViolation

Equations

• Pragmatics.GriceanMaxims.instDecidableEqMannerViolation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Pragmatics.GriceanMaxims.instReprMannerViolation.repr : MannerViolation → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Pragmatics.GriceanMaxims.instReprMannerViolation : Repr MannerViolation

Equations

• Pragmatics.GriceanMaxims.instReprMannerViolation = { reprPrec := Pragmatics.GriceanMaxims.instReprMannerViolation.repr }

def Pragmatics.GriceanMaxims.MannerViolation.submaxim : MannerViolation → MannerSubmaxim

Which sub-maxim a Manner violation targets.

Equations

• Pragmatics.GriceanMaxims.MannerViolation.obscure.submaxim = Pragmatics.GriceanMaxims.MannerSubmaxim.avoidObscurity
• Pragmatics.GriceanMaxims.MannerViolation.ambiguous.submaxim = Pragmatics.GriceanMaxims.MannerSubmaxim.avoidAmbiguity
• Pragmatics.GriceanMaxims.MannerViolation.verbose.submaxim = Pragmatics.GriceanMaxims.MannerSubmaxim.beBrief
• Pragmatics.GriceanMaxims.MannerViolation.disordered.submaxim = Pragmatics.GriceanMaxims.MannerSubmaxim.beOrderly

theorem Pragmatics.GriceanMaxims.manner_ambiguity_targets_M2 : MannerViolation.ambiguous.submaxim = MannerSubmaxim.avoidAmbiguity

The four Manner violation types each target different sub-maxims.

theorem Pragmatics.GriceanMaxims.manner_violations_M1_M2_independent : MannerViolation.obscure.submaxim ≠ MannerViolation.ambiguous.submaxim

Ambiguity and obscurity target different sub-maxims.