structure NeoGricean.Exhaustivity.Chierchia2004.StrengthenedMeaning (World : Type u_2) : Type u_2

A strengthened meaning pairs a plain denotation with its strengthened version and the alternatives used to compute the strengthening.

This is the central data structure: every propositional node in a derivation carries both ‖α‖ (plain) and ‖α‖^S (strong).

• plain : Prop' World

  ‖α‖ — the plain semantic value

• strong : Prop' World

  ‖α‖^S — the strengthened semantic value

• alternatives : Set (Prop' World)

  The scalar alternatives considered

def NeoGricean.Exhaustivity.Chierchia2004.StrengthenedMeaning.trivial {World : Type u_1} (φ : Prop' World) : StrengthenedMeaning World

Lift a plain meaning to a trivially strengthened one (‖α‖^S = ‖α‖).

Equations

• NeoGricean.Exhaustivity.Chierchia2004.StrengthenedMeaning.trivial φ = { plain := φ, strong := φ, alternatives := ∅ }

def NeoGricean.Exhaustivity.Chierchia2004.scaleAxiomsSatisfied {World : Type u_1} (activated : Set (Prop' World)) (utt : Prop' World) : Prop

Chierchia's scale axioms (99a–c) as a predicate: (a) Context activates at least 2 members of the scale (b) The uttered term is a member of the activated scale (c) The uttered term is not the strongest activated member

"Strictly stronger" means: a ⊆ₚ utt (a entails utt, true in fewer worlds) but not utt ⊆ₚ a (utt does not entail a).

Equations

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

def NeoGricean.Exhaustivity.Chierchia2004.strengthCondition {World : Type u_1} (sm : StrengthenedMeaning World) : Prop

The Strength Condition (82): ‖α‖^S must entail ‖α‖.

If this fails, the strengthened meaning is discarded and we fall back to the plain meaning. This prevents over-generation of implicatures.

Equations

• NeoGricean.Exhaustivity.Chierchia2004.strengthCondition sm = (sm.strong ⊆ₚ sm.plain)

def NeoGricean.Exhaustivity.Chierchia2004.applyStrengthCondition {World : Type u_1} (sm : StrengthenedMeaning World) (holds : Bool) : StrengthenedMeaning World

Apply the strength condition: keep strengthened meaning if it entails plain; otherwise fall back to plain. Uses a Boolean flag for decidability.

Equations

• NeoGricean.Exhaustivity.Chierchia2004.applyStrengthCondition sm holds = if holds = true then sm else { plain := sm.plain, strong := sm.plain, alternatives := sm.alternatives }

def NeoGricean.Exhaustivity.Chierchia2004.krifkaRule {World : Type u_1} (φ : Prop' World) (ALT : Set (Prop' World)) : StrengthenedMeaning World

Krifka's Rule (cf. (81)): At a scope site, introduce a direct implicature by conjoining the plain meaning with the negation of each strictly stronger alternative.

‖S‖^S = ‖S‖ ∧ ⋀{¬‖alt‖ : alt ∈ ALT, alt strictly stronger than ‖S‖}

"Strictly stronger" = a ⊆ₚ φ ∧ ¬(φ ⊆ₚ a): the alternative entails the uttered meaning but not vice versa (true in strictly fewer worlds).

This is the source of DIRECT implicatures.

Equations

• NeoGricean.Exhaustivity.Chierchia2004.krifkaRule φ ALT = { plain := φ, strong := φ ∧ₚ ⋀ {ψ : Prop' World | ∃ a ∈ ALT, ψ = ∼a ∧ (a ⊆ₚ φ) ∧ ¬φ ⊆ₚ a}, alternatives := ALT }

theorem NeoGricean.Exhaustivity.Chierchia2004.krifkaRule_satisfies_strength {World : Type u_1} (φ : Prop' World) (ALT : Set (Prop' World)) : strengthCondition (krifkaRule φ ALT)

Direct implicatures satisfy the strength condition: ‖S‖ ∧ ¬(stronger alts) entails ‖S‖.

def NeoGricean.Exhaustivity.Chierchia2004.IsDE {World : Type u_1} (f : Prop' World → Prop' World) : Prop

A context function is downward-entailing (DE) over Prop' World.

f is DE iff: φ ⊆ₚ ψ → f(ψ) ⊆ₚ f(φ).

This reverses entailment: strengthening the argument weakens the result.

Note: This is the World → Prop version, paralleling IsDownwardEntailing (Antitone) from Semantics.Entailment.Polarity which uses World → Bool.

Equations

• NeoGricean.Exhaustivity.Chierchia2004.IsDE f = ∀ (φ ψ : Prop' World), (φ ⊆ₚ ψ) → f ψ ⊆ₚ f φ

theorem NeoGricean.Exhaustivity.Chierchia2004.pneg_isDE {World : Type u_1} : IsDE pneg

Negation is DE.

def NeoGricean.Exhaustivity.Chierchia2004.strongApply {World : Type u_1} (f fS : Prop' World → Prop' World) (g : StrengthenedMeaning World) (fIsDE : Bool) : StrengthenedMeaning World

Strong Application (84): DE-sensitive function application.

This is the formal heart of @cite{chierchia-2004}.

Non-DE case (UE contexts): Pass strengthened meanings through. ‖[f g]‖^S = f^S(g^S)

DE case: Strip implicatures from the argument (use plain meaning), then add INDIRECT implicatures from the alternatives. ‖[f g]‖^S = f^S(g) ∧ₚ ⋀{∼(f(alt)) : alt ∈ g.alternatives, f(alt) not entailed}

The key insight: in DE contexts, direct SIs of the argument are blocked because strengthening the argument would WEAKEN the result. But indirect implicatures arise at the matrix level from the alternatives.

Equations

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

inductive NeoGricean.Exhaustivity.Chierchia2004.ImplicatureType : Type

Classification of implicatures by their source.

• direct : ImplicatureType

  Direct: from Krifka's Rule at a scope site (UE contexts)

• indirect : ImplicatureType

  Indirect: from Strong Application through a DE function

instance NeoGricean.Exhaustivity.Chierchia2004.instDecidableEqImplicatureType : DecidableEq ImplicatureType

Equations

• NeoGricean.Exhaustivity.Chierchia2004.instDecidableEqImplicatureType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def NeoGricean.Exhaustivity.Chierchia2004.instBEqImplicatureType.beq : ImplicatureType → ImplicatureType → Bool

Equations

• NeoGricean.Exhaustivity.Chierchia2004.instBEqImplicatureType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance NeoGricean.Exhaustivity.Chierchia2004.instBEqImplicatureType : BEq ImplicatureType

Equations

• NeoGricean.Exhaustivity.Chierchia2004.instBEqImplicatureType = { beq := NeoGricean.Exhaustivity.Chierchia2004.instBEqImplicatureType.beq }

instance NeoGricean.Exhaustivity.Chierchia2004.instReprImplicatureType : Repr ImplicatureType

Equations

• NeoGricean.Exhaustivity.Chierchia2004.instReprImplicatureType = { reprPrec := NeoGricean.Exhaustivity.Chierchia2004.instReprImplicatureType.repr }

def NeoGricean.Exhaustivity.Chierchia2004.instReprImplicatureType.repr : ImplicatureType → ℕ → Std.Format

Equations

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

def NeoGricean.Exhaustivity.Chierchia2004.implicatureSource (fIsDE : Bool) : ImplicatureType

In UE contexts, scalar items generate DIRECT implicatures. In DE contexts, the direct implicature is blocked, but the DE operator may generate INDIRECT implicatures at the matrix level.

Example:

• UE: "John ate some cookies" → direct: ¬all (from Krifka's Rule)
• DE: "John didn't eat some cookies" → direct ¬all blocked; indirect: ¬(¬all) = all may arise at matrix

Equations

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

theorem NeoGricean.Exhaustivity.Chierchia2004.si_npi_generalization {World : Type u_1} (f : Prop' World → Prop' World) (hDE : IsDE f) (g : StrengthenedMeaning World) (hStrength : g.strong ⊆ₚ g.plain) : f g.plain ⊆ₚ f g.strong

The SI-NPI Generalization (@cite{chierchia-2004}, (53)):

Scalar implicatures are systematically SUSPENDED in the same environments that LICENSE negative polarity items (NPIs).

Formally: If f is DE, then direct scalar implicatures of its argument are blocked. The strengthened argument g^S entails g (by the strength condition), so DE reverses this: f(g) ⊆ₚ f(g^S). Using the strengthened argument would WEAKEN the matrix meaning, violating the strength condition at that level.

This is exactly the DE property that licenses NPIs: DE contexts are precisely where scalar strengthening is blocked.

theorem NeoGricean.Exhaustivity.Chierchia2004.de_blocks_direct_si {World : Type u_1} (f : Prop' World → Prop' World) (hDE : IsDE f) (φ : Prop' World) (ALT : Set (Prop' World)) : have strengthened := (krifkaRule φ ALT).strong; f φ ⊆ₚ f strengthened

Corollary: Under a DE function, applying f to the Krifka-strengthened argument is WEAKER than applying f to the plain argument.

def NeoGricean.Exhaustivity.Chierchia2004.domainExhaustify {World : Type u_1} (assertion : Prop' World) (subdomainAlts : Set (Prop' World)) : Prop' World

Chierchia's O operator (cf. (127)): exhaustification over domain alternatives.

For an indefinite with domain D, the O operator provides universal closure over the domain — the NPI "widens" the domain to the maximal set, and O yields the strengthened meaning.

O_D(∃x∈D. P(x)) = ∃x∈D. P(x) ∧ ∀D'⊂D. ¬(∃x∈D'. P(x) ∧ ∀y∈D\D'. ¬P(y))

Simplified: the assertion holds AND no subdomain alternative holds.

Equations

• NeoGricean.Exhaustivity.Chierchia2004.domainExhaustify assertion subdomainAlts = assertion ∧ₚ ⋀ {ψ : Prop' World | ∃ alt ∈ subdomainAlts, ψ = ∼alt}

def NeoGricean.Exhaustivity.Chierchia2004.npiStrengtheningSucceeds {World : Type u_1} (exhaustified competitor : Prop' World) : Prop

NPI strengthening succeeds when the exhaustified meaning entails the plain meaning of the non-widened competitor.

(127): ‖any NP‖^S = O_D(∃x∈D.P(x)) must be stronger than ∃x∈D₀.P(x) where D₀ is the default (non-widened) domain.

Equations

• NeoGricean.Exhaustivity.Chierchia2004.npiStrengtheningSucceeds exhaustified competitor = (exhaustified ⊆ₚ competitor)

theorem NeoGricean.Exhaustivity.Chierchia2004.npi_blocked_under_de {World : Type u_1} (f : Prop' World → Prop' World) (hDE : IsDE f) (widened competitor : Prop' World) (hStronger : widened ⊆ₚ competitor) : f competitor ⊆ₚ f widened

NPI strengthening is BLOCKED when embedding under a DE function, because the DE function reverses the strengthening relationship.

This connects NPIs to scalar implicatures: both involve DE-ness, but for NPIs, the blocking is what makes them grammatical in DE contexts (they don't need to strengthen, so domain widening is "free").

inductive NeoGricean.Exhaustivity.Chierchia2004.ScalarStrength : Type

Intervention occurs when a strong scalar item (every, and, numerals) sits between an NPI licensor and the NPI.

The strong item generates an INDIRECT implicature that conflicts with the NPI's domain-widening requirement.

Weak items (some, or) do not intervene because they don't generate indirect implicatures that conflict.

• strong : ScalarStrength

  Strong: top of scale (every, and, all numerals > 1). Generates indirect implicatures that can interfere with NPI licensing.

• weak : ScalarStrength

  Weak: bottom of scale (some, or). No interfering indirect implicatures.

instance NeoGricean.Exhaustivity.Chierchia2004.instDecidableEqScalarStrength : DecidableEq ScalarStrength

Equations

• NeoGricean.Exhaustivity.Chierchia2004.instDecidableEqScalarStrength x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance NeoGricean.Exhaustivity.Chierchia2004.instBEqScalarStrength : BEq ScalarStrength

Equations

• NeoGricean.Exhaustivity.Chierchia2004.instBEqScalarStrength = { beq := NeoGricean.Exhaustivity.Chierchia2004.instBEqScalarStrength.beq }

def NeoGricean.Exhaustivity.Chierchia2004.instBEqScalarStrength.beq : ScalarStrength → ScalarStrength → Bool

Equations

• NeoGricean.Exhaustivity.Chierchia2004.instBEqScalarStrength.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def NeoGricean.Exhaustivity.Chierchia2004.instReprScalarStrength.repr : ScalarStrength → ℕ → Std.Format

Equations

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

instance NeoGricean.Exhaustivity.Chierchia2004.instReprScalarStrength : Repr ScalarStrength

Equations

• NeoGricean.Exhaustivity.Chierchia2004.instReprScalarStrength = { reprPrec := NeoGricean.Exhaustivity.Chierchia2004.instReprScalarStrength.repr }

def NeoGricean.Exhaustivity.Chierchia2004.intervenes (strength : ScalarStrength) : Bool

Whether a scalar item of given strength intervenes in NPI licensing.

Strong scalars generate indirect implicatures under DE operators; these indirect implicatures can block NPI strengthening. Weak scalars don't generate interfering implicatures.

Equations

• NeoGricean.Exhaustivity.Chierchia2004.intervenes NeoGricean.Exhaustivity.Chierchia2004.ScalarStrength.strong = true
• NeoGricean.Exhaustivity.Chierchia2004.intervenes NeoGricean.Exhaustivity.Chierchia2004.ScalarStrength.weak = false

theorem NeoGricean.Exhaustivity.Chierchia2004.root_ue_bridge {World : Type u_1} (φ : Prop' World) (ALT : Set (Prop' World)) (hMC : ∃ (E : Set (Prop' World)), isMCSet ALT φ E) (hFlat : ∀ a ∈ ALT, isInnocentlyExcludable ALT φ a → (a ⊆ₚ φ) ∧ ¬φ ⊆ₚ a) (w : World) : (krifkaRule φ ALT).strong w → exhIE ALT φ w

At a root-level scope site in a UE context, Chierchia's parallel strengthening entails Fox's exhIE.

Krifka's Rule produces: φ ∧ ⋀{¬alt : alt strictly stronger than φ} exhIE produces: φ ∧ ⋀{¬alt : alt innocently excludable}

On "flat" (linearly ordered) scales, every innocently excludable alternative is strictly stronger, so Krifka's output negates a superset and thus entails exhIE. The hypothesis hFlat captures this: every IE alt is strictly stronger.

Requires MC-set existence to decompose IE members into φ or ∼a forms.

inductive NeoGricean.Exhaustivity.Chierchia2004.StrengthRelation : Type

Strength relation for scalar licensing.

@cite{krifka-1995a} and @cite{chierchia-2004} treat all NPIs as STRENGTHENING: the NPI makes the assertion stronger than its scalar alternatives, so under negation the negated NPI statement is informationally weaker (= more conservative), which is the hallmark of DE environments.

@cite{schwab-2022} observes that ATTENUATING NPIs (like German "so recht") work in the opposite direction: they make the assertion WEAKER than alternatives. Under negation, the negated attenuating statement is actually STRONGER — which means attenuating NPIs should NOT produce illusion effects in non-DE environments (and empirically, they don't).

• strongerThan : StrengthRelation
• weakerThan : StrengthRelation

instance NeoGricean.Exhaustivity.Chierchia2004.instDecidableEqStrengthRelation : DecidableEq StrengthRelation

Equations

• NeoGricean.Exhaustivity.Chierchia2004.instDecidableEqStrengthRelation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance NeoGricean.Exhaustivity.Chierchia2004.instBEqStrengthRelation : BEq StrengthRelation

Equations

• NeoGricean.Exhaustivity.Chierchia2004.instBEqStrengthRelation = { beq := NeoGricean.Exhaustivity.Chierchia2004.instBEqStrengthRelation.beq }

def NeoGricean.Exhaustivity.Chierchia2004.instBEqStrengthRelation.beq : StrengthRelation → StrengthRelation → Bool

Equations

• NeoGricean.Exhaustivity.Chierchia2004.instBEqStrengthRelation.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def NeoGricean.Exhaustivity.Chierchia2004.instReprStrengthRelation.repr : StrengthRelation → ℕ → Std.Format

Equations

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

instance NeoGricean.Exhaustivity.Chierchia2004.instReprStrengthRelation : Repr StrengthRelation

Equations

• NeoGricean.Exhaustivity.Chierchia2004.instReprStrengthRelation = { reprPrec := NeoGricean.Exhaustivity.Chierchia2004.instReprStrengthRelation.repr }

def NeoGricean.Exhaustivity.Chierchia2004.scalarLicensing {World : Type u_1} (rel : StrengthRelation) (φ : Prop' World) (ALT : Set (Prop' World)) : StrengthenedMeaning World

Unified scalar licensing parametrized by direction.

For strengthening (= Krifka's ScalAssert): Assert φ and deny all strictly stronger alternatives. φ ∧ ⋀{¬alt : alt ∈ ALT, alt ⊂ φ}

For attenuating (Schwab & Liu's condition): Assert φ and affirm the existence of a strictly stronger alternative. φ ∧ ⋁{alt : alt ∈ ALT, alt ⊂ φ} (Simplified: we record the required relationship, not the full licensing.)

Equations

• One or more equations did not get rendered due to their size.
• NeoGricean.Exhaustivity.Chierchia2004.scalarLicensing NeoGricean.Exhaustivity.Chierchia2004.StrengthRelation.strongerThan φ ALT = NeoGricean.Exhaustivity.Chierchia2004.krifkaRule φ ALT

theorem NeoGricean.Exhaustivity.Chierchia2004.scalarLicensing_strongerThan_eq_krifkaRule {World : Type u_1} (φ : Prop' World) (ALT : Set (Prop' World)) : scalarLicensing StrengthRelation.strongerThan φ ALT = krifkaRule φ ALT

Bridge: scalarLicensing.strongerThan is exactly krifkaRule.

theorem NeoGricean.Exhaustivity.Chierchia2004.scalarLicensing_strongerThan_strength {World : Type u_1} (φ : Prop' World) (ALT : Set (Prop' World)) : strengthCondition (scalarLicensing StrengthRelation.strongerThan φ ALT)

Strengthening licensing satisfies the strength condition (inherits from krifkaRule).