Docs / Semantics / Exhaustification / Basic

Exhaustification

import Linglib.Semantics.Exhaustification.Basic · namespace Exhaustification

This file defines Chierchia's exhaustification operator O and its exclusion component. excludes C p holds at the worlds where every true alternative in C is entailed by the prejacent p, which is the assertion of the entailment-scale only. exh C p is the prejacent together with excludes C p: it denies every alternative the prejacent does not entail. Over finitely many worlds and an indexed family of alternatives, membership in exh is decidable.

Main statements

Exhaustification.exh_eq_sdiff: exh removes from the prejacent the alternatives it does not entail.
Exhaustification.Irredundant.excludes_injOn: over an irredundant family, exclusion separates the alternative sets that contain the prejacent.
Exhaustification.exh_setOf_not_dominated: among finitely many alternatives, the dominated ones change no exhaustification.

References

Horn 1969, A Presuppositional Analysis of Only and Even
Rooth 1992, A Theory of Focus Interpretation formalized
von Fintel 1999, NPI Licensing, Strawson Entailment, and Context Dependency formalized
Chierchia 2006, Broaden Your Views: Implicatures of Domain Widening and the “Logicality” of Language formalized
Fox & Katzir 2011, On the Characterization of Alternatives formalized
Enguehard 2025, Towards a pragmatic explanation for the prevalence of upward-monotonicity in natural language: some results on communicative stability, the strongest answer condition, and exhaustification formalized

Exclusion and exhaustification

excludes C p holds at the worlds where every true alternative in C is entailed by p.

def excludes L51–53

{W : Type u_1} (C : Set (Set W)) (p : Set W) :

Set W

excludes C p = {w : W | ∀ q ∈ C, w ∈ q → p ⊆ q}

Used by mem_excludes, exh, exh_subset_excludes, notMem_excludes, mem_excludes_of_forall_notMem, excludes_eq_compl_sUnion, excludes_antitone, antitone_excludes, excludes_union, mem_excludes_iff_forall_eq, Irredundant.excludes_ne, Irredundant.excludes_injOn

Used in Semantics/Exhaustification/InnocentExclusion, Semantics/Focus/Particles, Chierchia2004, Crnic2026b, GrubicRenansDuah2019 and 2 more

The prejacent p with every alternative it does not entail denied (Chierchia 2006's O).

def exh L57–59

{W : Type u_1} (C : Set (Set W)) (p : Set W) :

Set W

exh C p = p ∩ excludes C p

Built from

Used by mem_exh, exh_subset, exh_subset_excludes, notMem_exh, exh_subset_compl, mem_exh_image_iff, mem_exh_range_iff, instDecidablePredMemSetExhImageOfFintype, instDecidablePredMemSetExhRangeOfFintype, exh_eq_sdiff, exh_eq_self_iff, exh_eq_self, exh_empty, exh_insert_of_subset, exh_insert_of_not_subset, exh_singleton_of_not_subset, exh_antitone, mem_exh_range_iff_exhAgainst, Irredundant.mem_exh_range_iff, mem_exh_range_iff_exhAgainst_lt, exh_eq_empty_of_dominated, exh_setOf_not_dominated

Used in Semantics/Alternatives/Relevance, Semantics/Exhaustification/DomainAlternatives, Semantics/Exhaustification/InnocentExclusion, Semantics/Focus/Particles, Semantics/PolarityItem/LicensingContext and 26 more

theorem exh_eq_sdiff L105–106

{W : Type u_1} (C : Set (Set W)) (p : Set W) :

exh C p = p \ ⋃₀ {q : Set W | q ∈ C ∧ ¬p ⊆ q}

Built from

Irredundant alternatives

theorem Irredundant.excludes_injOn L182–193

{W : Type u_1} {ι : Type u_2} {f : ι → Set W} (hf : Irredundant f) (i₀ : ι) :

Set.InjOn (fun (s : Finset ι) => excludes (f '' ↑s) (f i₀)) {s : Finset ι | i₀ ∈ s}

Built from ,

Domination

Among finitely many alternatives, exhaustifying against the members that are not dominated is exhaustifying against all of them.

theorem exh_setOf_not_dominated L249–256

{W : Type u_1} {C : Set (Set W)} (hC : C.Finite) (p : Set W) :

exh {q : Set W | q ∈ C ∧ ¬Dominated C q} p = exh C p

Built from ,