Innocent Inclusion @cite{bar-lev-fox-2020}

From @cite{bar-lev-fox-2020}, Definition (51):

II(p, C) = ∩{C'' ⊆ C : C'' is maximal s.t. {r : r ∈ C''} ∪ {p} ∪ {¬q : q ∈ IE(p,C)} is consistent}

After computing IE, find all maximal subsets of alternatives that can consistently be assigned TRUE (given that IE alternatives are false). An alternative is innocently includable iff it appears in ALL such maximal sets.

Cell identification

@cite{bar-lev-fox-2020} eq. (20) + (27) + footnote 21. The cell of Partition(ALT) containing prejacent φ is the strongest proposition that assigns a definite truth value to every alternative in ALT: the prejacent, the negation of every IE-excludable alternative, and the truth of every non-excludable alternative. When the cell is consistent (= satisfiable at some world), exhIEII collapses onto it. When inconsistent (the simple-disjunction case {a∨b, a, b, a∧b}), exhIEII does no enrichment beyond exhIE.

def Exhaustification.IsIICompatible {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) (R : Set (Set World)) : Prop

Definition (II-compatible set): A set of propositions R is (ALT, φ, IE)-compatible for inclusion if:

• R ⊆ ALT
• {r : r ∈ R} ∪ {φ} ∪ {¬q : q ∈ IE(ALT, φ)} is consistent.

Equations

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

def Exhaustification.IsMISet {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) (R : Set (Set World)) : Prop

Definition (MI-set): Maximal II-compatible set.

Equations

• Exhaustification.IsMISet ALT φ R = (Exhaustification.IsIICompatible ALT φ R ∧ ∀ (R' : Set (Set World)), Exhaustification.IsIICompatible ALT φ R' → R ⊆ R' → R' ⊆ R)

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

Definition (II): II(ALT, φ) = {r ∈ ALT : r belongs to every MI-set}.

Equations

• Exhaustification.II ALT φ = {r : Set World | r ∈ ALT ∧ ∀ (R : Set (Set World)), Exhaustification.IsMISet ALT φ R → r ∈ R}

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

An alternative a is innocently includable given ALT and φ iff a ∈ II(ALT, φ).

Equations

• Exhaustification.IsInnocentlyIncludable ALT φ a = (a ∈ Exhaustification.II ALT φ)

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

Definition (Exh^{IE+II}): The exhaustivity operator with both IE and II.

⟦Exh^{IE+II}⟧(ALT)(φ)(w) ⇔ φ(w) ∧ ∀q ∈ IE(ALT,φ)[¬q(w)] ∧ ∀r ∈ II(ALT,φ)[r(w)].

Bar-Lev & Fox's key operator that derives free choice.

Equations

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

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

The non-IE alternatives: members of ALT not innocently excludable. @cite{bar-lev-fox-2020} (the C \ IE(p,C) of paper eq. 20).

Equations

• Exhaustification.nonExcludable ALT φ = {r : Set World | r ∈ ALT ∧ ¬Exhaustification.IsInnocentlyExcludable ALT φ r}

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

The cell of Partition(ALT) containing prejacent φ. @cite{bar-lev-fox-2020} eq. (20): Cell(p, C) = p ∧ ⋂₀ {¬q : q ∈ IE(p, C)} ∧ ⋂₀ (C \ IE(p, C)).

Equations

• Exhaustification.cell ALT φ w = (φ w ∧ (∀ (q : Set World), Exhaustification.IsInnocentlyExcludable ALT φ q → ¬q w) ∧ ∀ r ∈ Exhaustification.nonExcludable ALT φ, r w)

@[simp]

theorem Exhaustification.mem_nonExcludable {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) {r : Set World} : r ∈ nonExcludable ALT φ ↔ r ∈ ALT ∧ ¬IsInnocentlyExcludable ALT φ r

Membership in nonExcludable unfolds to r ∈ ALT plus non-excludability.

theorem Exhaustification.isIICompatible_subset_nonExcludable {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) {R : Set (Set World)} (hR : IsIICompatible ALT φ R) : R ⊆ nonExcludable ALT φ

Every II-compatible set consists of non-excludable alternatives.

theorem Exhaustification.isIICompatible_nonExcludable_of_cell_nonempty {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) (h : (cell ALT φ).Nonempty) : IsIICompatible ALT φ (nonExcludable ALT φ)

When the cell is consistent (nonempty as a set of worlds), nonExcludable is itself II-compatible.

theorem Exhaustification.II_eq_nonExcludable_of_cell_nonempty {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) (h : (cell ALT φ).Nonempty) : II ALT φ = nonExcludable ALT φ

Cell identification (@cite{bar-lev-fox-2020} footnote 21): when the cell is consistent, the unique MI-set is nonExcludable, hence II = nonExcludable.

theorem Exhaustification.exhIEII_eq_cell_of_cell_nonempty {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) (h : (cell ALT φ).Nonempty) : exhIEII ALT φ = cell ALT φ

Cell identification (@cite{bar-lev-fox-2020} eq. 27): when the cell is consistent, exhIEII coincides with cell.

theorem Exhaustification.mem_II_of_cell_witness {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) {target : Set World} (htarget_alt : target ∈ ALT) (w : World) (hwitness : cell ALT φ w) (htarget : target w) : target ∈ II ALT φ

Sufficient condition for II membership via a cell witness world.

Given any world w that witnesses cell consistency (satisfies the prejacent, falsifies all IE-excludable alternatives, and verifies all non-excludable alternatives), every alternative true at w is innocently includable.

The abstract content of @cite{bar-lev-fox-2020}'s free-choice derivation: each disjunct is true at the "separately-A-B" world, which is the cell witness for Alt(◇(a∨b)).

Cell-witness factorization: from cell verdict to exhIEII consequences

The headline theorem of cell-identification (@cite{bar-lev-fox-2020} §3.3): once a cell witness is exhibited, exhIEII factors through the per-alternative verdict at the witness. In abstract terms, every alternative that holds at a cell witness is in II, hence asserted by exhIEII; every innocently excludable alternative is in IE, hence negated by exhIEII. The two corollaries below package these patterns as substrate-level theorems consumable by any Exh^{IE+II}-based study (basic FC, universal FC, SDA via Innocent Inclusion, etc.).

theorem Exhaustification.exhIEII_implies_cell_witnessed_alt {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) {target : Set World} (htarget_alt : target ∈ ALT) (w : World) (hwitness : cell ALT φ w) (htarget : target w) (u : World) : exhIEII ALT φ u → target u

Substrate-level cell-witness factorization (positive side). Any alternative that holds at a cell witness is entailed by exhIEII at every world. Composition of mem_II_of_cell_witness with the hII projection of exhIEII.

theorem Exhaustification.exhIEII_implies_cell_witnessed_alts {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) (targets : List (Set World)) (h_in_alt : ∀ t ∈ targets, t ∈ ALT) (w : World) (hwitness : cell ALT φ w) (h_witness : ∀ t ∈ targets, t w) (u : World) : exhIEII ALT φ u → ∀ t ∈ targets, t u

Substrate-level cell-witness factorization (list / multi-target). Given a cell witness and a list of alternatives all true at the witness, exhIEII jointly entails every list member. The cross-mechanism agreement template: any per-alternative-conjunction operator (e.g., @cite{santorio-2018}'s sdaEval) factors through exhIEII whenever the per-alternatives hold at a shared cell witness.

theorem Exhaustification.exhIEII_negates_excludable {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) {target : Set World} (h_ie : IsInnocentlyExcludable ALT φ target) (u : World) : exhIEII ALT φ u → ¬target u

Substrate-level cell-witness factorization (negation side). Any innocently excludable alternative is negated by exhIEII. Definitional unfolding of exhIEII's IE projection — named for structural parallel with the positive side.

theorem Exhaustification.not_isInnocentlyExcludable_of_cell_witness {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) {target : Set World} (w : World) (hwitness : cell ALT φ w) (htarget : target w) : ¬IsInnocentlyExcludable ALT φ target

Cell-witness refutes IE-ness. Any alternative true at the cell witness is NOT innocently excludable. Direct contrapositive of the cell predicate's IE clause: the cell witness falsifies every IE alternative, so an alternative true at the witness cannot be IE. Avoids constructing MC-set witnesses for non-IE-ness proofs in study files: once the cell is established, every cell-witnessed alternative is non-IE by this 1-line corollary.