Core Theorems from @cite{chierchia-2013} Logic in Grammar

@cite{chierchia-2013} @cite{fox-2007} @cite{spector-2016}

Deep integration of Chierchia's central results connecting polarity, scalar implicatures, free choice, and intervention — all with real proofs.

Main results

1. Free Choice via Double Exhaustification (Ch. 2, 5): Exh(Exh(◇(p ∨ q))) ↔ ◇p ∧ ◇q

2. SI–NPI Generalization (Ch. 1–2): Scalar implicatures are vacuous in exactly DE contexts.

3. Domain Widening Reversal (Ch. 1, 3): Widening strengthens in DE contexts, weakens in UE contexts.

4. Intervention Disrupts DE (Ch. 7): Inserting a non-monotone strengthening operator inside a DE context destroys the DE property, blocking NPI licensing.

5. Scalar Reversal (Ch. 1): The same scale produces opposite implicatures in UE vs DE contexts.

6. FC Duality (Ch. 5–6): Free choice works uniformly for ◇ and □ via the same exhaustification.

Free Choice Derivation

Chierchia's signature result: the Free Choice inference for permission sentences like "You may have coffee or tea" → "You may have coffee AND you may have tea" is derived grammatically via double exhaustification.

We work over an abstract World type where ◇p = ∃ w, p w.

def Exhaustification.FreeChoice.diamond {World : Type u_1} (p : Set World) : Prop

Possibility modal: ◇p holds iff p is true at some accessible world.

Equations

• Exhaustification.FreeChoice.diamond p = ∃ (w : World), p w

def Exhaustification.FreeChoice.box {World : Type u_1} (p : Set World) : Prop

Necessity modal: □p holds iff p is true at all accessible worlds.

Equations

• Exhaustification.FreeChoice.box p = ∀ (w : World), p w

structure Exhaustification.FreeChoice.FCAltSet (World : Type u_2) : Type u_2

The alternative set for ◇(p ∨ q) consists of {◇p, ◇q, ◇(p ∧ q)}.

This is the standard alternative set: subdomain alternatives ◇p, ◇q (restricting the disjunction) and the conjunction alternative ◇(p ∧ q) (strengthening the disjunction).

• p : Set World
• q : Set World

def Exhaustification.FreeChoice.FCAltSet.assertion {World : Type u_1} (a : FCAltSet World) : Prop

The assertion: ◇(p ∨ q)

Equations

• a.assertion = Exhaustification.FreeChoice.diamond (a.p ∪ a.q)

def Exhaustification.FreeChoice.FCAltSet.altP {World : Type u_1} (a : FCAltSet World) : Prop

Alternative: ◇p

Equations

• a.altP = Exhaustification.FreeChoice.diamond a.p

def Exhaustification.FreeChoice.FCAltSet.altQ {World : Type u_1} (a : FCAltSet World) : Prop

Alternative: ◇q

Equations

• a.altQ = Exhaustification.FreeChoice.diamond a.q

def Exhaustification.FreeChoice.FCAltSet.altPQ {World : Type u_1} (a : FCAltSet World) : Prop

Alternative: ◇(p ∧ q)

Equations

• a.altPQ = Exhaustification.FreeChoice.diamond (a.p ∩ a.q)

def Exhaustification.FreeChoice.FCAltSet.exh1 {World : Type u_1} (a : FCAltSet World) : Prop

First exhaustification: Exh(◇(p ∨ q)) = ◇(p ∨ q) ∧ ¬◇(p ∧ q)

The conjunction alternative ◇(p ∧ q) is the unique innocently excludable alternative at this stage — excluding either ◇p or ◇q alone would be incompatible with the assertion.

Equations

• a.exh1 = (a.assertion ∧ ¬a.altPQ)

def Exhaustification.FreeChoice.FCAltSet.exhAltP {World : Type u_1} (a : FCAltSet World) : Prop

The strengthened alternatives after first Exh: Exh(◇p) = ◇p ∧ ¬◇q and Exh(◇q) = ◇q ∧ ¬◇p

These are the alternatives to the exhaustified sentence, obtained by exhaustifying each subdomain alternative the same way.

Equations

• a.exhAltP = (a.altP ∧ ¬a.altQ)

def Exhaustification.FreeChoice.FCAltSet.exhAltQ {World : Type u_1} (a : FCAltSet World) : Prop

Equations

• a.exhAltQ = (a.altQ ∧ ¬a.altP)

def Exhaustification.FreeChoice.FCAltSet.exh2 {World : Type u_1} (a : FCAltSet World) : Prop

Second exhaustification: Exh(Exh(◇(p ∨ q))) = Exh₁ ∧ ¬(◇p ∧ ¬◇q) ∧ ¬(◇q ∧ ¬◇p)

Now the strengthened subdomain alternatives are innocently excludable.

Equations

• a.exh2 = (a.exh1 ∧ ¬a.exhAltP ∧ ¬a.exhAltQ)

def Exhaustification.FreeChoice.FCAltSet.freeChoice {World : Type u_1} (a : FCAltSet World) : Prop

Free choice: ◇p ∧ ◇q

Equations

• a.freeChoice = (a.altP ∧ a.altQ)

theorem Exhaustification.FreeChoice.free_choice_forward {World : Type u_1} (a : FCAltSet World) (h : a.exh2) : a.freeChoice

Theorem 1 (Free Choice via Double Exhaustification).

@cite{chierchia-2013} Ch. 2, 5; @cite{fox-2007}:

Exh(Exh(◇(p ∨ q))) → ◇p ∧ ◇q

Double exhaustification of a disjunction under a possibility modal yields the conjunctive (free choice) reading.

Proof: The second Exh negates ◇p∧¬◇q and ◇q∧¬◇p. Combined with the assertion ◇(p∨q), we derive both ◇p and ◇q.

theorem Exhaustification.FreeChoice.free_choice_backward {World : Type u_1} (a : FCAltSet World) (hfc : a.freeChoice) (hnpq : ¬a.altPQ) : a.exh2

Theorem 1 (converse direction).

◇p ∧ ◇q ∧ ¬◇(p ∧ q) → Exh(Exh(◇(p ∨ q)))

When both disjuncts are individually possible but their conjunction is not, we get exactly the double-exhaustified meaning.

The SI–NPI Generalization

@cite{chierchia-2013} Ch. 1–2, building on @cite{chierchia-2004}:

Scalar implicatures are blocked in exactly the environments that license NPIs — namely, Downward Entailing environments.

In a DE environment f, if strong ⊆ weak (strong entails weak), then f weak ⊆ f strong (f reverses the entailment). Exhaustifying f(weak) by negating f(strong) would produce f(weak) ∩ ∼(f(strong)), but since f(weak) ⊆ f(strong), this is contradictory — i.e., the scalar implicature is vacuous.

@[reducible, inline]

abbrev Exhaustification.FreeChoice.Ctx (World : Type u_2) : Type u_2

A context function mapping propositions to propositions.

Equations

• Exhaustification.FreeChoice.Ctx World = (Set World → Set World)

def Exhaustification.FreeChoice.exhInCtx {World : Type u_1} (C : Ctx World) (weak strong : Set World) : Set World

Exhaustification in context: assert C(weak) and negate C(strong).

Equations

• Exhaustification.FreeChoice.exhInCtx C weak strong = C weak ∩ (C strong)ᶜ

def Exhaustification.FreeChoice.siVacuous {World : Type u_1} (C : Ctx World) (weak strong : Set World) : Prop

The SI is vacuous: the exhaustified meaning entails ⊥ (is empty).

Equations

• Exhaustification.FreeChoice.siVacuous C weak strong = ∀ (w : World), ¬Exhaustification.FreeChoice.exhInCtx C weak strong w

theorem Exhaustification.FreeChoice.si_vacuous_in_de {World : Type u_1} (C : Ctx World) (hDE : ∀ (p q : Set World), p ⊆ q → C q ⊆ C p) (weak strong : Set World) (h_ent : strong ⊆ weak) : siVacuous C weak strong

Theorem 2 (SI–NPI Generalization, one direction).

In a DE context, if strong ⊆ weak, then the scalar implicature C(weak) ∧ ¬C(strong) is contradictory (vacuous).

This is the formal content of Chierchia's observation that SIs are suspended in NPI-licensing environments.

theorem Exhaustification.FreeChoice.si_active_witness {World : Type u_1} (C : Ctx World) (weak strong : Set World) (h_witness : ∃ (w : World), C weak w ∧ ¬C strong w) : ¬siVacuous C weak strong

Theorem 2 (converse direction).

If the SI is non-vacuous, there must be some world where it fires.

Domain Widening and Informativity

@cite{chierchia-2013} Ch. 1, 3, building on @cite{kadmon-landman-1993}:

NPIs like "any" are indefinites with obligatory domain widening.

• In UE contexts, widening the domain is weakening (less informative) → bad
• In DE contexts, widening the domain is strengthening (more informative) → good

This explains NPI licensing: "any" is grammatical exactly where its obligatory widening is informative, i.e., in DE contexts.

def Exhaustification.FreeChoice.existsInDomain {World : Type u_1} {Entity : Type u_2} (D : Set Entity) (P : Entity → Set World) : Set World

An existential statement over a domain D: ∃ x ∈ D, P x.

Equations

• Exhaustification.FreeChoice.existsInDomain D P w = ∃ x ∈ D, P x w

theorem Exhaustification.FreeChoice.wider_domain_weaker_existential {World : Type u_1} {Entity : Type u_2} (D D' : Set Entity) (P : Entity → Set World) (h : D ⊆ D') : existsInDomain D P ⊆ existsInDomain D' P

Widening the domain is weakening: if D ⊆ D', then (∃x∈D, Px) ⊆ (∃x∈D', Px).

Larger domain = more potential witnesses = weaker existential claim.

theorem Exhaustification.FreeChoice.widening_strengthens_in_de {World : Type u_1} {Entity : Type u_2} (C : Ctx World) (hDE : ∀ (p q : Set World), p ⊆ q → C q ⊆ C p) (D D' : Set Entity) (P : Entity → Set World) (h : D ⊆ D') : C (existsInDomain D' P) ⊆ C (existsInDomain D P)

Theorem 3a (Widening strengthens in DE).

In a DE context, widening the domain of an indefinite strengthens the overall claim: C(∃x∈D', Px) ⊆ C(∃x∈D, Px) when D ⊆ D'.

This is why NPIs are licensed in DE contexts: widening is informative.

theorem Exhaustification.FreeChoice.widening_weakens_in_ue {World : Type u_1} {Entity : Type u_2} (C : Ctx World) (hUE : ∀ (p q : Set World), p ⊆ q → C p ⊆ C q) (D D' : Set Entity) (P : Entity → Set World) (h : D ⊆ D') : C (existsInDomain D P) ⊆ C (existsInDomain D' P)

Theorem 3b (Widening weakens in UE).

In a UE context, widening the domain weakens the overall claim: C(∃x∈D, Px) ⊆ C(∃x∈D', Px) when D ⊆ D'.

This is why NPIs are not licensed in UE contexts: widening is uninformative (violates Maximize Strength).

Intervention Effects

@cite{chierchia-2013} Ch. 7:

Scalar triggers embedded between an NPI licensor and the NPI can disrupt licensing. This is because exhaustification (EXH) applied at the scalar trigger's scope is not monotone: it can break the Downward Entailing property of the embedding context.

Key insight: Exhaustification is a strengthening operation (exh(φ) ⊆ φ). Any non-trivial strengthening can disrupt antitonicity because subset-preservation is not preserved under arbitrary strengthening.

def Exhaustification.FreeChoice.IsStrengthening {World : Type u_1} (S : Ctx World) : Prop

An operator S is a strengthening operator if S(φ) ⊆ φ for all φ.

Equations

• Exhaustification.FreeChoice.IsStrengthening S = ∀ (φ : Set World), S φ ⊆ φ

theorem Exhaustification.FreeChoice.intervention_negation_not_de {World : Type u_1} (S : Ctx World) (p q : Set World) (_hpq : p ⊆ q) (w : World) (hSpw : S p w) (hnSqw : ¬S q w) : ¬(S q)ᶜ ⊆ (S p)ᶜ

Theorem 4 (Intervention disrupts DE).

If S is not monotone (∃ p ⊆ q with ¬(S p ⊆ S q)), then composing negation (a DE context) with S fails to be DE.

This captures Chierchia's insight: a scalar trigger (which acts like Exh, a non-monotone strengthening operator) between an NPI licensor and an NPI disrupts the DE chain.

theorem Exhaustification.FreeChoice.exh_is_strengthening {World : Type u_1} (ALT : Set (Set World)) : IsStrengthening (exhMW ALT)

Corollary: Exhaustification (Exh) is the prototypical intervener.

Exh is strengthening (exh(φ) ⊆ φ) and not monotone (∃ p ⊆ q with exh(p) ⊄ exh(q)). So Exh inserted between a DE licensor and an NPI disrupts the DE property.

Scalar Reversal in DE Contexts

@cite{chierchia-2013} Ch. 1:

The same Horn scale produces opposite effects depending on polarity:

• In UE: "some" implicates "not all" (negate stronger alternative)
• In DE: "some" is STRONGER than "all" (entailment reverses), so exhaustification is vacuous

This is proven as a direct consequence of antitonicity.

theorem Exhaustification.FreeChoice.entailment_reversal_in_de {World : Type u_1} (C : Ctx World) (hDE : ∀ (p q : Set World), p ⊆ q → C q ⊆ C p) (weak strong : Set World) (h : strong ⊆ weak) : C weak ⊆ C strong

Theorem 5 (Entailment reversal in DE contexts).

If strong ⊆ weak (strong entails weak) and C is DE, then C weak ⊆ C strong (C(weak) entails C(strong)).

The "stronger" alternative in UE becomes the "weaker" one in DE, making the exhaustification move vacuous.

theorem Exhaustification.FreeChoice.weak_is_strong_in_de {World : Type u_1} (C : Ctx World) (hDE : ∀ (p q : Set World), p ⊆ q → C q ⊆ C p) (some_ all_ : Set World) (h : all_ ⊆ some_) : C some_ ⊆ C all_

Corollary: In DE, the "weak" scalar term is informationally stronger.

"Not all students came" entails "Not some students came" (= "No student came"). So in "not ___ students came", "some" is the stronger filler. This is why "any" (= widened "some") is licensed: it's the strongest.

Diamond distributes over union

@cite{chierchia-2013} Ch. 5–6 motivates the FC derivation as uniform across modal forces; this section provides the basic distribution lemma ◇(A ∪ B) ↔ ◇A ∨ ◇B consumed by @cite{ciardelli-guerrini-2026}'s reductionist thesis.

theorem Exhaustification.FreeChoice.diamond_distributes {World : Type u_1} (p q : Set World) : diamond (p ∪ q) → diamond p ∨ diamond q

◇ distributes over union.

theorem Exhaustification.FreeChoice.diamond_collects {World : Type u_1} (p q : Set World) : diamond p ∨ diamond q → diamond (p ∪ q)

Reverse: ◇A ∨ ◇B → ◇(A ∨ B).

theorem Exhaustification.FreeChoice.diamond_distributes_iff {World : Type u_1} (p q : Set World) : diamond (p ∪ q) ↔ diamond p ∨ diamond q

◇(A ∨ B) ↔ ◇A ∨ ◇B: the scope distinction is truth-conditionally vacuous in standard modal logic. Central to @cite{ciardelli-guerrini-2026}'s reductionist thesis: the difference between narrow-scope ◇(A ∨ B) and wide-scope ◇A ∨ ◇B matters only for pragmatic enrichment.

Maximize Strength as Exhaustification

@cite{chierchia-2013} Ch. 1 §1.1.4:

Maximize Strength says: among alternative parses, prefer the one that generates the strongest (most informative) proposition. This is equivalent to applying the exhaustivity operator, since exhaustification negates alternatives to produce the strongest consistent meaning.

theorem Exhaustification.FreeChoice.maximize_strength_eq_exhIE {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) : exhIE ALT φ ⊆ φ

Maximize Strength: exhIE produces an interpretation that entails the plain meaning — it is a strengthening operation. This is Chierchia's Maximize Strength principle formalized as the defining property of exhaustification.