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 : Prop' 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 : Prop' World) : Prop

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

Equations

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

def Exhaustification.FreeChoice.pdisj {World : Type u_1} (p q : Prop' World) : Prop' World

Disjunction of propositions.

Equations

• Exhaustification.FreeChoice.pdisj p q w = (p w ∨ q 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 : Prop' World
• q : Prop' World

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

The assertion: ◇(p ∨ q)

Equations

• a.assertion = Exhaustification.FreeChoice.diamond (Exhaustification.FreeChoice.pdisj 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 = (Prop' World → Prop' World)

def Exhaustification.FreeChoice.exhInCtx {World : Type u_1} (C : Ctx World) (weak strong : Prop' World) : Prop' 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 : Prop' 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 : Prop' World), (p ⊆ₚ q) → C q ⊆ₚ C p) (weak strong : Prop' 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 : Prop' 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 → Prop' World) : Prop' 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 → Prop' 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 : Prop' World), (p ⊆ₚ q) → C q ⊆ₚ C p) (D D' : Set Entity) (P : Entity → Prop' 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 : Prop' World), (p ⊆ₚ q) → C p ⊆ₚ C q) (D D' : Set Entity) (P : Entity → Prop' 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 = ∀ (φ : Prop' World), S φ ⊆ₚ φ

theorem Exhaustification.FreeChoice.intervention_negation_not_de {World : Type u_1} (S : Ctx World) (p q : Prop' 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 (Prop' 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 : Prop' World), (p ⊆ₚ q) → C q ⊆ₚ C p) (weak strong : Prop' 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 : Prop' World), (p ⊆ₚ q) → C q ⊆ₚ C p) (some_ all_ : Prop' 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.

Free Choice Duality

@cite{chierchia-2013} Ch. 5–6:

The Free Choice derivation is uniform across modal forces. Both existential FC (◇(p∨q) → ◇p ∧ ◇q) and universal FC (□(p∨q) → □p ∧ □q, i.e., "subtrigging") follow from the same double-exhaustification mechanism.

We prove this by parameterizing over an arbitrary modal operator.

@[reducible, inline]

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

A modal operator: maps a proposition about worlds to a truth value.

Equations

• Exhaustification.FreeChoice.ModalOp World = (Prop' World → Prop)

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

The FC alt set parameterized by modal operator M: Assertion M(p ∨ q), alternatives M(p), M(q), M(p ∧ q).

• M : ModalOp World
• p : Prop' World
• q : Prop' World

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

Equations

• a.assertion = a.M (Exhaustification.FreeChoice.pdisj a.p a.q)

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

Equations

• a.altP = a.M a.p

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

Equations

• a.altQ = a.M a.q

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

Equations

• a.altPQ = a.M (a.p ∧ₚ a.q)

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

theorem Exhaustification.FreeChoice.fc_duality_forward {World : Type u_1} (a : ModalFCAltSet World) (h_distrib : a.assertion → a.altP ∨ a.altQ) (h : a.exh2) : a.freeChoice

Theorem 6 (FC Duality).

For ANY modal operator M satisfying distributivity over disjunction (M(p ∨ q) → M(p) ∨ M(q)), double exhaustification yields free choice.

This covers:

• ◇ (possibility): ◇(p∨q) → ◇p ∨ ◇q trivially
• □ (necessity): □(p∨q) → □p ∨ □q (when the box distributes)
• Deontic, epistemic, ability modals

The proof is structurally identical to the ◇ case.

theorem Exhaustification.FreeChoice.diamond_distributes {World : Type u_1} (p q : Prop' World) : diamond (pdisj p q) → diamond p ∨ diamond q

Corollary: ◇ satisfies the distributivity condition.

Polarity Composition Laws

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

The four composition rules for monotonicity, grounded in Mathlib's order theory. These are the foundation for all of Chierchia's results.

theorem Exhaustification.FreeChoice.double_negation_ue {World : Type u_1} {f g : Prop' World → Prop' World} (hf : Antitone f) (hg : Antitone g) : Monotone (f ∘ g)

Double negation restores UE: "Nobody doubts that..." is UE. DE ∘ DE = UE, from Mathlib's Antitone.comp.

theorem Exhaustification.FreeChoice.ue_under_de {World : Type u_1} {f g : Prop' World → Prop' World} (hf : Monotone f) (hg : Antitone g) : Antitone (f ∘ g)

DE under UE stays DE: "It's true that nobody..." is DE. UE ∘ DE = DE

theorem Exhaustification.FreeChoice.de_under_ue {World : Type u_1} {f g : Prop' World → Prop' World} (hf : Antitone f) (hg : Monotone g) : Antitone (f ∘ g)

UE under DE stays DE: "Nobody said..." is DE when "said" is UE. DE ∘ UE = DE

theorem Exhaustification.FreeChoice.ue_under_ue {World : Type u_1} {f g : Prop' World → Prop' World} (hf : Monotone f) (hg : Monotone g) : Monotone (f ∘ g)

UE under UE stays UE: "Somebody said..." is UE. UE ∘ UE = UE

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 (Prop' World)) (φ : Prop' 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.