Innocent exclusion

A set of alternatives is a consistent exclusion when denying all of them is consistent with the prejacent. Fox calls an alternative innocently excludable when it belongs to every maximal consistent exclusion, and the exhaustifier exhIE asserts the prejacent and denies the innocently excludable alternatives. The maximal consistent exclusions are the sets of alternatives false at the minimal worlds of Alternatives, so an alternative is innocently excludable iff it fails at every minimal world. Hence minimal-world exhaustification entails innocent exclusion, with equality when the alternatives are closed under conjunction, and closing them under disjunction changes neither exhaustifier. Innocent exclusion is exh with its alternative set selected by innocent excludability.

Main definitions

• IsConsistentExclusion: a set of alternatives whose joint denial is consistent with the prejacent.
• IsInnocentlyExcludable, exhIE: membership in every maximal consistent exclusion, and the exhaustifier denying such alternatives.

Main results

• maximal_sdiff_satisfied_iff, Maximal.exists_eq_sdiff_satisfied: the maximal consistent exclusions are the sets of alternatives false at a minimal world.
• isInnocentlyExcludable_iff_exhMW_subset_compl
• exhIE_eq_exh, exhIE_eq_exh_of_nonempty, exhIE_eq_sdiff_of_maximal_unique
• exh_nonempty_iff, mem_exhIE_iff_subset_sUnion: exh is consistent iff some prejacent world verifies the least set of alternatives, and exhIE keeps the worlds verifying only alternatives in a minimal verified set
• exhMW_eq_exhIE_of_infClosed, exhIE_sUnion_image_powerset

References

• [Fox07]
• [Spe16]

Consistent exclusions

def Exhaustification.IsConsistentExclusion {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) (X : Set (Set World)) : Prop

A set of alternatives is a consistent exclusion when denying all of them is consistent with the prejacent.

Equations

• Exhaustification.IsConsistentExclusion ALT φ X = (X ⊆ ALT ∧ (φ \ ⋃₀ X).Nonempty)

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

An alternative is innocently excludable when it belongs to every maximal consistent exclusion.

Equations

• Exhaustification.IsInnocentlyExcludable ALT φ a = (a ∈ ALT ∧ ∀ (X : Set (Set World)), Maximal (Exhaustification.IsConsistentExclusion ALT φ) X → a ∈ X)

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

The innocent-exclusion exhaustifier asserts the prejacent and denies every innocently excludable alternative.

Equations

• Exhaustification.exhIE ALT φ = {u : World | u ∈ φ ∧ ∀ (a : Set World), Exhaustification.IsInnocentlyExcludable ALT φ a → u ∉ a}

theorem Exhaustification.mem_exhIE_iff {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) {u : World} : u ∈ exhIE ALT φ ↔ u ∈ φ ∧ ∀ (a : Set World), IsInnocentlyExcludable ALT φ a → u ∉ a

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

Exhaustification entails its prejacent.

theorem Exhaustification.IsConsistentExclusion.mono {World : Type u_1} {ALT : Set (Set World)} {φ : Set World} {X Y : Set (Set World)} (hY : IsConsistentExclusion ALT φ Y) (hXY : X ⊆ Y) : IsConsistentExclusion ALT φ X

A subset of a consistent exclusion is a consistent exclusion.

theorem Exhaustification.IsInnocentlyExcludable.of_forall_maximal {World : Type u_1} {ALT : Set (Set World)} {φ a : Set World} (ha : a ∈ ALT) (h : ∀ (X : Set (Set World)), Maximal (IsConsistentExclusion ALT φ) X → (φ \ ⋃₀ insert a X).Nonempty) : IsInnocentlyExcludable ALT φ a

An alternative belonging to every maximal consistent exclusion it extends consistently is innocently excludable.

theorem Exhaustification.Maximal.not_isInnocentlyExcludable {World : Type u_1} {ALT : Set (Set World)} {φ : Set World} {X : Set (Set World)} {a : Set World} (hX : Maximal (IsConsistentExclusion ALT φ) X) (ha : a ∉ X) : ¬IsInnocentlyExcludable ALT φ a

An alternative missing from some maximal consistent exclusion is not innocently excludable.

theorem Exhaustification.IsInnocentlyExcludable.of_forall_subset_or_notMem {World : Type u_1} {ALT : Set (Set World)} {φ a : Set World} {w : World} (ha : a ∈ ALT) (hw : w ∈ φ) (hwa : w ∉ a) (h : ∀ b ∈ ALT, φ ⊆ b ∨ w ∉ b) : IsInnocentlyExcludable ALT φ a

An alternative failing at a prejacent world that falsifies every alternative the prejacent does not entail is innocently excludable, since that world witnesses every maximal consistent exclusion together with it.

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

Every alternative is innocently excludable when some prejacent world falsifies them all.

theorem Exhaustification.IsInnocentlyExcludable.exhIE_subset_compl {World : Type u_1} {ALT : Set (Set World)} {φ a : Set World} (h : IsInnocentlyExcludable ALT φ a) : exhIE ALT φ ⊆ aᶜ

Exhaustification denies an innocently excludable alternative.

theorem Exhaustification.IsInnocentlyExcludable.exhIE_subset_compl_exhIE {World : Type u_1} {ALT : Set (Set World)} {φ a : Set World} (h : IsInnocentlyExcludable ALT φ a) : exhIE ALT φ ⊆ (exhIE ALT a)ᶜ

Exhaustification denies the exhaustification of an innocently excludable alternative.

Maximal consistent exclusions and minimal worlds

theorem Exhaustification.mem_sdiff_satisfied {World : Type u_1} {ALT : Set (Set World)} {u : World} {b : Set World} : b ∈ ALT \ Preorder.satisfied (fun (x1 : World) (x2 : Set World) => x1 ∈ x2) ALT u ↔ b ∈ ALT ∧ u ∉ b

The alternatives a world does not verify are those false there.

theorem Exhaustification.isConsistentExclusion_sdiff_satisfied {World : Type u_1} {ALT : Set (Set World)} {φ : Set World} {u : World} (hu : u ∈ φ) : IsConsistentExclusion ALT φ (ALT \ Preorder.satisfied (fun (x1 : World) (x2 : Set World) => x1 ∈ x2) ALT u)

theorem Exhaustification.IsConsistentExclusion.subset_sdiff_satisfied {World : Type u_1} {ALT : Set (Set World)} {φ : Set World} {X : Set (Set World)} (hX : IsConsistentExclusion ALT φ X) {u : World} (hu : u ∉ ⋃₀ X) : X ⊆ ALT \ Preorder.satisfied (fun (x1 : World) (x2 : Set World) => x1 ∈ x2) ALT u

A consistent exclusion lies among the alternatives false at any prejacent world witnessing it.

theorem Exhaustification.maximal_sdiff_satisfied_iff {World : Type u_1} {ALT : Set (Set World)} {φ : Set World} {u : World} (hu : u ∈ φ) : Maximal (IsConsistentExclusion ALT φ) (ALT \ Preorder.satisfied (fun (x1 : World) (x2 : Set World) => x1 ∈ x2) ALT u) ↔ IsMinimal ALT φ u

The alternatives false at a prejacent world form a maximal consistent exclusion iff the world is minimal.

theorem Exhaustification.Maximal.exists_eq_sdiff_satisfied {World : Type u_1} {ALT : Set (Set World)} {φ : Set World} {X : Set (Set World)} (hX : Maximal (IsConsistentExclusion ALT φ) X) : ∃ (u : World), IsMinimal ALT φ u ∧ X = ALT \ Preorder.satisfied (fun (x1 : World) (x2 : Set World) => x1 ∈ x2) ALT u

Every maximal consistent exclusion is the set of alternatives false at a minimal world.

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

An alternative is innocently excludable iff it fails at every minimal world.

theorem Exhaustification.exists_maximal_isConsistentExclusion {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) (hfin : ALT.Finite) (hsat : φ.Nonempty) : ∃ (X : Set (Set World)), Maximal (IsConsistentExclusion ALT φ) X

A satisfiable prejacent over finitely many alternatives has a maximal consistent exclusion.

theorem Exhaustification.not_isInnocentlyExcludable_of_phi_subset {World : Type u_1} {ALT : Set (Set World)} {φ : Set World} (hfin : ALT.Finite) (hsat : φ.Nonempty) {a : Set World} (h : φ ⊆ a) : ¬IsInnocentlyExcludable ALT φ a

An alternative entailed by a satisfiable prejacent is never innocently excludable.

theorem Exhaustification.mem_exhIE_of_forall_subset_or_notMem {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) (hfin : ALT.Finite) {u : World} (hu : u ∈ φ) (h : ∀ a ∈ ALT, φ ⊆ a ∨ u ∉ a) : u ∈ exhIE ALT φ

A prejacent world falsifying every alternative the prejacent does not entail survives exhaustification.

theorem Exhaustification.exhIE_eq_of_iff {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) {P : Set World → Prop} (h : ∀ q ∈ ALT, IsInnocentlyExcludable ALT φ q ↔ P q) : exhIE ALT φ = {w : World | w ∈ φ ∧ ∀ q ∈ ALT, P q → w ∉ q}

With the innocently excludable alternatives characterized, the exhaustifier denies exactly them.

theorem Exhaustification.exhIE_eq_exh {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) (hfin : ALT.Finite) : exhIE ALT φ = exh {a : Set World | IsInnocentlyExcludable ALT φ a} φ

Innocent exclusion is exhaustification over the innocently excludable alternatives.

theorem Exhaustification.exhIE_preimage_image {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) {β : Type u_2} {f : World → β} (hφ : f ⁻¹' f '' φ = φ) (hALT : ∀ a ∈ ALT, f ⁻¹' f '' a = a) : f ⁻¹' f '' exhIE ALT φ = exhIE ALT φ

If the prejacent and the alternatives are unions of fibres of f, so is the exhaustified prejacent.

theorem Exhaustification.exhIE_eq_self_iff {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) : exhIE ALT φ = φ ↔ ∀ (a : Set World), IsInnocentlyExcludable ALT φ a → Disjoint φ a

Exhaustification is vacuous iff every innocently excludable alternative is already incompatible with the prejacent.

theorem Exhaustification.exhIE_empty {World : Type u_1} (φ : Set World) : exhIE ∅ φ = φ

Without alternatives, exhaustification is vacuous.

theorem Exhaustification.exhIE_subset_exhIE {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) {ALT' : Set (Set World)} (h : ∀ (q : Set World), IsInnocentlyExcludable ALT' φ q → IsInnocentlyExcludable ALT φ q) : exhIE ALT φ ⊆ exhIE ALT' φ

Exhaustification is antitone in the innocently excludable alternatives, more of them giving a stronger result.

Innocent exclusion and minimal worlds

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

Minimal-world exhaustification entails innocent exclusion.

theorem Exhaustification.exhIE_univ {World : Type u_1} (φ : Set World) : exhIE Set.univ φ = φ

Exhaustification against all propositions is vacuous.

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

A prejacent world at which only entailed alternatives hold is minimal.

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

Denying every alternative the prejacent does not entail is at least as strong as innocent exclusion.

theorem Exhaustification.exhIE_eq_sdiff_of_maximal_unique {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) {X₀ : Set (Set World)} (h₀ : Maximal (IsConsistentExclusion ALT φ) X₀) (huniq : ∀ (X : Set (Set World)), Maximal (IsConsistentExclusion ALT φ) X → X = X₀) : exhIE ALT φ = φ \ ⋃₀ X₀

With a unique maximal consistent exclusion, innocent exclusion denies exactly its members.

theorem Exhaustification.exhIE_eq_exh_of_nonempty {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) (h : (exh ALT φ).Nonempty) : exhIE ALT φ = exh ALT φ

When the prejacent is consistent with the denial of every alternative it does not entail, innocent exclusion denies them all ([Fox07]).

theorem Exhaustification.exhIE_eq_self_of_forall {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) (h : ∀ a ∈ ALT, (φ ∩ a).Nonempty → φ ⊆ a) : exhIE ALT φ = φ

Exhaustification is vacuous when every alternative is entailed by the prejacent or incompatible with it.

theorem Exhaustification.exhIE_singleton_self {World : Type u_1} (φ : Set World) : exhIE {φ} φ = φ

Against itself alone, exhaustification is vacuous.

theorem Exhaustification.exhIE_pair_sdiff {World : Type u_1} (φ : Set World) {d : Set World} (hne : (φ \ d).Nonempty) : exhIE {φ, d} φ = φ \ d

Against one alternative that some prejacent world falsifies, exhaustification denies exactly it.

theorem Exhaustification.not_isInnocentlyExcludable_of_subset_union {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) (hfin : ALT.Finite) {p q : Set World} (hp : p ∈ ALT) (hq : q ∈ ALT) (hcov : φ ⊆ p ∪ q) (hne : (φ \ q).Nonempty) : ¬IsInnocentlyExcludable ALT φ p

An alternative that covers the prejacent together with a second alternative some prejacent world falsifies is not innocently excludable, since negating both contradicts the prejacent and a minimal world below that prejacent world verifies the first.

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

Innocent exclusion denies exactly the alternatives failing at every minimal world.

theorem Exhaustification.IsMinimalCover.isInnocentlyExcludable_iff {World : Type u_1} {ALT : Set (Set World)} {φ M : Set World} (hM : IsMinimalCover ALT φ M) {a : Set World} (ha : a ∈ ALT) : IsInnocentlyExcludable ALT φ a ↔ ∀ v ∈ M, v ∉ a

An alternative is innocently excludable iff it fails at every representative minimal world.

theorem Exhaustification.IsMinimalCover.exhIE_eq {World : Type u_1} {ALT : Set (Set World)} {φ M : Set World} (hM : IsMinimalCover ALT φ M) : exhIE ALT φ = {u : World | u ∈ φ ∧ ∀ a ∈ ALT, (∀ v ∈ M, v ∉ a) → u ∉ a}

Exhaustification denies exactly the alternatives false at every representative minimal world.

Closure under conjunction and disjunction

theorem Exhaustification.exhMW_eq_exhIE_of_infClosed {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) (hfin : ALT.Finite) (hinf : InfClosed ALT) : exhMW ALT φ = exhIE ALT φ

With finitely many alternatives closed under conjunction the two exhaustifiers coincide. A prejacent world above another verifies the conjunction of the alternatives true at it, which every minimal world falsifies.

theorem Exhaustification.leALT_sUnion_image_powerset {World : Type u_1} (ALT : Set (Set World)) {u v : World} : leALT (Set.sUnion '' 𝒫 ALT) u v ↔ leALT ALT u v

The order on worlds is unchanged by closing the alternatives under disjunction.

theorem Exhaustification.exhMW_sUnion_image_powerset {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) : exhMW (Set.sUnion '' 𝒫 ALT) φ = exhMW ALT φ

Minimal-world exhaustification is unchanged by closing the alternatives under disjunction.

theorem Exhaustification.exhIE_sUnion_image_powerset {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) : exhIE (Set.sUnion '' 𝒫 ALT) φ = exhIE ALT φ

Innocent exclusion is unchanged by closing the alternatives under disjunction, since a disjunction fails at every minimal world iff each disjunct does.

theorem Exhaustification.exhMW_eq_exhIE_of_infClosed_sUnion_image {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) (hfin : ALT.Finite) (hinf : InfClosed (Set.sUnion '' 𝒫 ALT)) : exhMW ALT φ = exhIE ALT φ

When the disjunctive closure of finitely many alternatives is closed under conjunction the two exhaustifiers coincide.

Verified alternatives

Each operator reads a world only through the alternatives it verifies, and the prejacent only through the sets of alternatives its worlds verify. exh keeps the worlds verifying the least such set, exhMW those verifying a minimal one (mem_exhMW_iff_minimal), and exhIE those verifying only alternatives that some minimal verified set contains.

theorem Exhaustification.mem_exh_iff_isLeast {World : Type u_1} {ALT : Set (Set World)} {φ : Set World} {w : World} : w ∈ exh ALT φ ↔ w ∈ φ ∧ IsLeast (Preorder.satisfied (fun (x1 : World) (x2 : Set World) => x1 ∈ x2) ALT '' φ) (Preorder.satisfied (fun (x1 : World) (x2 : Set World) => x1 ∈ x2) ALT w)

Exhaustification keeps the prejacent worlds verifying the least set of alternatives that a prejacent world verifies.

theorem Exhaustification.exh_nonempty_iff {World : Type u_1} {ALT : Set (Set World)} {φ : Set World} : (exh ALT φ).Nonempty ↔ ∃ (P : Set (Set World)), IsLeast (Preorder.satisfied (fun (x1 : World) (x2 : Set World) => x1 ∈ x2) ALT '' φ) P

Exhaustification is consistent iff the sets of alternatives the prejacent worlds verify have a least element.

theorem Exhaustification.isInnocentlyExcludable_iff_forall_minimal {World : Type u_1} {ALT : Set (Set World)} {φ a : Set World} (ha : a ∈ ALT) : IsInnocentlyExcludable ALT φ a ↔ ∀ (P : Set (Set World)), Minimal (fun (x : Set (Set World)) => x ∈ Preorder.satisfied (fun (x1 : World) (x2 : Set World) => x1 ∈ x2) ALT '' φ) P → a ∉ P

An alternative is innocently excludable iff no minimal verified set contains it.

theorem Exhaustification.mem_exhIE_iff_subset_sUnion {World : Type u_1} {ALT : Set (Set World)} {φ : Set World} {w : World} : w ∈ exhIE ALT φ ↔ w ∈ φ ∧ Preorder.satisfied (fun (x1 : World) (x2 : Set World) => x1 ∈ x2) ALT w ⊆ ⋃₀ {P : Set (Set World) | Minimal (fun (x : Set (Set World)) => x ∈ Preorder.satisfied (fun (x1 : World) (x2 : Set World) => x1 ∈ x2) ALT '' φ) P}

Innocent exclusion keeps the prejacent worlds verifying only alternatives that some minimal verified set contains.