Relevance — @cite{sperber-wilson-1986}

Relevance is a comparative notion defined along two dimensions:

• Cognitive effects: greater effects → more relevant
• Processing effort: less effort → more relevant

The Two Principles (2nd ed, Postface)

First (Cognitive) Principle: Human cognition tends to be geared to the maximisation of relevance. (Descriptive cognitive universal, not a norm.)

Second (Communicative) Principle: Every act of ostensive communication communicates a presumption of its own optimal relevance.

Optimal Relevance (revised, 2nd ed, p. 270)

(a) Relevant enough to be worth the addressee's effort to process (b) The most relevant stimulus compatible with the communicator's abilities and preferences

Clause (b) does the work of Grice's maxim of Quantity without a cooperative principle — it derives implicatures about the speaker's knowledge and goals.

structure Theories.Pragmatics.RelevanceTheory.RelevanceAssessment : Type

Relevance assessment: the two independent dimensions.

NOT a ratio or single number. Relevance is comparative: an input is more relevant to the extent that effects are greater and effort is smaller. Some inputs are incomparable (more effects AND more effort).

• effects : ℕ

  Magnitude of positive cognitive effects

• effort : ℕ

  Processing effort required

def Theories.Pragmatics.RelevanceTheory.instDecidableEqRelevanceAssessment.decEq (x✝ x✝¹ : RelevanceAssessment) : Decidable (x✝ = x✝¹)

Equations

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

instance Theories.Pragmatics.RelevanceTheory.instDecidableEqRelevanceAssessment : DecidableEq RelevanceAssessment

Equations

• Theories.Pragmatics.RelevanceTheory.instDecidableEqRelevanceAssessment = Theories.Pragmatics.RelevanceTheory.instDecidableEqRelevanceAssessment.decEq

def Theories.Pragmatics.RelevanceTheory.instBEqRelevanceAssessment.beq : RelevanceAssessment → RelevanceAssessment → Bool

Equations

• Theories.Pragmatics.RelevanceTheory.instBEqRelevanceAssessment.beq { effects := a, effort := a_1 } { effects := b, effort := b_1 } = (a == b && a_1 == b_1)
• Theories.Pragmatics.RelevanceTheory.instBEqRelevanceAssessment.beq x✝¹ x✝ = false

instance Theories.Pragmatics.RelevanceTheory.instBEqRelevanceAssessment : BEq RelevanceAssessment

Equations

• Theories.Pragmatics.RelevanceTheory.instBEqRelevanceAssessment = { beq := Theories.Pragmatics.RelevanceTheory.instBEqRelevanceAssessment.beq }

instance Theories.Pragmatics.RelevanceTheory.instReprRelevanceAssessment : Repr RelevanceAssessment

Equations

• Theories.Pragmatics.RelevanceTheory.instReprRelevanceAssessment = { reprPrec := Theories.Pragmatics.RelevanceTheory.instReprRelevanceAssessment.repr }

def Theories.Pragmatics.RelevanceTheory.instReprRelevanceAssessment.repr : RelevanceAssessment → ℕ → Std.Format

Equations

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

def Theories.Pragmatics.RelevanceTheory.RelevanceAssessment.moreRelevant (a b : RelevanceAssessment) : Prop

Comparative relevance: a is strictly more relevant than b.

Strict partial order — some inputs are incomparable (more effects but also more effort). This partiality is deliberate: RT does not claim all inputs can be ranked on relevance.

Equations

• a.moreRelevant b = ((b.effects ≤ a.effects ∧ a.effort ≤ b.effort) ∧ (b.effects < a.effects ∨ a.effort < b.effort))

theorem Theories.Pragmatics.RelevanceTheory.RelevanceAssessment.moreRelevant_irrefl (a : RelevanceAssessment) : ¬a.moreRelevant a

Nothing is more relevant than itself.

theorem Theories.Pragmatics.RelevanceTheory.RelevanceAssessment.moreRelevant_trans {a b c : RelevanceAssessment} (hab : a.moreRelevant b) (hbc : b.moreRelevant c) : a.moreRelevant c

Comparative relevance is transitive.

def Theories.Pragmatics.RelevanceTheory.RelevanceAssessment.worthProcessing (r : RelevanceAssessment) (minEffects : ℕ) : Prop

Clause (a) of optimal relevance: the stimulus is worth processing. Its cognitive effects justify the processing effort.

S&W (Postface p. 270): "The set of assumptions {I} which the communicator intends to make manifest to the addressee is relevant enough to make it worth the addressee's while to process the ostensive stimulus."

Equations

• r.worthProcessing minEffects = (minEffects ≤ r.effects)

def Theories.Pragmatics.RelevanceTheory.RelevanceAssessment.mostRelevantCompatible (r : RelevanceAssessment) (alternatives : List RelevanceAssessment) : Prop

Clause (b) of optimal relevance: no available alternative is strictly more relevant than the stimulus actually used.

S&W (Postface p. 270): "The ostensive stimulus is the most relevant one the communicator could have used to communicate {I}."

Implicatures about the speaker's knowledge and goals derive from this clause: if a more relevant alternative existed, the speaker COULDN'T or DIDN'T WANT TO use it.

Equations

• r.mostRelevantCompatible alternatives = ∀ (alt : Theories.Pragmatics.RelevanceTheory.RelevanceAssessment), alt ∈ alternatives → ¬alt.moreRelevant r

def Theories.Pragmatics.RelevanceTheory.RelevanceAssessment.optimallyRelevant (r : RelevanceAssessment) (minEffects : ℕ) (alternatives : List RelevanceAssessment) : Prop

Optimal relevance: both clauses (a) and (b) hold jointly.

Clause (a) sets a floor on the relevance of the stimulus. Clause (b) is an optimality condition on the communicator's choice.

Equations

• r.optimallyRelevant minEffects alternatives = (r.worthProcessing minEffects ∧ r.mostRelevantCompatible alternatives)

theorem Theories.Pragmatics.RelevanceTheory.RelevanceAssessment.optimal_no_alternatives (r : RelevanceAssessment) (minEffects : ℕ) (ha : r.worthProcessing minEffects) : r.optimallyRelevant minEffects []

If a stimulus is optimally relevant with no available alternatives, clause (b) is trivially satisfied — only clause (a) matters.

theorem Theories.Pragmatics.RelevanceTheory.RelevanceAssessment.more_effects_more_relevant (e1 e2 eff : ℕ) (h : e1 < e2) : { effects := e2, effort := eff }.moreRelevant { effects := e1, effort := eff }

More effects with the same effort → more relevant.

theorem Theories.Pragmatics.RelevanceTheory.RelevanceAssessment.less_effort_more_relevant (eff1 eff2 e : ℕ) (h : eff2 < eff1) : { effects := e, effort := eff2 }.moreRelevant { effects := e, effort := eff1 }

Less effort with the same effects → more relevant.