Innocence as naturality

Fox motivates innocent exclusion by arbitrariness: each maximal consistent exclusion could be carried out on its own, so excluding an alternative outside one of them would choose arbitrarily among them, and only the alternatives in all of them are excluded non-arbitrarily. Bar-Lev and Fox define innocent inclusion the same way from the maximal consistent inclusions. Reading non-arbitrary as natural, both are theorems: over finitely many alternatives, the innocently excludable alternatives are the greatest set a natural consistent rule selects from the maximal consistent exclusions, and the innocently includable ones the greatest it selects from the maximal consistent inclusions.

Main statements

• Exhaustification.isGreatest_setOf_isInnocentlyExcludable
• Exhaustification.isGreatest_II

References

• [Fox07]
• [BLF20]

theorem Exhaustification.isGreatest_setOf_isInnocentlyExcludable {World : Type u} {ALT : Set (Set World)} {φ : Set World} (hfin : ALT.Finite) (hsat : φ.Nonempty) : IsGreatest ((fun (F : (A : Type u) → Set (Set A) → Set A) => F (Set World) {X : Set (Set World) | Maximal (IsConsistentExclusion ALT φ) X}) '' {F : (A : Type u) → Set (Set A) → Set A | Set.IsNaturalSelection F ∧ Set.IsConsistentSelection F}) {a : Set World | IsInnocentlyExcludable ALT φ a}

Innocent exclusion is the greatest natural consistent exclusion. Over finitely many alternatives and a satisfiable prejacent, the innocently excludable alternatives are the greatest set a natural consistent rule selects from the maximal consistent exclusions.

theorem Exhaustification.isGreatest_II {World : Type u} {ALT : Set (Set World)} {φ : Set World} (hfin : ALT.Finite) (hne : (exhIE ALT φ).Nonempty) : IsGreatest ((fun (F : (A : Type u) → Set (Set A) → Set A) => F (Set World) {R : Set (Set World) | Maximal (IsConsistentInclusion ALT φ) R}) '' {F : (A : Type u) → Set (Set A) → Set A | Set.IsNaturalSelection F ∧ Set.IsConsistentSelection F}) (II ALT φ)

Innocent inclusion is the greatest natural consistent inclusion. Over finitely many alternatives, when innocent exclusion is consistent the innocently includable alternatives are the greatest set a natural consistent rule selects from the maximal consistent inclusions.