Structural-pattern theorems for IE and tolerant exhaustification

[Fox07] [Chi13] [AOM25a]

The algorithmic characterizations of innocent exclusion (Fox 2007) and tolerant exhaustification (Chierchia 2013) live in Linglib/Semantics/Exhaustification/Operators/{Basic,Decidable}.lean, exposed through the Excluder packaging in InnocentExclusion.lean / Tolerant.lean. Concrete paper analyses typically need a different shape of theorem: "for an alternative set of structural shape X (singleton excludable / pairwise-disjoint cover / complement-partition / Kripke-frame lift / ...), the operator returns this specific value." That bridging layer is what this file provides.

Main results

• tolerant_exh_eq_empty_iff — tolerant.exh ALT φ = ∅ iff every φ-world belongs to some non-entailed alternative. This is the algorithm-level characterization of "contradictory tolerant exhaustification" used in [AOM25a]'s eq. 92 / root_full_tolerant_contradiction.

• innocent_exh_pairwise_disjoint_partial — when (φ \ ALT.sup id) is nonempty (the alts don't cover φ), every alternative is innocently excludable and innocent.exh ALT φ = φ \ ALT.sup id. The partial-cover witness suffices for joint full-exclusion-consistency across all α ∈ ALT simultaneously. Drives [AOM25a]'s root domain-only result (eq. 93b) and the deontic split-exh results (eq. 119, 120).

• innocent_exh_singleton_proper — corollary of the above for |ALT| = 1: when α ⊊ φ, innocent.exh {α} φ = φ \ α. Drives yek-i's root uniqueness reading ([AOM25a] eq. 93a).

• tolerant_exh_subset_innocent_exh — Chierchia's tolerant operator is always ⊆ Fox's innocent operator. Concrete form of the "tolerant excludes ≥ as much" lemma motivating the IE/tolerant divergence on EFCI alternative sets.

• innocent_exh_erase_entailed — removing an alternative entailed by the prejacent (φ ⊆ a) doesn't change innocent.exh. Drives paper-side reductions: filter the trivial alts before invoking the singleton / partial-cover theorems. Applied iteratively to drop multiple entailed alts.

Implementation notes

The theorems here are stated against innocent.exh / tolerant.exh (the Excluder packagings) rather than the lower-level Innocent.innocentlyExcludable substrate. This is the API consumed by study files, so theorems at this layer slot in directly.

Pure-logic facts about "exclusive satisfiers of a predicate" (P d ∧ ∀ e ≠ d, ¬P e) — which characterize the structural shape of pre-exhaustified domain alternatives — live in Linglib/Semantics/Quantification/Exclusive.lean. That file is framework-agnostic; this file is the Excluder-API specialization.

Todo

• innocent_exh_pairwise_disjoint_cover — when ALT's members are pairwise disjoint and their union covers φ (the complementary case to _partial), IE = ∅. This is the Spector closure-failure case driving [AOM25a] eq. 101's missing third MCE. Currently consumers reach this case via innocent_exh_eq_phi_of_innocentlyExcludable_empty + a decide on IE = ∅; a structural lemma would expose the reason for the collapse rather than the algorithm's output.

• Kripke-frame lift: a D → Bool predicate transports to W → Bool via λ w => Acc w ∧ ∃ d, P d w. The structural results about D-shape ALT sets should lift through this transport.

Tolerant: structural characterizations

theorem Exhaustification.tolerant_exh_eq_empty_of_covered {W : Type u_1} [Fintype W] [DecidableEq W] {ALT : Finset (Finset W)} {φ : Finset W} (h : ∀ w ∈ φ, ∃ α ∈ ALT, ¬φ ⊆ α ∧ w ∈ α) : tolerant.exh ALT φ = ∅

Tolerant vacuity (forward): if every φ-world belongs to some non-entailed alternative, then tolerant.exh ALT φ = ∅. The "tolerant contradiction" case driving [AOM25a] eq. 92.

theorem Exhaustification.covered_of_tolerant_exh_eq_empty {W : Type u_1} [Fintype W] [DecidableEq W] {ALT : Finset (Finset W)} {φ : Finset W} (h : tolerant.exh ALT φ = ∅) (w : W) (hw : w ∈ φ) : ∃ α ∈ ALT, ¬φ ⊆ α ∧ w ∈ α

Tolerant vacuity (backward): if tolerant.exh ALT φ = ∅, then every φ-world belongs to some non-entailed alternative.

theorem Exhaustification.tolerant_exh_eq_empty_iff {W : Type u_1} [Fintype W] [DecidableEq W] (ALT : Finset (Finset W)) (φ : Finset W) : tolerant.exh ALT φ = ∅ ↔ ∀ w ∈ φ, ∃ α ∈ ALT, ¬φ ⊆ α ∧ w ∈ α

Tolerant vacuity, biconditional: combines the two directions.

Innocent: structural characterizations

theorem Exhaustification.tolerant_exh_subset_innocent_exh {W : Type u_1} [Fintype W] [DecidableEq W] (ALT : Finset (Finset W)) (φ : Finset W) : tolerant.exh ALT φ ⊆ innocent.exh ALT φ

Innocent ≤ tolerant: Fox's IE operator returns at least as many worlds as Chierchia's tolerant operator. Equivalently, the tolerant exhaustified set is contained in the innocent one.

The reason: tolerant excludes every non-entailed alternative unconditionally; innocent only excludes those in every MCE. The MCE condition is strictly stronger, so fewer alternatives get excluded, which means fewer worlds get removed from φ.

theorem Exhaustification.innocent_exh_pairwise_disjoint_partial {W : Type u_1} [Fintype W] [DecidableEq W] {ALT : Finset (Finset W)} {φ : Finset W} (hcompat : (φ \ ALT.sup id).Nonempty) : innocent.exh ALT φ = φ \ ALT.sup id

Partial-cover alts: when (φ \ ALT.sup id).Nonempty, every alternative in ALT is innocently excludable, and innocent.exh ALT φ = φ \ ALT.sup id.

The "consumer-intent" hypotheses one might expect — ∀ α ∈ ALT, α ⊆ φ and (ALT : Set _).PairwiseDisjoint id — turn out to be unused. The single witness w ∈ φ \ ALT.sup id discharges IsInnocentlyExcludable.of_full_exclusion_consistent for every α ∈ ALT simultaneously: the witness condition w ∈ φ ∧ ∀ b ∈ ALT, w ∉ b doesn't depend on which α is being shown excludable. The MC-set {φ} ∪ ((univ \ ·) '' ALT) is then unique and contains every complement, so innocentlyExcludable ALT φ = ALT.

This lets the same substrate result fire on consumer patterns where the alts aren't subsets of φ (e.g., AOM 2025's □-side pre-exhaustified domain alts — boxB1 ∧ ¬boxB2 extends outside □(b₁⊻b₂) to worlds where canJoint is true). φ \ ALT.sup id masks the out-of-φ portion of each alt automatically.

Generalizes innocent_exh_singleton_proper (the |ALT| = 1 case; derived as a corollary below). The complementary case where ALT.sup id ⊇ φ (so hcompat fails) is covered by innocent_exh_eq_phi_of_innocentlyExcludable_empty when IE collapses.

theorem Exhaustification.innocent_exh_singleton_proper {W : Type u_1} [Fintype W] [DecidableEq W] {α φ : Finset W} (h : α ⊂ φ) : innocent.exh {α} φ = φ \ α

Singleton excludable alt: when ALT = {α} and α ⊊ φ, exhaustification returns φ \ α. This is yek-i's partial-scalar exhaustification result ([AOM25a] eq. 93a): with a single innocently-excludable alternative, IE returns it exactly, giving "exactly one" semantics.

Corollary of innocent_exh_pairwise_disjoint_partial: {α}.sup id = α, and α ⊂ φ provides the partial-cover witness.

theorem Exhaustification.innocent_exh_erase_entailed {W : Type u_1} [Fintype W] [DecidableEq W] {ALT : Finset (Finset W)} {a φ : Finset W} (h_entails : φ ⊆ a) (hphi_nonempty : φ.Nonempty) : innocent.exh ALT φ = innocent.exh (ALT.erase a) φ

Drop entailed alternative: removing an alternative a that is entailed by the prejacent (φ ⊆ a) doesn't change innocent.exh.

The entailed alt is never innocently excludable: its negation aᶜ is inconsistent with φ (the witness must satisfy both, but φ ⊆ a forces u ∈ a, hence u ∉ aᶜ). Furthermore, aᶜ is in no MC-set (same consistency argument), so the MC-set structure of ALT and ALT.erase a coincides — and therefore so do the innocentlyExcludable sets.

Lets paper analyses reduce to the substrate's singleton / partial-cover theorems after filtering out trivial alts. Applied iteratively to drop multiple entailed alts.