Chierchia 2004: parallel recursive strengthening

[Chi04] ("Scalar Implicatures, Polarity Phenomena, and the Syntax/Pragmatics Interface", §3) computes two meanings for every expression in tandem: a plain value ‖α‖ and a strengthened value ‖α‖^S that folds scalar implicatures in as soon as their triggers appear. Direct implicatures enter at scope sites by a variant of [Kri95b]'s rule (75); the Strength Condition (§3.1) requires ‖α‖^S to entail ‖α‖ at every step; and Strong Application (84) dispatches on entailment behaviour: non-DE functions pass strengthened values through, DE functions strip the argument's implicatures and add indirect implicatures at the matrix level. Implicature suspension in exactly the any-licensing environments — the Generalization on SIs (53) — is Antitone reversal of the Strength Condition, and intervention (§4.3) follows from NPIs competing with strong rather than plain meanings (127).

Implementation notes

Numbered items follow the circulated manuscript (the "Bicocca, May 2001" version); the published chapter may renumber. The paper's scalar assertion σ is a definite description — the weakest alternative asymmetrically entailing the target, ⊥ if none — well-defined only when the stronger alternatives have a greatest element, as on the paper's linearly ordered scales. Meaning.strengthen and strongApplyDE instead negate all strictly stronger alternatives, a total operation that coincides with negating σ exactly where σ is defined (strengthen_strong_eq_of_isGreatest, strongApplyDE_strong_eq_of_isGreatest; the σ = ⊥ case is the empty intersection). The appendix's ‖α‖^S is a set of admissible strong meanings (implicature addition at a scope site is optional); Meaning.strong tracks the maximal admissible strengthening, the path the paper's own computations follow.

Strengthened meanings

structure Chierchia2004.Meaning (World : Type u_2) : Type u_2

The semantic values the parallel recursion assigns to a propositional node: the plain value ‖α‖, the strengthened value ‖α‖^S, and the active scalar alternatives.

• plain : Set World

  The plain semantic value ‖α‖.

• strong : Set World

  The strengthened semantic value ‖α‖^S.

• alternatives : Set (Set World)

  The active scalar alternatives.

def Chierchia2004.Meaning.lexical {World : Type u_1} (φ : Set World) (ALT : Set (Set World)) : Meaning World

(73a): a lexical item's strong meaning is its plain meaning.

Equations

• Chierchia2004.Meaning.lexical φ ALT = { plain := φ, strong := φ, alternatives := ALT }

def Chierchia2004.Meaning.StrengthCondition {World : Type u_1} (sm : Meaning World) : Prop

The Strength Condition (§3.1): the strong value entails the plain value, sm.strong ⊆ sm.plain.

Equations

• sm.StrengthCondition = (sm.strong ⊆ sm.plain)

theorem Chierchia2004.Meaning.lexical_strengthCondition {World : Type u_1} (φ : Set World) (ALT : Set (Set World)) : (lexical φ ALT).StrengthCondition

Krifka's rule

def Chierchia2004.Meaning.strengthen {World : Type u_1} (sm : Meaning World) : Meaning World

Krifka's rule (75) [Kri95b]: at a scope site, conjoin the strong value with the negations of the strictly stronger alternatives.

Equations

• sm.strengthen = { plain := sm.plain, strong := sm.strong ∩ ⋂ a ∈ {a : Set World | a ∈ sm.alternatives ∧ a ⊂ sm.plain}, aᶜ, alternatives := sm.alternatives }

@[simp]

theorem Chierchia2004.Meaning.mem_strengthen_strong {World : Type u_1} {sm : Meaning World} {w : World} : w ∈ sm.strengthen.strong ↔ w ∈ sm.strong ∧ ∀ a ∈ sm.alternatives, a ⊂ sm.plain → w ∉ a

theorem Chierchia2004.Meaning.StrengthCondition.strengthen {World : Type u_1} {sm : Meaning World} (h : sm.StrengthCondition) : sm.strengthen.StrengthCondition

Strengthening preserves the Strength Condition.

theorem Chierchia2004.Meaning.strengthen_strong_ssubset {World : Type u_1} {sm : Meaning World} (hsc : sm.StrengthCondition) (h : ∃ a ∈ sm.alternatives, a ⊂ sm.plain ∧ a.Nonempty) : sm.strengthen.strong ⊂ sm.plain

Strengthening is proper whenever some activated alternative is strictly stronger and consistent.

theorem Chierchia2004.Meaning.strengthen_strong_eq_of_isGreatest {World : Type u_1} {sm : Meaning World} {a₀ : Set World} (h : IsGreatest {a : Set World | a ∈ sm.alternatives ∧ a ⊂ sm.plain} a₀) : sm.strengthen.strong = sm.strong ∩ a₀ᶜ

Agreement with the paper's scalar assertion σ: whenever the strictly stronger alternatives have a weakest member a₀ — the case in which (2)'s definite description is defined, as on linearly ordered scales — negating all of them is negating a₀ alone.

theorem Chierchia2004.Meaning.strengthen_strong_eq_of_not_ssubset {World : Type u_1} {sm : Meaning World} (h : ∀ a ∈ sm.alternatives, ¬a ⊂ sm.plain) : sm.strengthen.strong = sm.strong

A node none of whose alternatives is strictly stronger strengthens vacuously — the strongest member of a scale triggers no implicature ((130)).

theorem Chierchia2004.Meaning.strengthen_strong_lexical_pair {World : Type u_1} {φ ψ : Set World} (h : ψ ⊂ φ) : (lexical φ {φ, ψ}).strengthen.strong = φ \ ψ

Strengthening over a pair scale whose second member is strictly stronger: the classic "φ but not ψ" implicature.

Scale axioms

structure Chierchia2004.IsScaleSelection {World : Type u_1} (lexicalScale chosen : Set (Set World)) (utt : Set World) : Prop

An admissible context choice of scale for an uttered scalar term — the scale axioms (99).

• chosen_subset : chosen ⊆ lexicalScale

  (99a): the chosen scale is a subset of the lexical scale.

• nontrivial : chosen.Nontrivial

  (99b): the chosen scale has at least two members.

• utt_mem : utt ∈ chosen

  The uttered term belongs to its chosen scale (presupposed by (99)).

• not_strongest : (∃ a ∈ lexicalScale, a ⊂ utt) → ∃ a ∈ chosen, a ⊂ utt

  (99c): the uttered term is not the strongest chosen member whenever the lexical scale offers a stronger one — the "if possible" proviso.

theorem Chierchia2004.IsScaleSelection.strengthen_ssubset {World : Type u_1} {lex chosen : Set (Set World)} {utt : Set World} (h : IsScaleSelection lex chosen utt) (hstr : ∃ a ∈ lex, a ⊂ utt) (hne : ∀ a ∈ chosen, a ⊂ utt → a.Nonempty) : (Meaning.lexical utt chosen).strengthen.strong ⊂ utt

Under the scale axioms, a stronger lexical alternative guarantees proper strengthening — the point of the (99c) proviso.

Downward entailingness suspends implicatures

theorem Chierchia2004.si_npi_generalization {World : Type u_1} {sm : Meaning World} {f : Set World → Set World} (hDE : Antitone f) (hsc : sm.StrengthCondition) : f sm.plain ⊆ f sm.strong

Generalization on SIs (53): a DE function maps the strengthened argument to a weaker matrix value, so keeping a direct implicature under DE embedding would violate the Strength Condition — implicatures are suspended in exactly the any-licensing environments.

theorem Chierchia2004.de_blocks_direct_si {World : Type u_1} {sm : Meaning World} {f : Set World → Set World} (hDE : Antitone f) (hsc : sm.StrengthCondition) : f sm.plain ⊆ f sm.strengthen.strong

Instantiation of (53) at strengthened arguments.

Strong Application

def Chierchia2004.Meaning.map {World : Type u_1} (f fS : Set World → Set World) (g : Meaning World) : Meaning World

Apply a function and its strengthening to a node's two tracks, projecting alternatives pointwise ((82b)) — the non-DE clause of Strong Application (84).

Equations

• Chierchia2004.Meaning.map f fS g = { plain := f g.plain, strong := fS g.strong, alternatives := f '' g.alternatives }

def Chierchia2004.Meaning.weaken {World : Type u_1} (g : Meaning World) : Meaning World

The Strength-Condition fallback (§3.1): remove the argument's implicatures by resetting its strong track to the plain value.

Equations

• g.weaken = { plain := g.plain, strong := g.plain, alternatives := g.alternatives }

def Chierchia2004.strongApplyDE {World : Type u_1} (f fS : Set World → Set World) (g : Meaning World) : Meaning World

Strong Application (84), DE clause: strip the argument's implicatures, apply, and re-strengthen at the matrix level.

Equations

• Chierchia2004.strongApplyDE f fS g = (Chierchia2004.Meaning.map f fS g.weaken).strengthen

@[simp]

theorem Chierchia2004.mem_strongApplyDE_strong {World : Type u_1} {w : World} {f fS : Set World → Set World} {g : Meaning World} : w ∈ (strongApplyDE f fS g).strong ↔ w ∈ fS g.plain ∧ ∀ a ∈ g.alternatives, f a ⊂ f g.plain → w ∉ f a

theorem Chierchia2004.strongApplyDE_lexical {World : Type u_1} (f : Set World → Set World) (φ : Set World) (ALT : Set (Set World)) : strongApplyDE f f (Meaning.lexical φ ALT) = (Meaning.lexical (f φ) (f '' ALT)).strengthen

(84) at a lexical argument: apply plainly and re-run Krifka's rule over the image scale.

theorem Chierchia2004.strongApplyDE_strong_eq_of_isGreatest {World : Type u_1} {f fS : Set World → Set World} {g : Meaning World} {ψ₀ : Set World} (h : IsGreatest {ψ : Set World | ψ ∈ f '' g.alternatives ∧ ψ ⊂ f g.plain} ψ₀) : (strongApplyDE f fS g).strong = fS g.plain ∩ ψ₀ᶜ

Agreement with (84)'s matrix-level σ: inherited from the (75) lemma, the DE clause being strengthening at the mapped node.

theorem Chierchia2004.Meaning.map_strengthCondition {World : Type u_1} {f fS : Set World → Set World} {g : Meaning World} (hf : Monotone f) (hfS : fS ≤ f) (hg : g.StrengthCondition) : (map f fS g).StrengthCondition

The non-DE clause of (84) preserves the Strength Condition when f is UE and its strengthening entails it.

theorem Chierchia2004.strongApplyDE_strengthCondition {World : Type u_1} {f fS : Set World → Set World} {g : Meaning World} (hfS : fS ≤ f) : (strongApplyDE f fS g).StrengthCondition

The DE clause of (84) satisfies the Strength Condition by construction: it falls back to the plain argument before re-strengthening.

The direct implicature of "some"

def Chierchia2004.sawSome : Set (Fin 3)

Worlds for "John saw some students": saw none, some-but-not-all, or all.

Equations

• Chierchia2004.sawSome = {w : Fin 3 | w ≠ 0}

def Chierchia2004.sawEvery : Set (Fin 3)

"John saw every student" — true only in the saw-all world.

Equations

• Chierchia2004.sawEvery = {w : Fin 3 | w = 2}

theorem Chierchia2004.sawEvery_ssubset : sawEvery ⊂ sawSome

theorem Chierchia2004.some_not_all_implicature : (Meaning.lexical sawSome {sawSome, sawEvery}).strengthen.strong = sawSome \ sawEvery

(74)–(76): strengthening the lexical node of "John saw some students" computes the direct implicature — some but not every.

The doubt example

def Chierchia2004.drinks : Set (Bool × Bool)

"John drinks", over worlds valuating ⟨drinks, drives⟩.

Equations

• Chierchia2004.drinks = {w : Bool × Bool | w.1 = true}

def Chierchia2004.drives : Set (Bool × Bool)

"John drives".

Equations

• Chierchia2004.drives = {w : Bool × Bool | w.2 = true}

theorem Chierchia2004.drinks_ne_drives : drinks ≠ drives

theorem Chierchia2004.doubt_and_indirect_implicature : (strongApplyDE compl compl (Meaning.lexical (drinks ∩ drives) {drinks ∩ drives, drinks ∪ drives})).strong = (drinks ∩ drives)ᶜ ∩ (drinks ∪ drives)

The (81)–(83) computation: embedding "John drinks and drives" under DE doubt (modelled as complement) yields the indirect implicature (83b) — doubt the conjunction yet believe the disjunction.

Intervention

def Chierchia2004.ateCake : Set (Bool × Bool × Bool)

Worlds valuate ⟨John ate the cake, drank coffee c₁, drank coffee c₂⟩; {c₁} is the default coffee domain and {c₁, c₂} its widening.

Equations

• Chierchia2004.ateCake = {w : Bool × Bool × Bool | w.1 = true}

def Chierchia2004.drankC1 : Set (Bool × Bool × Bool)

"John drank some coffee" on the default domain {c₁}.

Equations

• Chierchia2004.drankC1 = {w : Bool × Bool × Bool | w.2.1 = true}

def Chierchia2004.drankC2 : Set (Bool × Bool × Bool)

"John drank coffee c₂" — the widened part of the domain.

Equations

• Chierchia2004.drankC2 = {w : Bool × Bool × Bool | w.2.2 = true}

def Chierchia2004.anyAndClosure : Set (Bool × Bool × Bool)

(128b): universal closure over domain choices of "I doubt that John ate the cake and drank any coffee", spelled out over the nonempty subdomains of {c₁, c₂}.

Equations

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

def Chierchia2004.someAndCompetitor : Meaning (Bool × Bool × Bool)

The some-competitor of (128): "I doubt that John ate the cake and drank some coffee" ((129a)), strengthened by the DE clause of (84).

Equations

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

theorem Chierchia2004.ateCake_ne_drankC1 : ateCake ≠ drankC1

theorem Chierchia2004.someAndCompetitor_strong : someAndCompetitor.strong = (ateCake ∩ drankC1)ᶜ ∩ (ateCake ∪ drankC1)

(129b): the competitor's strong meaning — doubt the conjunction yet believe John did one of the two.

theorem Chierchia2004.and_blocks_any : ¬anyAndClosure ⊆ someAndCompetitor.strong

(127)/(128): any is blocked under doubt … and. The universal closure fails to entail the competitor's strong meaning — the indirect implicature of the intervening and is what breaks the entailment.

theorem Chierchia2004.and_any_entails_plain : anyAndClosure ⊆ (ateCake ∩ drankC1)ᶜ

The closure does entail the competitor's plain meaning: competition with plain meanings ((122)-style) would wrongly license any under and.

def Chierchia2004.anyOrClosure : Set (Bool × Bool × Bool)

(130): universal closure of "I doubt that John ate the cake or drank any coffee" over the nonempty subdomains of {c₁, c₂}.

Equations

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

def Chierchia2004.someOrCompetitor : Meaning (Bool × Bool × Bool)

The some-competitor of (130): under doubt, or is the strongest member of its scale, so no indirect implicature arises.

Equations

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

theorem Chierchia2004.someOrCompetitor_strong : someOrCompetitor.strong = (ateCake ∪ drankC1)ᶜ

(130): the or-competitor's strong meaning is its plain meaning — the strongest member of a scale triggers no implicature.

theorem Chierchia2004.or_licenses_any : anyOrClosure ⊆ someOrCompetitor.strong

(130): any is licensed under doubt … or — the closure entails the competitor's strong meaning, which never gained an indirect implicature.