Exhaustivity Operators: exhMW and exhIE

@cite{groenendijk-stokhof-1984} @cite{spector-2016} @cite{wang-2025} @cite{chierchia-2013}

Formalization of @cite{spector-2016} "Comparing exhaustivity operators" (Semantics & Pragmatics 9, Article 11: 1–33).

Paper structure

• §2.1 Definitions 1–4: ≤_ALT, exhMW, compatible sets, MC-sets, IE, exhIE
• §3.4 Propositions 6, 7, Corollary 8: exhMW ⊆ exhIE and characterisation
• §3.5 Theorem 9 (main result): closure under ∧ gives exhMW = exhIE
• §3.6 Theorem 10, Corollary 11: closure under ∨ is vacuous for exhIE
• §5.3 Lemmas 1, 2, 3: minimal-world ↔ MC-set connection
• §5.4 Proof of Theorem 9

Set-theoretic operators use mathlib primitives directly: ⊆ (subset), ·ᶜ (complement), ∩ (intersection), ⋂₀ (sInter), ⋃₀ (sUnion).

Relation to the Finset / Excluder API

This file is the reference formalization of Spector 2016, faithful to the paper's prose and the natural home for paper-level theorems (Props 6/7, Cor 8, Thm 9, Thm 10). The computational refinement lives in Exhaustification/Innocent.lean (the Finset-canonical version, plugged into the Excluder strategy interface from Excluder.lean). Exhaustification/SetFinsetBridge.lean proves the two agree on IsCompatible, IsMCSet, IE, and IsInnocentlyExcludable, so results proven on either side are usable from the other. New code that needs decidability or Excluder uniformity should prefer the Finset side.

def Exhaustification.leALT {World : Type u_1} (ALT : Set (Set World)) (u v : World) : Prop

Definition 1.1: Given a set of alternatives ALT, ≤_ALT is the preorder over possible worlds defined as follows:

u ≤_ALT v iff {a ∈ ALT : a(u) = 1} ⊆ {a ∈ ALT : a(v) = 1}

"u makes true a subset of the alternatives that v makes true"

Equations

• (u ≤[ALT] v) = ∀ a ∈ ALT, a u → a v

def Exhaustification.ltALT {World : Type u_1} (ALT : Set (Set World)) (u v : World) : Prop

Definition 1.2: <_ALT is the strict preorder corresponding to ≤_ALT:

u <_ALT v iff u ≤_ALT v ∧ ¬(v ≤_ALT u)

"The alternatives that u makes true are a proper subset of those that v makes true."

Equations

• (u <[ALT] v) = ((u ≤[ALT] v) ∧ ¬v ≤[ALT] u)

def Exhaustification.«term_≤[_]_» : Lean.TrailingParserDescr

Equations

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

def Exhaustification.«term_<[_]_» : Lean.TrailingParserDescr

Equations

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

theorem Exhaustification.leALT_refl {World : Type u_1} (ALT : Set (Set World)) (u : World) : u ≤[ALT] u

theorem Exhaustification.leALT_trans {World : Type u_1} (ALT : Set (Set World)) (u v w : World) (huv : u ≤[ALT] v) (hvw : v ≤[ALT] w) : u ≤[ALT] w

def Exhaustification.exhMW {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) : Set World

Definition 2: Exhaustivity operator based on minimal worlds (exh_mw)

Given a set of propositions ALT and a proposition φ,

exh_mw(ALT, φ) = {u : φ(u) = 1 ∧ ¬∃v(φ(v) = 1 ∧ v <_ALT u)}

Equivalently: exh_mw(ALT, φ) = φ ∩ {u : ¬∃v(φ(v) = 1 ∧ v <_ALT u)}

"The set of φ-worlds that are minimal relative to <_ALT"

Equations

• Exhaustification.exhMW ALT φ u = (φ u ∧ ¬∃ (v : World), φ v ∧ v <[ALT] u)

def Exhaustification.IsMinimal {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) (u : World) : Prop

A world u is minimal among φ-worlds relative to <_ALT.

Definitionally equal to u ∈ exhMW ALT φ — the named version is preserved because Spector 2016's prose talks about minimal worlds independently of the exhMW operator that selects them.

Equations

• Exhaustification.IsMinimal ALT φ u = (u ∈ Exhaustification.exhMW ALT φ)

theorem Exhaustification.exhMW_entails {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) : exhMW ALT φ ⊆ φ

def Exhaustification.SetConsistent {World : Type u_1} (X : Set (Set World)) : Prop

Definition 3.1: A set of propositions X is consistent if there exists a world u in which every member of X is true.

Equations

• Exhaustification.SetConsistent X = ∃ (u : World), ∀ ψ ∈ X, ψ u

def Exhaustification.IsCompatible {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) (E : Set (Set World)) : Prop

Definition 3.2: Given a proposition φ and a set of alternatives ALT, a set of propositions E is (ALT, φ)-compatible if and only if: a) φ ∈ E b) every member of E distinct from φ is the negation of a member of ALT c) E is consistent

Equations

• Exhaustification.IsCompatible ALT φ E = (φ ∈ E ∧ (∀ ψ ∈ E, ψ = φ ∨ ∃ a ∈ ALT, ψ = aᶜ) ∧ Exhaustification.SetConsistent E)

theorem Exhaustification.IsCompatible.exists_phi_witness {World : Type u_1} {ALT : Set (Set World)} {φ : Set World} {E : Set (Set World)} (hE : IsCompatible ALT φ E) : ∃ (v : World), φ v ∧ ∀ ψ ∈ E, ψ v

A compatible set's consistency witness satisfies φ (since φ ∈ E) and every member of E. Frequently used pattern: instead of unpacking hE.2.2 into the witness and then applying it to hE.1 separately, this packages both in one obtain.

def Exhaustification.IsMCSet {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) (E : Set (Set World)) : Prop

Definition 3.3: MC_(ALT,φ)-sets

A set is maximal (ALT, φ)-compatible (MC_(ALT,φ)-set for short) if it is (ALT, φ)-compatible and is not properly included in any other (ALT, φ)-compatible set.

Equations

• Exhaustification.IsMCSet ALT φ E = (Exhaustification.IsCompatible ALT φ E ∧ ∀ (E' : Set (Set World)), Exhaustification.IsCompatible ALT φ E' → E ⊆ E' → E' ⊆ E)

def Exhaustification.IE {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) : Set (Set World)

Definition 3.4: IE_(ALT,φ) = {ψ : ψ belongs to every MC_(ALT,φ)-set}

"Note that, somewhat counter-intuitively, the set IE_(ALT,φ) is not the set of innocently excludable alternatives, but rather the set that contains φ and all the negations of innocently excludable alternatives."

Equations

• Exhaustification.IE ALT φ = {ψ : Set World | ∀ (E : Set (Set World)), Exhaustification.IsMCSet ALT φ E → ψ ∈ E}

theorem Exhaustification.phi_mem_IE {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) : φ ∈ IE ALT φ

The prejacent always lies in IE — every MC-set is (ALT, φ)-compatible and therefore contains φ. Mirrors Innocent.phi_mem_IE on the Finset side.

def Exhaustification.IsInnocentlyExcludable {World : Type u_1} (ALT : Set (Set World)) (φ a : Set World) : Prop

Definition 3.5: An alternative a is innocently excludable given ALT and φ if and only if ¬a ∈ IE_(ALT,φ).

Equations

• Exhaustification.IsInnocentlyExcludable ALT φ a = (a ∈ ALT ∧ aᶜ ∈ Exhaustification.IE ALT φ)

theorem Exhaustification.IsInnocentlyExcludable.of_full_exclusion_consistent {World : Type u_1} {ALT : Set (Set World)} {φ a : Set World} (ha : a ∈ ALT) (h_consist : ∃ (w : World), φ w ∧ ∀ b ∈ ALT, ¬b w) : IsInnocentlyExcludable ALT φ a

Sufficient condition for innocent excludability: every alternative is IE when there exists a world where φ holds and every alternative is false.

The set S = {φ} ∪ {bᶜ | b ∈ ALT} is then the unique MC-set: it is compatible by hypothesis, and every compatible set is a subset of it (by Definition 3.2(b), every element is φ or bᶜ for some b ∈ ALT). By maximality, every MC-set equals S. Since aᶜ ∈ S for every a ∈ ALT, each alternative is innocently excludable.

This is the typical situation in alternative-set scenarios where the prejacent and the negations of all alternatives are jointly satisfiable (e.g., 3-button conditional perfection paradigms).

theorem Exhaustification.IsMCSet.not_isInnocentlyExcludable_of_compl_notMem {World : Type u_1} {ALT : Set (Set World)} {φ a : Set World} {E : Set (Set World)} (hE : IsMCSet ALT φ E) (h : aᶜ ∉ E) : ¬IsInnocentlyExcludable ALT φ a

Contrapositive of IsInnocentlyExcludable's defining condition: a single witness MC-set whose complement-of-a membership fails refutes innocent excludability. Useful when a specific MC-set has been constructed by hand.

theorem Exhaustification.IsInnocentlyExcludable.of_extension_consistent {World : Type u_1} {ALT : Set (Set World)} {φ a : Set World} (ha : a ∈ ALT) (h_extend : ∀ (E : Set (Set World)), IsMCSet ALT φ E → SetConsistent (E ∪ {aᶜ})) : IsInnocentlyExcludable ALT φ a

Sufficient condition for innocent excludability via MC-set extension: if extending every MC-set with aᶜ is consistent, then aᶜ lies in every MC-set (by maximality), so a is innocently excludable.

Captures the recurring "for any MC-set E, E ∪ {aᶜ} is compatible → aᶜ ∈ E by maximality" pattern in scalar-implicature proofs. Callers provide the consistency witness; the rest of the maximality argument is discharged here.

def Exhaustification.exhIE {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) : Set World

Definition 4: Exhaustivity operator based on innocent exclusion (exh_ie)

exh_ie(ALT, φ) = {u : ∀ψ(ψ ∈ IE_(ALT,φ) → ψ(u) = 1)}

Equivalently: exh_ie(ALT, φ) = ⋂₀ IE_(ALT,φ)

Equivalently: exh_ie(ALT, φ) = φ ∧ ⋂₀ {¬a : a is a member of ALT that is innocently excludable given ALT and φ}

Equations

• Exhaustification.exhIE ALT φ u = ∀ ψ ∈ Exhaustification.IE ALT φ, ψ u

def Exhaustification.closedUnderConj {World : Type u_1} (ALT : Set (Set World)) : Prop

A set ALT is closed under conjunction if for any subset X of ALT, ⋂₀ X ∈ ALT.

(Definition 5 in Spector)

Equations

• Exhaustification.closedUnderConj ALT = ∀ X ⊆ ALT, ⋂₀ X ∈ ALT

theorem Exhaustification.ltALT_wf_of_finite {World : Type u_1} (ALT : Set (Set World)) (hfin : ALT.Finite) : WellFounded (ltALT ALT)

Well-foundedness for finite ALT: The strict ordering <_ALT is well-founded when ALT is finite.

Proof idea: For any infinite descending chain w₁ >_ALT w₂ >_ALT..., the set of true alternatives strictly increases at each step. Since ALT is finite, this cannot continue indefinitely.

theorem Exhaustification.exists_minimal_of_finite {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) (hfin : ALT.Finite) (hsat : ∃ (w : World), φ w) : ∃ (u : World), IsMinimal ALT φ u

Existence of minimal worlds for finite ALT: When ALT is finite and φ is satisfiable, there exists a minimal φ-world.

def Exhaustification.X_of_world {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) (u : World) : Set (Set World)

Definition from Section 5.3: X(u) = {φ} ∪ {¬a : a ∈ ALT ∧ a(u) = 0}

For any world u, X(u) is the set containing φ and the negations of all alternatives that are false at u.

"XALT,φ(u) = {φ} ∪ {¬a: a ∈ ALT ∧ a(u) = 0}"

Equations

• Exhaustification.X_of_world ALT φ u = {φ} ∪ {ψ : Set World | ∃ a ∈ ALT, ψ = aᶜ ∧ ¬a u}

theorem Exhaustification.ltALT_iff_X_ssubset {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) (u v : World) (hu : φ u) (hv : φ v) : (u <[ALT] v) ↔ X_of_world ALT φ v ⊂ X_of_world ALT φ u

Key equivalence (from proof of Lemma 1): For any two φ-worlds u and v: u <_ALT v ⟺ X(v) ⊊ X(u)

"The alternatives that u makes true are a proper subset of those v makes true" is equivalent to "X(v) is a proper subset of X(u)".

theorem Exhaustification.X_contains_phi {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) (u : World) : φ ∈ X_of_world ALT φ u

X(u) contains φ.

theorem Exhaustification.X_elements {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) (u : World) (ψ : Set World) (hψ : ψ ∈ X_of_world ALT φ u) : ψ = φ ∨ ∃ a ∈ ALT, ψ = aᶜ

Every element of X(u) is either φ or the negation of some alternative.

theorem Exhaustification.u_satisfies_X {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) (u : World) (hu : φ u) (ψ : Set World) : ψ ∈ X_of_world ALT φ u → ψ u

u satisfies everything in X(u).

theorem Exhaustification.X_is_compatible {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) (u : World) (hu : φ u) : IsCompatible ALT φ (X_of_world ALT φ u)

X(u) is (ALT, φ)-compatible when φ u holds.

theorem Exhaustification.minimal_iff_MCset {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) (u : World) (hu : φ u) : IsMinimal ALT φ u ↔ IsMCSet ALT φ (X_of_world ALT φ u)

Lemma 1 (Spector p.22): For any φ-world u: u is a minimal φ-world relative to <ALT ⟺ X(u) is an MC(ALT,φ)-set.

This is the key connection between the two definitions of exhaustivity.

Note: We add the explicit hypothesis (hu : φ u) since both directions require it.

theorem Exhaustification.exists_MCset_of_minimal {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) (hmin : ∃ (u : World), IsMinimal ALT φ u) : ∃ (E : Set (Set World)), IsMCSet ALT φ E

MC-set existence from minimal world existence (Spector's approach): When a minimal φ-world exists, an MC-set exists.

This follows directly from Lemma 1: if u is minimal, then X(u) is an MC-set.

theorem Exhaustification.exists_MCset {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) (hfin : ALT.Finite) (hsat : ∃ (w : World), φ w) : ∃ (E : Set (Set World)), IsMCSet ALT φ E

MC-set existence for finite ALT: When ALT is finite and φ is satisfiable, an MC-set exists.

This combines:

1. exists_minimal_of_finite: finite ALT + satisfiable φ → minimal world exists
2. exists_MCset_of_minimal: minimal world exists → MC-set exists

theorem Exhaustification.not_isInnocentlyExcludable_of_phi_subset {World : Type u_1} {ALT : Set (Set World)} {φ : Set World} (hfin : ALT.Finite) (hsat : ∃ (w : World), φ w) {a : Set World} (h_subset : φ ⊆ a) : ¬IsInnocentlyExcludable ALT φ a

A prejacent-entailed alternative is never innocently excludable (when ALT is finite and φ is satisfiable). The MC-set's consistency witness satisfies both φ (hence a by entailment) and aᶜ (since aᶜ ∈ E), contradiction.

Specializes to a = φ (the prejacent itself can never be IE) via Set.Subset.refl.

theorem Exhaustification.IE_structure {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) (hfin : ALT.Finite) (ψ : Set World) (hψ : ψ ∈ IE ALT φ) (hsat : ∃ (w : World), φ w) : ψ = φ ∨ ∃ a ∈ ALT, ψ = aᶜ

Every element of IE is either φ or aᶜ for some a ∈ ALT. This follows from the structure of compatible sets.

Note: Requires finite ALT to ensure MC-sets exist.

theorem Exhaustification.exhMW_iff_satisfies_MCset {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) (u : World) : exhMW ALT φ u ↔ ∃ (E : Set (Set World)), IsMCSet ALT φ E ∧ ∀ ψ ∈ E, ψ u

Lemma 2 (Spector p.23, Core Lemma): For every proposition φ, every set of alternatives ALT, and every world u, exh_mw(ALT, φ)(u) = 1 ⟺ there is an MC_(ALT,φ)-set X that u satisfies.

Equivalently: u is a minimal φ-world relative to <ALT ⟺ there is an MC(ALT,φ)-set X that u satisfies.

theorem Exhaustification.exhMW_eq_disj_MCsets {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) : exhMW ALT φ = {u : World | ∃ (E : Set (Set World)), IsMCSet ALT φ E ∧ ∀ ψ ∈ E, ψ u}

Lemma 3 (reformulation of Lemma 2): exh_mw(ALT, φ) = ⋃₀ {⋂₀ X : X is an MC_(ALT,φ)-set}

The minimal-worlds exhaustification is the disjunction of the conjunctions of all MC-sets.

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

Proposition 6 (Spector p.12): For any proposition φ with alternatives ALT, exh_mw(ALT, φ) entails exh_ie(ALT, φ).

Proof idea: Any world satisfying exh_mw satisfies some MC-set, hence satisfies the intersection of all MC-sets, hence satisfies IE.

theorem Exhaustification.isInnocentlyExcludable_iff_exhMW_entails_neg {World : Type u_1} (ALT : Set (Set World)) (φ a : Set World) (ha : a ∈ ALT) : IsInnocentlyExcludable ALT φ a ↔ exhMW ALT φ ⊆ aᶜ

Proposition 7 (Spector p.12): For any ALT, any a ∈ ALT, and any proposition φ, a is innocently excludable given ALT and φ if and only if exh_mw(ALT, φ) entails ¬a.

This characterizes innocent exclusion in terms of the minimal-worlds operator.

theorem Exhaustification.exhIE_eq_phi_and_exhMW_negated {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) (hfin : ALT.Finite) : exhIE ALT φ = {u : World | φ u ∧ ∀ a ∈ ALT, exhMW ALT φ ⊆ aᶜ → ¬a u}

Corollary 8 (Spector p.12): exh_ie(ALT, φ) = φ ∧ ⋂₀ {¬a : a ∈ ALT ∧ exh_mw(ALT, φ) ⊆ ¬a}

This gives an alternative characterization of exh_ie in terms of exh_mw.

Note: The backward direction requires finite ALT for IE_structure.

theorem Exhaustification.exhMW_eq_exhIE_of_closedUnderConj {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) (hclosed : closedUnderConj ALT) : exhMW ALT φ = exhIE ALT φ

Theorem 9 (Main Result, Spector p.12-13): For any φ and any ALT, if ALT is closed under conjunction, then

exh_mw(ALT, φ) = exh_ie(ALT, φ)

Proof outline (from Section 5.4): Since exh_mw always entails exh_ie (Prop 6), we need to show exh_ie ⊆ exh_mw when ALT is closed under conjunction.

Suppose exh_mw(φ)(u) = 0 but φ(u) = 1. We must show exh_ie(φ)(u) = 0.

Let A = {a ∈ ALT : a(u) = 1}. Since u is not minimal, every MC-set contains a negation of some member of A. Consider ⋂₀ A. Since every MC-set has a member whose negation is in A, ⋂₀ A is false in every world satisfying an MC-set. Therefore ¬(⋂₀ A) is consistent with every MC-set.

Since ALT is closed under conjunction, ⋂₀ A ∈ ALT. Since ¬(⋂₀ A) is consistent with every MC-set and MC-sets are maximal, ¬(⋂₀ A) ∈ IE. But (⋂₀ A)(u) = 1, so u fails to satisfy IE, hence exh_ie(φ)(u) = 0.

theorem Exhaustification.neg_bigDisj_iff {World : Type u_1} (X : Set (Set World)) (w : World) : (⋃₀ X)ᶜ w ↔ ∀ a ∈ X, aᶜ w

De Morgan for big disjunction: ¬(⋃₀ X) at w iff ∀ a ∈ X, ¬a at w

theorem Exhaustification.subset_disjClosure {World : Type u_1} (ALT ALT' : Set (Set World)) (h : ALT' = {p : Set World | ∃ X ⊆ ALT, p = ⋃₀ X}) : ALT ⊆ ALT'

The disjunction closure contains the original set (via singleton disjunctions).

theorem Exhaustification.mem_disjClosure_iff {World : Type u_1} (ALT ALT' : Set (Set World)) (h : ALT' = {p : Set World | ∃ X ⊆ ALT, p = ⋃₀ X}) (p : Set World) : p ∈ ALT' ↔ ∃ X ⊆ ALT, p = ⋃₀ X

Every element of the disjunction closure is a disjunction of ALT elements.

theorem Exhaustification.leALT_disjClosure_eq {World : Type u_1} (ALT ALT' : Set (Set World)) (h : ALT' = {p : Set World | ∃ X ⊆ ALT, p = ⋃₀ X}) (u v : World) : (u ≤[ALT] v) ↔ u ≤[ALT'] v

Key lemma: The preorder ≤_ALT is unchanged by disjunction closure.

If ALT' is the disjunction closure of ALT, then u ≤{ALT} v ↔ u ≤{ALT'} v.

Proof: If a disjunction (⋃₀ X) is true at u where X ⊆ ALT, then some b ∈ X is true at u. If u ≤_{ALT} v, then b is true at v, so (⋃₀ X) is true at v.

theorem Exhaustification.ltALT_disjClosure_eq {World : Type u_1} (ALT ALT' : Set (Set World)) (h : ALT' = {p : Set World | ∃ X ⊆ ALT, p = ⋃₀ X}) (u v : World) : (u <[ALT] v) ↔ u <[ALT'] v

Corollary: The strict ordering <_ALT is unchanged by disjunction closure.

theorem Exhaustification.exhMW_disjClosure_eq {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) (ALT' : Set (Set World)) (h : ALT' = {p : Set World | ∃ X ⊆ ALT, p = ⋃₀ X}) : exhMW ALT φ = exhMW ALT' φ

Corollary: exh_mw is unchanged by disjunction closure.

theorem Exhaustification.exhIE_disjClosure_eq {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) (hfin : ALT.Finite) (ALT' : Set (Set World)) (h : ALT' = {p : Set World | ∃ X ⊆ ALT, p = ⋃₀ X}) : exhIE ALT φ = exhIE ALT' φ

Theorem 10 (Spector p.13): For any proposition φ and any alternative set ALT, exh_ie(ALT, φ) = exh_ie(ALT∨, φ)

where ALT∨ is the closure of ALT under disjunction.

"Closing the alternatives under disjunction (but crucially not conjunction) is vacuous for exh_ie."

Proof strategy: Use Corollary 8's characterization: exhIE ALT φ ≡ₚ λ u => φ u ∧ ∀ a ∈ ALT, (exhMW ALT φ ⊆ aᶜ) → ¬(a u)

Since exhMW is unchanged by disjunction closure, we just need to check that the extra conditions for ALT' (disjunctions) are implied by the ALT conditions.

theorem Exhaustification.exhMW_eq_exhIE_of_disjClosure_closedUnderConj {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) (hfin : ALT.Finite) (hcond : closedUnderConj {p : Set World | ∃ Y ⊆ ALT, p = ⋃₀ Y}) : exhMW ALT φ = exhIE ALT φ

Corollary 11 (Spector p.13): For any proposition φ and any alternative set ALT, if ALT∨ = ALT∨∧, then exh_mw(ALT, φ) = exh_ie(ALT, φ).

"If the closure of ALT under disjunction is closed under conjunction, applying exh_mw and exh_ie give rise to equivalent results."