The Comprehension Procedure — @cite{sperber-wilson-1986}

The comprehension procedure is the heart of RT's account of utterance understanding. S&W (2nd ed, Postface):

"Follow a path of least effort in computing cognitive effects. Test interpretive hypotheses in order of accessibility. Stop when your expectations of relevance are satisfied."

This is an ordered search with a satisficing criterion:

1. Consider candidate interpretations in order of accessibility
2. For each, assess whether it achieves enough cognitive effects
3. Accept the FIRST interpretation that meets the relevance threshold
4. If none does, communication fails

The RT Argument Form

The characteristic RT argument shows that interpretation I is selected by the comprehension procedure in a given scenario. In Lean:

theorem my_analysis :
    scenario.comprehensionSelects interpretationI :=...

This requires showing three things:

1. I is a candidate interpretation
2. I's effects reach the relevance threshold (clause a)
3. No more accessible candidate also reaches the threshold (first acceptable)

Processing Effort Arguments

Processing effort enters at TWO levels:

1. Accessibility ordering: more effort → less accessible → tried later. This is the accessibility field: it determines the ORDER of search.
2. Relevance trade-off: more effort → less relevant (other things equal). This is the effort field: it can RAISE the threshold for an interpretation to count as "worth processing."

The adjustedThreshold captures this: an interpretation that requires more effort must produce proportionally more effects to satisfy clause (a). Set effortWeight = 0 to ignore effort in the threshold (pure effects-based).

structure Theories.Pragmatics.RelevanceTheory.RTScenario (I : Type u_1) : Type u_1

An RT scenario: everything the comprehension procedure needs.

The practitioner sets up a scenario by specifying candidates, their accessibility ordering, their effects, and the relevance threshold. The comprehension procedure determines which interpretation is selected.

Processing effort: enter effort values per interpretation. The adjustedThreshold adds effortWeight * effort i to the base threshold, so costlier interpretations must produce more effects.

• candidates : List I

  Candidate interpretations

• accessibility : I → ℕ

  Accessibility ordering: lower = more accessible = tried first. Encodes the "path of least effort" — more accessible interpretations require less processing effort to ACCESS (not to SATISFY).

• effects : I → ℕ

  Cognitive effects of each interpretation

• effort : I → ℕ

  Processing effort of each interpretation (cost to derive it)

• threshold : ℕ

  Base relevance threshold: minimum effects to be worth processing when effort is zero

• effortWeight : ℕ

  How much each unit of effort raises the threshold. Set to 0 for pure effects-based assessment.

def Theories.Pragmatics.RelevanceTheory.RTScenario.adjustedThreshold {I : Type u_1} (s : RTScenario I) (i : I) : ℕ

The adjusted threshold for interpretation i: base threshold plus effort-proportional cost. An interpretation must produce at least this many effects to be "worth processing."

Equations

• s.adjustedThreshold i = s.threshold + s.effortWeight * s.effort i

def Theories.Pragmatics.RelevanceTheory.RTScenario.comprehensionSelects {I : Type u_1} (s : RTScenario I) (i : I) : Prop

The comprehension procedure selects interpretation i.

An interpretation is selected iff:

1. It is a candidate
2. Its effects reach the adjusted threshold (clause a: worth processing)
3. No more accessible candidate also reaches its own threshold (first acceptable: the hearer stops at the first good-enough answer)

The third condition makes the procedure SATISFICING, not OPTIMIZING — the hearer doesn't search for the best interpretation, just the first good enough one.

Equations

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

def Theories.Pragmatics.RelevanceTheory.RTScenario.communicationFails {I : Type u_1} (s : RTScenario I) : Prop

Communication failure: no candidate reaches its relevance threshold.

Equations

• s.communicationFails = ∀ (i : I), i ∈ s.candidates → s.effects i < s.adjustedThreshold i

theorem Theories.Pragmatics.RelevanceTheory.RTScenario.selects_not_fails {I : Type u_1} (s : RTScenario I) (i : I) (h : s.comprehensionSelects i) : ¬s.communicationFails

If the procedure selects i, communication does not fail.

theorem Theories.Pragmatics.RelevanceTheory.RTScenario.selected_blocks {I : Type u_1} (s : RTScenario I) (i j : I) (hi : s.comprehensionSelects i) (hj : j ∈ s.candidates) (hacc : s.accessibility j < s.accessibility i) : s.effects j < s.adjustedThreshold j

If i is selected, every more accessible candidate fails its threshold.

theorem Theories.Pragmatics.RelevanceTheory.RTScenario.selects_at_most_one {I : Type u_1} (s : RTScenario I) (i j : I) (hi : s.comprehensionSelects i) (hj : s.comprehensionSelects j) (hacc : s.accessibility i < s.accessibility j) : False

Two interpretations at different accessibility levels cannot both be selected: the more accessible one would block the less accessible one.

This is a direct consequence of satisficing: once the procedure stops at the first good-enough interpretation, less accessible candidates are never reached.

theorem Theories.Pragmatics.RelevanceTheory.RTScenario.selected_passes_threshold {I : Type u_1} (s : RTScenario I) (i : I) (h : s.comprehensionSelects i) : s.adjustedThreshold i ≤ s.effects i

The selected interpretation passes its threshold.

theorem Theories.Pragmatics.RelevanceTheory.RTScenario.most_accessible_selected {I : Type u_1} (s : RTScenario I) (i : I) (hmem : i ∈ s.candidates) (hpass : s.adjustedThreshold i ≤ s.effects i) (hmost : ∀ (j : I), j ∈ s.candidates → ¬s.accessibility j < s.accessibility i) : s.comprehensionSelects i

If the most accessible candidate passes threshold, it is selected.

def Theories.Pragmatics.RelevanceTheory.RTScenario.blockedByEffort {I : Type u_1} (s : RTScenario I) (i : I) : Prop

A processing effort argument: interpretation i is DISpreferred because its effort raises the threshold above its effects, even though it would be acceptable at zero effort.

Example: in a rapid conversational exchange, enriching "some" to "some but not all" may cost more effort than the effects justify, even though in a slower context the enriched reading would be selected.

This mechanism is distinctive to RT — NeoGricean theories have no counterpart.

Equations

• s.blockedByEffort i = (s.threshold ≤ s.effects i ∧ s.effects i < s.adjustedThreshold i)

def Theories.Pragmatics.RelevanceTheory.RTScenario.effortFree {I : Type u_1} (s : RTScenario I) : Prop

An effort-free scenario: effort plays no role in relevance assessment. Useful when the argument turns purely on effects, not processing cost.

Equations

• s.effortFree = (s.effortWeight = 0)

theorem Theories.Pragmatics.RelevanceTheory.RTScenario.effortFree_threshold {I : Type u_1} (s : RTScenario I) (i : I) (h : s.effortFree) : s.adjustedThreshold i = s.threshold

In an effort-free scenario, the adjusted threshold equals the base.

theorem Theories.Pragmatics.RelevanceTheory.RTScenario.effortFree_not_blocked {I : Type u_1} (s : RTScenario I) (i : I) (h : s.effortFree) : ¬s.blockedByEffort i

Effort blocking requires nonzero effort weight — in an effort-free scenario, no interpretation can be blocked by effort.

structure Theories.Pragmatics.RelevanceTheory.ClauseBArgument (I : Type u_2) : Type u_2

Clause (b) of optimal relevance: the communicator's choice was the most relevant compatible with their abilities and preferences.

An alternative stimulus alt was AVAILABLE but not used. If alt would have been more relevant (more effects, less effort), the hearer can infer the communicator COULDN'T or DIDN'T WANT TO use it.

This derives implicatures about the speaker's epistemic state.

Example: "Some students passed" rather than "All students passed" → the speaker wasn't in a position to say "all" → speaker doesn't believe all passed.

• actual : I

  The stimulus actually used

• alternative : I

  An alternative the communicator could have used

• alternativeMoreRelevant : Prop

  The alternative would have been more relevant

• communicatorConstraint : Prop

  The communicator's constraint: inability or preference

structure Theories.Pragmatics.RelevanceTheory.RTScenario.StructuralVariant {I : Type u_1} (s₁ s₂ : RTScenario I) : Prop

Two scenarios are STRUCTURAL VARIANTS when they share the same candidate set and accessibility ordering. This is the natural comparison class in RT: the same utterance type processed in different contexts, where context modulates effects/effort/threshold but not the interpretive search path.

Structural variants support monotonicity reasoning: if interpretation i is selected in one variant, sufficient conditions for transferring selection to another can be stated algebraically.

• candidates_eq : s₁.candidates = s₂.candidates

  Same candidate interpretations

• accessibility_eq (x : I) : s₁.accessibility x = s₂.accessibility x

  Same accessibility ordering (search path)

theorem Theories.Pragmatics.RelevanceTheory.RTScenario.selects_of_strengthened_effects {I : Type u_2} (s₁ s₂ : RTScenario I) (i : I) (hvar : s₁.StructuralVariant s₂) (hsel : s₁.comprehensionSelects i) (hthr : s₁.threshold = s₂.threshold) (hew : s₁.effortWeight = s₂.effortWeight) (heffort : ∀ (x : I), s₁.effort x = s₂.effort x) (hi_stronger : s₁.effects i ≤ s₂.effects i) (hj_weaker : ∀ (j : I), j ∈ s₁.candidates → s₁.accessibility j < s₁.accessibility i → s₂.effects j ≤ s₁.effects j) : s₂.comprehensionSelects i

Effect strengthening preserves selection: if interpretation i is selected in scenario s₁, and s₂ is a structural variant with the same threshold parameters where i's effects are weakly higher and every more-accessible candidate's effects are weakly lower, then i is also selected in s₂.

This is the core monotonicity property of RT's comprehension procedure. Increasing the cognitive effects of an interpretation (while not strengthening blocking candidates) can only help it get selected.

The theorem is independent of whether the comprehension procedure is modeled as a step function (qualitative RT) or a sigmoid (graded extension): the ordinal prediction — which interpretation is on the passing side — is preserved under effect strengthening regardless of threshold shape.