Bar-Lev & Fox (2020) — Free Choice via Innocent Inclusion

@cite{bar-lev-fox-2020} @cite{fox-2007} @cite{spector-2016}

Worked example of @cite{bar-lev-fox-2020} "Free choice, simplification, and Innocent Inclusion" (Natural Language Semantics 28:175–223) over a five-world toy modal model.

What this file does

The abstract theory of Innocent Exclusion (IE), Innocent Inclusion (II), the cell-of-the-induced-partition (cell), and the cell-identification theorem mem_II_of_cell_witness lives in Theories/Semantics/Exhaustification/Operators/Basic.lean. This file instantiates that theory on a small FCWorld and verifies the paper's headline empirical prediction:

Exh^{IE+II}(◇(a ∨ b)) ⊨ ◇a ∧ ◇b

The contrast with simple disjunction (where the alternative set IS closed under conjunction and free choice does not arise) is captured via a parallel DisjWorld toy + simpleALT and simple_has_conjunction.

Why the cell-identification API matters

In the paper, the move from "exhaustification of a disjunction" to "free choice" is enabled by a structural property of the alternative set: the pairwise conjunction of the disjunctive alternatives ◇a ∩ ◇b is NOT a member of Alt(◇(a∨b)) (paper eqn 13b p. 182). The cell of the partition induced by the alternatives is therefore consistent and identified by Exh^{IE+II}. The free choice proof is a one-line corollary of mem_II_of_cell_witness once a witness world for the cell is exhibited (the separatelyAB world, where each disjunct is individually possible but not jointly).

On the Exh^{IE+II} definition (paper §3, eqn 24-25 pp. 187-188)

Exh^{IE+II} strengthens the prejacent with two operations:

1. Innocent Exclusion (IE) — the intersection of maximal subsets of alternatives that can consistently be assigned false together with the prejacent. Members are negated.
2. Innocent Inclusion (II) — the intersection of maximal subsets of alternatives that can consistently be assigned true together with the prejacent AND the IE negations from step 1. Members are asserted.

II is not "all non-IE alternatives" (a popular but incorrect gloss). The non-IE = II coincidence in the basic FC case is a derived fact (paper §3.3.3) once the cell is identified, not a definition. The substrate Theories/Semantics/Exhaustification/Operators/Basic.lean follows the paper's actual definitions.

inductive Phenomena.Modality.Studies.BarLevFox2020.FCWorld : Type

Possible worlds for free choice: each represents a configuration of which disjuncts are individually or jointly permitted.

The separatelyAB world is the cell witness: each disjunct is individually permitted but they are not jointly permitted. This world distinguishes ◇a ∧ ◇b from ◇(a ∧ b) and is the cornerstone of @cite{bar-lev-fox-2020}'s free-choice derivation.

• neither : FCWorld
• onlyA : FCWorld
• onlyB : FCWorld
• both : FCWorld
• separatelyAB : FCWorld

@[implicit_reducible]

instance Phenomena.Modality.Studies.BarLevFox2020.instDecidableEqFCWorld : DecidableEq FCWorld

Equations

• Phenomena.Modality.Studies.BarLevFox2020.instDecidableEqFCWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Modality.Studies.BarLevFox2020.instReprFCWorld.repr : FCWorld → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Modality.Studies.BarLevFox2020.instReprFCWorld : Repr FCWorld

Equations

• Phenomena.Modality.Studies.BarLevFox2020.instReprFCWorld = { reprPrec := Phenomena.Modality.Studies.BarLevFox2020.instReprFCWorld.repr }

def Phenomena.Modality.Studies.BarLevFox2020.instInhabitedFCWorld.default : FCWorld

Equations

• Phenomena.Modality.Studies.BarLevFox2020.instInhabitedFCWorld.default = Phenomena.Modality.Studies.BarLevFox2020.FCWorld.neither

@[implicit_reducible]

instance Phenomena.Modality.Studies.BarLevFox2020.instInhabitedFCWorld : Inhabited FCWorld

Equations

• Phenomena.Modality.Studies.BarLevFox2020.instInhabitedFCWorld = { default := Phenomena.Modality.Studies.BarLevFox2020.instInhabitedFCWorld.default }

def Phenomena.Modality.Studies.BarLevFox2020.permA : Set FCWorld

◇a — a is permitted at the world.

Equations

• Phenomena.Modality.Studies.BarLevFox2020.permA Phenomena.Modality.Studies.BarLevFox2020.FCWorld.neither = False
• Phenomena.Modality.Studies.BarLevFox2020.permA Phenomena.Modality.Studies.BarLevFox2020.FCWorld.onlyA = True
• Phenomena.Modality.Studies.BarLevFox2020.permA Phenomena.Modality.Studies.BarLevFox2020.FCWorld.onlyB = False
• Phenomena.Modality.Studies.BarLevFox2020.permA Phenomena.Modality.Studies.BarLevFox2020.FCWorld.both = True
• Phenomena.Modality.Studies.BarLevFox2020.permA Phenomena.Modality.Studies.BarLevFox2020.FCWorld.separatelyAB = True

def Phenomena.Modality.Studies.BarLevFox2020.permB : Set FCWorld

◇b — b is permitted at the world.

Equations

• Phenomena.Modality.Studies.BarLevFox2020.permB Phenomena.Modality.Studies.BarLevFox2020.FCWorld.neither = False
• Phenomena.Modality.Studies.BarLevFox2020.permB Phenomena.Modality.Studies.BarLevFox2020.FCWorld.onlyA = False
• Phenomena.Modality.Studies.BarLevFox2020.permB Phenomena.Modality.Studies.BarLevFox2020.FCWorld.onlyB = True
• Phenomena.Modality.Studies.BarLevFox2020.permB Phenomena.Modality.Studies.BarLevFox2020.FCWorld.both = True
• Phenomena.Modality.Studies.BarLevFox2020.permB Phenomena.Modality.Studies.BarLevFox2020.FCWorld.separatelyAB = True

def Phenomena.Modality.Studies.BarLevFox2020.permAorB : Set FCWorld

◇(a ∨ b) — the prejacent.

Equations

• Phenomena.Modality.Studies.BarLevFox2020.permAorB Phenomena.Modality.Studies.BarLevFox2020.FCWorld.neither = False
• Phenomena.Modality.Studies.BarLevFox2020.permAorB Phenomena.Modality.Studies.BarLevFox2020.FCWorld.onlyA = True
• Phenomena.Modality.Studies.BarLevFox2020.permAorB Phenomena.Modality.Studies.BarLevFox2020.FCWorld.onlyB = True
• Phenomena.Modality.Studies.BarLevFox2020.permAorB Phenomena.Modality.Studies.BarLevFox2020.FCWorld.both = True
• Phenomena.Modality.Studies.BarLevFox2020.permAorB Phenomena.Modality.Studies.BarLevFox2020.FCWorld.separatelyAB = True

def Phenomena.Modality.Studies.BarLevFox2020.permAandB : Set FCWorld

◇(a ∧ b) — joint permission.

Equations

• Phenomena.Modality.Studies.BarLevFox2020.permAandB Phenomena.Modality.Studies.BarLevFox2020.FCWorld.neither = False
• Phenomena.Modality.Studies.BarLevFox2020.permAandB Phenomena.Modality.Studies.BarLevFox2020.FCWorld.onlyA = False
• Phenomena.Modality.Studies.BarLevFox2020.permAandB Phenomena.Modality.Studies.BarLevFox2020.FCWorld.onlyB = False
• Phenomena.Modality.Studies.BarLevFox2020.permAandB Phenomena.Modality.Studies.BarLevFox2020.FCWorld.both = True
• Phenomena.Modality.Studies.BarLevFox2020.permAandB Phenomena.Modality.Studies.BarLevFox2020.FCWorld.separatelyAB = False

def Phenomena.Modality.Studies.BarLevFox2020.fcALT : Set (Set FCWorld)

The free-choice alternative set: {◇(a ∨ b), ◇a, ◇b, ◇(a ∧ b)}.

Equations

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

def Phenomena.Modality.Studies.BarLevFox2020.fcPrejacent : Set FCWorld

The prejacent: ◇(a ∨ b).

Equations

• Phenomena.Modality.Studies.BarLevFox2020.fcPrejacent = Phenomena.Modality.Studies.BarLevFox2020.permAorB

theorem Phenomena.Modality.Studies.BarLevFox2020.fc_alt_not_closed_under_pairwise_conjunction : ¬∀ X ⊆ fcALT, ⋂₀ X ∈ fcALT

@cite{bar-lev-fox-2020} eqn (13b) p. 182: the pairwise conjunction of the disjunctive alternatives is NOT closed by fcALT. The separatelyAB world satisfies permA ∩ permB but no element of fcALT (specifically not permAandB); witnesses at .onlyA/ .onlyB rule out the other three potential matches. This structural property — that Alt(◇(a∨b)) is not closed under pairwise conjunction — is what lets cell identification yield free choice.

The cornerstone of the free-choice derivation is exhibiting a world that witnesses the cell of the partition induced by fcALT. Once this is in place, free choice follows as a one-line corollary of mem_II_of_cell_witness.

The witness world is separatelyAB. Establishing the cell predicate at separatelyAB requires four facts about the IE structure of fcALT:

• permAorB is not innocently excludable (since permAorBᶜ contradicts the prejacent in any MC-set);
• permA is not innocently excludable (witnessed by an MC-set that omits permAᶜ);
• permB is not innocently excludable (symmetric);
• permAandB is innocently excludable.

theorem Phenomena.Modality.Studies.BarLevFox2020.separatelyAB_in_cell : Exhaustification.cell fcALT fcPrejacent FCWorld.separatelyAB

Cell witness for the FC alternative set. The separatelyAB world verifies cell fcALT fcPrejacent — it satisfies the prejacent, falsifies every IE-excludable alternative (only permAandB), and verifies every non-excludable alternative (permAorB, permA, permB).

theorem Phenomena.Modality.Studies.BarLevFox2020.free_choice (w : FCWorld) : Exhaustification.exhIEII fcALT fcPrejacent w → permA w ∧ permB w

Main free-choice theorem. Exh^{IE+II}(◇(a ∨ b)) ⊨ ◇a ∧ ◇b.

Direct application of the substrate-level cell-witness factorization exhIEII_implies_cell_witnessed_alt (Operators/InnocentInclusion.lean) to each disjunct, using separatelyAB_in_cell as the cell witness. The substrate theorem encapsulates the abstract content of @cite{bar-lev-fox-2020} §3.3: any alternative true at a cell witness is entailed by exhIEII.

inductive Phenomena.Modality.Studies.BarLevFox2020.DisjWorld : Type

Simple-disjunction worlds (no modal layer).

• neither : DisjWorld
• onlyA : DisjWorld
• onlyB : DisjWorld
• both : DisjWorld

@[implicit_reducible]

instance Phenomena.Modality.Studies.BarLevFox2020.instDecidableEqDisjWorld : DecidableEq DisjWorld

Equations

• Phenomena.Modality.Studies.BarLevFox2020.instDecidableEqDisjWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Modality.Studies.BarLevFox2020.instReprDisjWorld.repr : DisjWorld → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Modality.Studies.BarLevFox2020.instReprDisjWorld : Repr DisjWorld

Equations

• Phenomena.Modality.Studies.BarLevFox2020.instReprDisjWorld = { reprPrec := Phenomena.Modality.Studies.BarLevFox2020.instReprDisjWorld.repr }

@[implicit_reducible]

instance Phenomena.Modality.Studies.BarLevFox2020.instInhabitedDisjWorld : Inhabited DisjWorld

Equations

• Phenomena.Modality.Studies.BarLevFox2020.instInhabitedDisjWorld = { default := Phenomena.Modality.Studies.BarLevFox2020.instInhabitedDisjWorld.default }

def Phenomena.Modality.Studies.BarLevFox2020.instInhabitedDisjWorld.default : DisjWorld

Equations

• Phenomena.Modality.Studies.BarLevFox2020.instInhabitedDisjWorld.default = Phenomena.Modality.Studies.BarLevFox2020.DisjWorld.neither

def Phenomena.Modality.Studies.BarLevFox2020.propA : Set DisjWorld

Atomic proposition a.

Equations

• Phenomena.Modality.Studies.BarLevFox2020.propA Phenomena.Modality.Studies.BarLevFox2020.DisjWorld.neither = False
• Phenomena.Modality.Studies.BarLevFox2020.propA Phenomena.Modality.Studies.BarLevFox2020.DisjWorld.onlyA = True
• Phenomena.Modality.Studies.BarLevFox2020.propA Phenomena.Modality.Studies.BarLevFox2020.DisjWorld.onlyB = False
• Phenomena.Modality.Studies.BarLevFox2020.propA Phenomena.Modality.Studies.BarLevFox2020.DisjWorld.both = True

def Phenomena.Modality.Studies.BarLevFox2020.propB : Set DisjWorld

Atomic proposition b.

Equations

• Phenomena.Modality.Studies.BarLevFox2020.propB Phenomena.Modality.Studies.BarLevFox2020.DisjWorld.neither = False
• Phenomena.Modality.Studies.BarLevFox2020.propB Phenomena.Modality.Studies.BarLevFox2020.DisjWorld.onlyA = False
• Phenomena.Modality.Studies.BarLevFox2020.propB Phenomena.Modality.Studies.BarLevFox2020.DisjWorld.onlyB = True
• Phenomena.Modality.Studies.BarLevFox2020.propB Phenomena.Modality.Studies.BarLevFox2020.DisjWorld.both = True

def Phenomena.Modality.Studies.BarLevFox2020.propAorB : Set DisjWorld

Disjunction a ∨ b.

Equations

• Phenomena.Modality.Studies.BarLevFox2020.propAorB Phenomena.Modality.Studies.BarLevFox2020.DisjWorld.neither = False
• Phenomena.Modality.Studies.BarLevFox2020.propAorB Phenomena.Modality.Studies.BarLevFox2020.DisjWorld.onlyA = True
• Phenomena.Modality.Studies.BarLevFox2020.propAorB Phenomena.Modality.Studies.BarLevFox2020.DisjWorld.onlyB = True
• Phenomena.Modality.Studies.BarLevFox2020.propAorB Phenomena.Modality.Studies.BarLevFox2020.DisjWorld.both = True

def Phenomena.Modality.Studies.BarLevFox2020.propAandB : Set DisjWorld

Conjunction a ∧ b.

Equations

• Phenomena.Modality.Studies.BarLevFox2020.propAandB Phenomena.Modality.Studies.BarLevFox2020.DisjWorld.neither = False
• Phenomena.Modality.Studies.BarLevFox2020.propAandB Phenomena.Modality.Studies.BarLevFox2020.DisjWorld.onlyA = False
• Phenomena.Modality.Studies.BarLevFox2020.propAandB Phenomena.Modality.Studies.BarLevFox2020.DisjWorld.onlyB = False
• Phenomena.Modality.Studies.BarLevFox2020.propAandB Phenomena.Modality.Studies.BarLevFox2020.DisjWorld.both = True

def Phenomena.Modality.Studies.BarLevFox2020.simpleALT : Set (Set DisjWorld)

Simple disjunction's alternative set: {a ∨ b, a, b, a ∧ b}.

Equations

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

theorem Phenomena.Modality.Studies.BarLevFox2020.simple_has_conjunction : propAandB ∈ simpleALT

The structural contrast with FC: simple disjunction's alternative set is closed under conjunction (a ∧ b ∈ simpleALT). This is what blocks the cell from being consistent and prevents free choice from arising.

SDA — the second contribution highlighted in the paper title

@cite{bar-lev-fox-2020} §7 derives simplification of disjunctive antecedents by applying Exh^{IE+II} to a counterfactual prejacent (p∨q)□→r over the 4-element alternative set obtained by disjunct-replacement (eqn 65 p. 205):

Alt((p∨q)□→r) = {(p∨q)□→r, p□→r, q□→r, (p∧q)□→r}

The maximal-false-assignment sets (eqn 66 p. 206) yield IE = {(p∧q)□→r}. Innocent Inclusion then asserts the three non-IE alternatives, giving Bar-Lev/Fox's verdict (eqn 67 p. 206):

Exh^{IE+II}((p∨q)□→r) ⇔ (p□→r) ∧ (q□→r) ∧ ¬((p∧q)□→r)

This is the central rival mechanism to @cite{santorio-2018}'s homogeneity-based SDA derivation: both predict the SDA inference (p∨q)□→r ⊨ (p□→r) ∧ (q□→r) via incompatible mechanisms (Bar-Lev/Fox: exhaustification-via-Innocent-Inclusion; Santorio: per-alternative DIST_π homogeneity over Katzir-generated truthmakers). The bar_lev_fox_sda_implies_santorio_sda_inference theorem at the end of this section makes this cross-mechanism agreement Lean-checkable.

inductive Phenomena.Modality.Studies.BarLevFox2020.SDAWorld : Type

Worlds for the SDA toy model. actual is the evaluation world (no atomic prop holds); wp / wq / wpq are the relevant counterfactual alternatives where p (and r), q (and r), or both p and q (but not r) hold respectively.

Designed so that, centered at actual, wp and wq are closer than wpq, making the three conditional alternatives evaluate as follows at actual: prejacent TRUE, p□→r TRUE, q□→r TRUE, (p∧q)□→r FALSE.

• actual : SDAWorld
• wp : SDAWorld
• wq : SDAWorld
• wpq : SDAWorld

@[implicit_reducible]

instance Phenomena.Modality.Studies.BarLevFox2020.instDecidableEqSDAWorld : DecidableEq SDAWorld

Equations

• Phenomena.Modality.Studies.BarLevFox2020.instDecidableEqSDAWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Phenomena.Modality.Studies.BarLevFox2020.instReprSDAWorld : Repr SDAWorld

Equations

• Phenomena.Modality.Studies.BarLevFox2020.instReprSDAWorld = { reprPrec := Phenomena.Modality.Studies.BarLevFox2020.instReprSDAWorld.repr }

def Phenomena.Modality.Studies.BarLevFox2020.instReprSDAWorld.repr : SDAWorld → ℕ → Std.Format

Equations

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

def Phenomena.Modality.Studies.BarLevFox2020.instInhabitedSDAWorld.default : SDAWorld

Equations

• Phenomena.Modality.Studies.BarLevFox2020.instInhabitedSDAWorld.default = Phenomena.Modality.Studies.BarLevFox2020.SDAWorld.actual

@[implicit_reducible]

instance Phenomena.Modality.Studies.BarLevFox2020.instInhabitedSDAWorld : Inhabited SDAWorld

Equations

• Phenomena.Modality.Studies.BarLevFox2020.instInhabitedSDAWorld = { default := Phenomena.Modality.Studies.BarLevFox2020.instInhabitedSDAWorld.default }

@[implicit_reducible]

instance Phenomena.Modality.Studies.BarLevFox2020.instFintypeSDAWorld : Fintype SDAWorld

Equations

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

def Phenomena.Modality.Studies.BarLevFox2020.sdaP : SDAWorld → Prop

Atomic proposition p.

Equations

• Phenomena.Modality.Studies.BarLevFox2020.sdaP Phenomena.Modality.Studies.BarLevFox2020.SDAWorld.actual = False
• Phenomena.Modality.Studies.BarLevFox2020.sdaP Phenomena.Modality.Studies.BarLevFox2020.SDAWorld.wp = True
• Phenomena.Modality.Studies.BarLevFox2020.sdaP Phenomena.Modality.Studies.BarLevFox2020.SDAWorld.wq = False
• Phenomena.Modality.Studies.BarLevFox2020.sdaP Phenomena.Modality.Studies.BarLevFox2020.SDAWorld.wpq = True

def Phenomena.Modality.Studies.BarLevFox2020.sdaQ : SDAWorld → Prop

Atomic proposition q.

Equations

• Phenomena.Modality.Studies.BarLevFox2020.sdaQ Phenomena.Modality.Studies.BarLevFox2020.SDAWorld.actual = False
• Phenomena.Modality.Studies.BarLevFox2020.sdaQ Phenomena.Modality.Studies.BarLevFox2020.SDAWorld.wp = False
• Phenomena.Modality.Studies.BarLevFox2020.sdaQ Phenomena.Modality.Studies.BarLevFox2020.SDAWorld.wq = True
• Phenomena.Modality.Studies.BarLevFox2020.sdaQ Phenomena.Modality.Studies.BarLevFox2020.SDAWorld.wpq = True

def Phenomena.Modality.Studies.BarLevFox2020.sdaR : SDAWorld → Prop

Atomic proposition r.

Equations

• Phenomena.Modality.Studies.BarLevFox2020.sdaR Phenomena.Modality.Studies.BarLevFox2020.SDAWorld.actual = False
• Phenomena.Modality.Studies.BarLevFox2020.sdaR Phenomena.Modality.Studies.BarLevFox2020.SDAWorld.wp = True
• Phenomena.Modality.Studies.BarLevFox2020.sdaR Phenomena.Modality.Studies.BarLevFox2020.SDAWorld.wq = True
• Phenomena.Modality.Studies.BarLevFox2020.sdaR Phenomena.Modality.Studies.BarLevFox2020.SDAWorld.wpq = False

@[implicit_reducible]

instance Phenomena.Modality.Studies.BarLevFox2020.instDecidablePredSDAWorldSdaP : DecidablePred sdaP

Equations

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

@[implicit_reducible]

instance Phenomena.Modality.Studies.BarLevFox2020.instDecidablePredSDAWorldSdaQ : DecidablePred sdaQ

Equations

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

@[implicit_reducible]

instance Phenomena.Modality.Studies.BarLevFox2020.instDecidablePredSDAWorldSdaR : DecidablePred sdaR

Equations

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

def Phenomena.Modality.Studies.BarLevFox2020.sdaSim : Core.Order.SimilarityOrdering SDAWorld

Similarity ordering: from actual, wp and wq are closer than wpq. From wp, wp itself is closer than wpq (so closest p-worlds from wp are just {wp}). Symmetric for wq. The minimal structure needed for the cell-witness analysis at actual.

Equations

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

def Phenomena.Modality.Studies.BarLevFox2020.sdaPbox : Set SDAWorld

The conditional p □→ r as a Set SDAWorld.

Equations

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

def Phenomena.Modality.Studies.BarLevFox2020.sdaQbox : Set SDAWorld

The conditional q □→ r as a Set SDAWorld.

Equations

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

def Phenomena.Modality.Studies.BarLevFox2020.sdaPorQbox : Set SDAWorld

The conditional (p∨q) □→ r (the prejacent) as a Set SDAWorld.

Equations

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

def Phenomena.Modality.Studies.BarLevFox2020.sdaPandQbox : Set SDAWorld

The conditional (p∧q) □→ r as a Set SDAWorld.

Equations

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

def Phenomena.Modality.Studies.BarLevFox2020.sdaALT : Set (Set SDAWorld)

The SDA alternative set per eqn (65) p. 205.

Equations

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

def Phenomena.Modality.Studies.BarLevFox2020.sdaPrejacent : Set SDAWorld

The SDA prejacent: (p∨q) □→ r.

Equations

• Phenomena.Modality.Studies.BarLevFox2020.sdaPrejacent = Phenomena.Modality.Studies.BarLevFox2020.sdaPorQbox

Per-alternative verdicts at .actual

theorem Phenomena.Modality.Studies.BarLevFox2020.sdaPrejacent_at_actual : sdaPrejacent SDAWorld.actual

theorem Phenomena.Modality.Studies.BarLevFox2020.sdaPbox_at_actual : sdaPbox SDAWorld.actual

theorem Phenomena.Modality.Studies.BarLevFox2020.sdaQbox_at_actual : sdaQbox SDAWorld.actual

theorem Phenomena.Modality.Studies.BarLevFox2020.sdaPandQbox_false_at_actual : ¬sdaPandQbox SDAWorld.actual

Per-world verdicts at the MC-set witnesses .wp and .wq.

theorem Phenomena.Modality.Studies.BarLevFox2020.sdaPrejacent_at_wp : sdaPrejacent SDAWorld.wp

theorem Phenomena.Modality.Studies.BarLevFox2020.sdaPrejacent_at_wq : sdaPrejacent SDAWorld.wq

theorem Phenomena.Modality.Studies.BarLevFox2020.sdaPbox_at_wp : sdaPbox SDAWorld.wp

theorem Phenomena.Modality.Studies.BarLevFox2020.sdaPbox_false_at_wq : ¬sdaPbox SDAWorld.wq

theorem Phenomena.Modality.Studies.BarLevFox2020.sdaQbox_at_wq : sdaQbox SDAWorld.wq

theorem Phenomena.Modality.Studies.BarLevFox2020.sdaQbox_false_at_wp : ¬sdaQbox SDAWorld.wp

IE structure (paper eqn 66 p. 206)

The maximal-false-assignment subsets of sdaALT (consistent with the prejacent) are {sdaPbox, sdaPandQbox} and {sdaQbox, sdaPandQbox}, yielding IE(prejacent, sdaALT) = {sdaPandQbox}. The proofs adapt §3's FC pattern (permA_not_ie / permB_not_ie / permAandB_is_ie) to conditional-typed alternatives.

theorem Phenomena.Modality.Studies.BarLevFox2020.sdaPandQbox_always_false (u : SDAWorld) : ¬sdaPandQbox u

sdaPandQbox is identically false on SDAWorld: the unique (p∧q)-world is .wpq, where r does not hold, so universalCounterfactual sim (p∧q) r u fails for every u.

theorem Phenomena.Modality.Studies.BarLevFox2020.sdaPrejacent_not_ie : ¬Exhaustification.IsInnocentlyExcludable sdaALT sdaPrejacent sdaPorQbox

theorem Phenomena.Modality.Studies.BarLevFox2020.sdaPbox_not_ie : ¬Exhaustification.IsInnocentlyExcludable sdaALT sdaPrejacent sdaPbox

sdaPbox is not innocently excludable: the MC-set {prejacent, sdaQboxᶜ, sdaPandQboxᶜ} does not contain sdaPboxᶜ.

theorem Phenomena.Modality.Studies.BarLevFox2020.sdaQbox_not_ie : ¬Exhaustification.IsInnocentlyExcludable sdaALT sdaPrejacent sdaQbox

sdaQbox is not innocently excludable (symmetric to sdaPbox).

theorem Phenomena.Modality.Studies.BarLevFox2020.sdaPandQbox_is_ie : Exhaustification.IsInnocentlyExcludable sdaALT sdaPrejacent sdaPandQbox

sdaPandQbox IS innocently excludable: since sdaPandQbox is identically false on SDAWorld, sdaPandQboxᶜ holds at every world, so adjoining it to any MC-set keeps it consistent — maximality forces inclusion.

theorem Phenomena.Modality.Studies.BarLevFox2020.actual_in_sda_cell : Exhaustification.cell sdaALT sdaPrejacent SDAWorld.actual

Cell witness for the SDA alternative set. The .actual world verifies cell sdaALT sdaPrejacent: it satisfies the prejacent plus the two non-IE conditional alternatives (sdaPbox, sdaQbox) and falsifies the unique IE alternative (sdaPandQbox). Once the IE-structure proofs above are complete, this follows from the per-alternative verdicts at .actual.

theorem Phenomena.Modality.Studies.BarLevFox2020.bar_lev_fox_sda (w : SDAWorld) : Exhaustification.exhIEII sdaALT sdaPrejacent w → sdaPbox w ∧ sdaQbox w ∧ ¬sdaPandQbox w

Bar-Lev/Fox SDA derivation (paper eqn 67 p. 206). Exh^{IE+II}((p∨q)□→r) entails (p□→r) ∧ (q□→r) ∧ ¬((p∧q)□→r). Three one-shot applications of the substrate-level cell-witness factorization theorems (Operators/InnocentInclusion.lean): exhIEII_implies_cell_witnessed_alt for the two non-IE conditionals (witnessed at .actual), and exhIEII_negates_excludable for the unique IE alternative.

The central debate Zani-Ciardelli-Sanfelici 2026 frames

@cite{santorio-2018} derives SDA via per-alternative homogeneity (sdaEval = universal over per-disjunct counterfactuals). @cite{bar-lev-fox-2020} derives SDA via Innocent Inclusion (exhIEII over disjunct-replacement alternatives, asserting the non-IE conditional alternatives). The two mechanisms are RIVAL but they AGREE on the SDA inference proper:

(p∨q)□→r ⊨ (p□→r) ∧ (q□→r)

This agreement is the substrate for @cite{zani-ciardelli-sanfelici-2026}'s acquisition study, which contrasts the two frameworks' predicted developmental trajectories (Bar-Lev/Fox: AR→SDA; Santorio: DCR→SDA). The cross-mechanism agreement theorem below makes this Lean-checkable.

Bar-Lev/Fox's full verdict additionally entails ¬((p∧q)□→r) (the IE-driven negation of the conjunctive alternative); Santorio's sdaEval does not entail this. So Bar-Lev/Fox is STRICTLY STRONGER than Santorio on this scenario — they agree on SDA, diverge on the extra negative conjunct.

def Phenomena.Modality.Studies.BarLevFox2020.sdaSantorioAlts : List (Conditionals.Studies.Santorio2018.DecAlt SDAWorld)

The SDA alternatives as DecAlt SDAWorlds for use in @cite{santorio-2018}'s sdaEval apparatus.

Equations

• Phenomena.Modality.Studies.BarLevFox2020.sdaSantorioAlts = [⟨Phenomena.Modality.Studies.BarLevFox2020.sdaP, inferInstance⟩, ⟨Phenomena.Modality.Studies.BarLevFox2020.sdaQ, inferInstance⟩]

theorem Phenomena.Modality.Studies.BarLevFox2020.bar_lev_fox_sda_implies_santorio_sda_inference (w : SDAWorld) : Exhaustification.exhIEII sdaALT sdaPrejacent w → Conditionals.Studies.Santorio2018.sdaEval sdaSim sdaSantorioAlts sdaR w

Cross-framework agreement on the SDA inference. @cite{bar-lev-fox-2020}'s Exh^{IE+II} verdict on the SDA prejacent entails @cite{santorio-2018}'s sdaEval verdict on the same scenario.

Direct application of the substrate-level multi-target cell-witness factorization exhIEII_implies_cell_witnessed_alts to the list of Santorio-style disjunct conditionals [sdaPbox, sdaQbox]. The factorization captures the abstract structural fact (any cell-witnessed alternatives are jointly entailed by Exh^{IE+II}); the bridge to sdaEval is mechanical via sdaEval_iff_forall. Santorio is silent on the negative conjunct ¬((p∧q)□→r) that Bar-Lev/Fox additionally derives — they coincide on the SDA inference proper, diverge on the negative component.

◇∀x(Px ∨ Qx) ⊨ ◇∀xPx ∧ ◇∀xQx — second application of Exh^{IE+II}

@cite{bar-lev-fox-2020} §6.1 derives universal free choice by applying Exh^{IE+II} to a counterfactual prejacent ◇∀x(Px ∨ Qx) over the 8-element alternative set obtained by replacing both the universal quantifier and the disjunction (eqn 55 p. 202):

Alt(◇∀x(P∨Q)) = {◇∀x(P∨Q), ◇∀xP, ◇∀xQ, ◇∀x(P∧Q), ◇∃x(P∨Q), ◇∃xP, ◇∃xQ, ◇∃x(P∧Q)}

The maximal-false-assignment subsets (eqn 56 p. 202) are three:

• (i) {◇∀xP, ◇∀xQ, ◇∀x(P∧Q), ◇∃x(P∧Q)} — witnessed at wMixed
• (ii) {◇∀xP, ◇∃xP, ◇∀x(P∧Q), ◇∃x(P∧Q)} — witnessed at wAllQ
• (iii) {◇∀xQ, ◇∃xQ, ◇∀x(P∧Q), ◇∃x(P∧Q)} — witnessed at wAllP

yielding IE = {◇∀x(P∧Q), ◇∃x(P∧Q)}. Innocent Inclusion then asserts the six non-IE alternatives, giving Bar-Lev/Fox's verdict (eqn 57 p. 202):

Exh^{IE+II}(◇∀x(P∨Q)) ⇔ ◇∀xP ∧ ◇∀xQ ∧ ¬◇∃x(P∧Q)

This is the second consumer of the substrate factorization theorems exhIEII_implies_cell_witnessed_alt and exhIEII_negates_excludable added in Theories/Semantics/Exhaustification/Operators/InnocentInclusion.lean. The cell witness wAllP_AllQ realizes simultaneous accessibility of the all-P and all-Q scenarios with no overlap-scenario; the main theorem follows in 3 substrate-application lines.

inductive Phenomena.Modality.Studies.BarLevFox2020.UnivFCWorld : Type

Worlds for the universal-FC toy model. Each world represents the set of accessible scenarios from the evaluation point — abstract enough to validate the 8-alternative IE structure of paper eqn 55 p. 202.

• wAllP : UnivFCWorld
• wAllQ : UnivFCWorld
• wMixed : UnivFCWorld
• wAllP_AllQ : UnivFCWorld
• wInaccessible : UnivFCWorld

@[implicit_reducible]

instance Phenomena.Modality.Studies.BarLevFox2020.instDecidableEqUnivFCWorld : DecidableEq UnivFCWorld

Equations

• Phenomena.Modality.Studies.BarLevFox2020.instDecidableEqUnivFCWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Phenomena.Modality.Studies.BarLevFox2020.instReprUnivFCWorld : Repr UnivFCWorld

Equations

• Phenomena.Modality.Studies.BarLevFox2020.instReprUnivFCWorld = { reprPrec := Phenomena.Modality.Studies.BarLevFox2020.instReprUnivFCWorld.repr }

def Phenomena.Modality.Studies.BarLevFox2020.instReprUnivFCWorld.repr : UnivFCWorld → ℕ → Std.Format

Equations

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

def Phenomena.Modality.Studies.BarLevFox2020.instInhabitedUnivFCWorld.default : UnivFCWorld

Equations

• Phenomena.Modality.Studies.BarLevFox2020.instInhabitedUnivFCWorld.default = Phenomena.Modality.Studies.BarLevFox2020.UnivFCWorld.wAllP

@[implicit_reducible]

instance Phenomena.Modality.Studies.BarLevFox2020.instInhabitedUnivFCWorld : Inhabited UnivFCWorld

Equations

• Phenomena.Modality.Studies.BarLevFox2020.instInhabitedUnivFCWorld = { default := Phenomena.Modality.Studies.BarLevFox2020.instInhabitedUnivFCWorld.default }

@[implicit_reducible]

instance Phenomena.Modality.Studies.BarLevFox2020.instFintypeUnivFCWorld : Fintype UnivFCWorld

Equations

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

The 8 alternative predicates per paper eqn (55) p. 202

def Phenomena.Modality.Studies.BarLevFox2020.univFcAllPorQ : Set UnivFCWorld

◇∀x(P∨Q) — the prejacent: some accessible scenario has every individual reading at least one of P, Q.

Equations

• Phenomena.Modality.Studies.BarLevFox2020.univFcAllPorQ Phenomena.Modality.Studies.BarLevFox2020.UnivFCWorld.wAllP = True
• Phenomena.Modality.Studies.BarLevFox2020.univFcAllPorQ Phenomena.Modality.Studies.BarLevFox2020.UnivFCWorld.wAllQ = True
• Phenomena.Modality.Studies.BarLevFox2020.univFcAllPorQ Phenomena.Modality.Studies.BarLevFox2020.UnivFCWorld.wMixed = True
• Phenomena.Modality.Studies.BarLevFox2020.univFcAllPorQ Phenomena.Modality.Studies.BarLevFox2020.UnivFCWorld.wAllP_AllQ = True
• Phenomena.Modality.Studies.BarLevFox2020.univFcAllPorQ Phenomena.Modality.Studies.BarLevFox2020.UnivFCWorld.wInaccessible = False

def Phenomena.Modality.Studies.BarLevFox2020.univFcAllP : Set UnivFCWorld

◇∀xP — some accessible scenario has every individual reading P.

Equations

• Phenomena.Modality.Studies.BarLevFox2020.univFcAllP Phenomena.Modality.Studies.BarLevFox2020.UnivFCWorld.wAllP = True
• Phenomena.Modality.Studies.BarLevFox2020.univFcAllP Phenomena.Modality.Studies.BarLevFox2020.UnivFCWorld.wAllP_AllQ = True
• Phenomena.Modality.Studies.BarLevFox2020.univFcAllP Phenomena.Modality.Studies.BarLevFox2020.UnivFCWorld.wAllQ = False
• Phenomena.Modality.Studies.BarLevFox2020.univFcAllP Phenomena.Modality.Studies.BarLevFox2020.UnivFCWorld.wMixed = False
• Phenomena.Modality.Studies.BarLevFox2020.univFcAllP Phenomena.Modality.Studies.BarLevFox2020.UnivFCWorld.wInaccessible = False

def Phenomena.Modality.Studies.BarLevFox2020.univFcAllQ : Set UnivFCWorld

◇∀xQ — some accessible scenario has every individual reading Q.

Equations

• Phenomena.Modality.Studies.BarLevFox2020.univFcAllQ Phenomena.Modality.Studies.BarLevFox2020.UnivFCWorld.wAllQ = True
• Phenomena.Modality.Studies.BarLevFox2020.univFcAllQ Phenomena.Modality.Studies.BarLevFox2020.UnivFCWorld.wAllP_AllQ = True
• Phenomena.Modality.Studies.BarLevFox2020.univFcAllQ Phenomena.Modality.Studies.BarLevFox2020.UnivFCWorld.wAllP = False
• Phenomena.Modality.Studies.BarLevFox2020.univFcAllQ Phenomena.Modality.Studies.BarLevFox2020.UnivFCWorld.wMixed = False
• Phenomena.Modality.Studies.BarLevFox2020.univFcAllQ Phenomena.Modality.Studies.BarLevFox2020.UnivFCWorld.wInaccessible = False

def Phenomena.Modality.Studies.BarLevFox2020.univFcAllBoth : Set UnivFCWorld

◇∀x(P∧Q) — some accessible scenario has every individual reading both. None of our worlds witness an all-both scenario.

Equations

• Phenomena.Modality.Studies.BarLevFox2020.univFcAllBoth x✝ = False

def Phenomena.Modality.Studies.BarLevFox2020.univFcSomePorQ : Set UnivFCWorld

◇∃x(P∨Q) — some accessible scenario has some individual reading at least one.

Equations

• Phenomena.Modality.Studies.BarLevFox2020.univFcSomePorQ Phenomena.Modality.Studies.BarLevFox2020.UnivFCWorld.wInaccessible = False
• Phenomena.Modality.Studies.BarLevFox2020.univFcSomePorQ x✝ = True

def Phenomena.Modality.Studies.BarLevFox2020.univFcSomeP : Set UnivFCWorld

◇∃xP — some accessible scenario has some individual reading P.

Equations

• Phenomena.Modality.Studies.BarLevFox2020.univFcSomeP Phenomena.Modality.Studies.BarLevFox2020.UnivFCWorld.wAllP = True
• Phenomena.Modality.Studies.BarLevFox2020.univFcSomeP Phenomena.Modality.Studies.BarLevFox2020.UnivFCWorld.wMixed = True
• Phenomena.Modality.Studies.BarLevFox2020.univFcSomeP Phenomena.Modality.Studies.BarLevFox2020.UnivFCWorld.wAllP_AllQ = True
• Phenomena.Modality.Studies.BarLevFox2020.univFcSomeP Phenomena.Modality.Studies.BarLevFox2020.UnivFCWorld.wAllQ = False
• Phenomena.Modality.Studies.BarLevFox2020.univFcSomeP Phenomena.Modality.Studies.BarLevFox2020.UnivFCWorld.wInaccessible = False

def Phenomena.Modality.Studies.BarLevFox2020.univFcSomeQ : Set UnivFCWorld

◇∃xQ — some accessible scenario has some individual reading Q.

Equations

• Phenomena.Modality.Studies.BarLevFox2020.univFcSomeQ Phenomena.Modality.Studies.BarLevFox2020.UnivFCWorld.wAllQ = True
• Phenomena.Modality.Studies.BarLevFox2020.univFcSomeQ Phenomena.Modality.Studies.BarLevFox2020.UnivFCWorld.wMixed = True
• Phenomena.Modality.Studies.BarLevFox2020.univFcSomeQ Phenomena.Modality.Studies.BarLevFox2020.UnivFCWorld.wAllP_AllQ = True
• Phenomena.Modality.Studies.BarLevFox2020.univFcSomeQ Phenomena.Modality.Studies.BarLevFox2020.UnivFCWorld.wAllP = False
• Phenomena.Modality.Studies.BarLevFox2020.univFcSomeQ Phenomena.Modality.Studies.BarLevFox2020.UnivFCWorld.wInaccessible = False

def Phenomena.Modality.Studies.BarLevFox2020.univFcSomeBoth : Set UnivFCWorld

◇∃x(P∧Q) — some accessible scenario has some individual reading both. None of our worlds witness an overlap scenario.

Equations

• Phenomena.Modality.Studies.BarLevFox2020.univFcSomeBoth x✝ = False

def Phenomena.Modality.Studies.BarLevFox2020.universalFcALT : Set (Set UnivFCWorld)

The 8-element alternative set per paper eqn (55) p. 202.

Equations

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

def Phenomena.Modality.Studies.BarLevFox2020.universalFcPrejacent : Set UnivFCWorld

The universal-FC prejacent.

Equations

• Phenomena.Modality.Studies.BarLevFox2020.universalFcPrejacent = Phenomena.Modality.Studies.BarLevFox2020.univFcAllPorQ

Per-world verdicts at the cell witness wAllP_AllQ

Established by direct case analysis. The cell witness satisfies the prejacent + every non-IE alternative; the two IE alternatives (univFcAllBoth, univFcSomeBoth) are identically false on this toy model.

theorem Phenomena.Modality.Studies.BarLevFox2020.universalFcPrejacent_at_witness : universalFcPrejacent UnivFCWorld.wAllP_AllQ

theorem Phenomena.Modality.Studies.BarLevFox2020.univFcAllP_at_witness : univFcAllP UnivFCWorld.wAllP_AllQ

theorem Phenomena.Modality.Studies.BarLevFox2020.univFcAllQ_at_witness : univFcAllQ UnivFCWorld.wAllP_AllQ

theorem Phenomena.Modality.Studies.BarLevFox2020.univFcSomePorQ_at_witness : univFcSomePorQ UnivFCWorld.wAllP_AllQ

theorem Phenomena.Modality.Studies.BarLevFox2020.univFcSomeP_at_witness : univFcSomeP UnivFCWorld.wAllP_AllQ

theorem Phenomena.Modality.Studies.BarLevFox2020.univFcSomeQ_at_witness : univFcSomeQ UnivFCWorld.wAllP_AllQ

theorem Phenomena.Modality.Studies.BarLevFox2020.univFcAllBoth_always_false (u : UnivFCWorld) : ¬univFcAllBoth u

theorem Phenomena.Modality.Studies.BarLevFox2020.univFcSomeBoth_always_false (u : UnivFCWorld) : ¬univFcSomeBoth u

Finset-side alternative set + bridge to Set side

For decidability of cell membership and IE-ness, work with Finset versions of the 8 alternatives. Bridge equations to the Set side let the general substrate theorems (Operators/InnocentInclusion.lean::mem_II_of_cell_witness, not_isInnocentlyExcludable_of_cell_witness) consume Finset-derived facts via decide.

def Phenomena.Modality.Studies.BarLevFox2020.univFcAllPorQ_f : Finset UnivFCWorld

Finset version of univFcAllPorQ.

Equations

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

def Phenomena.Modality.Studies.BarLevFox2020.univFcAllP_f : Finset UnivFCWorld

Equations

• Phenomena.Modality.Studies.BarLevFox2020.univFcAllP_f = {Phenomena.Modality.Studies.BarLevFox2020.UnivFCWorld.wAllP, Phenomena.Modality.Studies.BarLevFox2020.UnivFCWorld.wAllP_AllQ}

def Phenomena.Modality.Studies.BarLevFox2020.univFcAllQ_f : Finset UnivFCWorld

Equations

• Phenomena.Modality.Studies.BarLevFox2020.univFcAllQ_f = {Phenomena.Modality.Studies.BarLevFox2020.UnivFCWorld.wAllQ, Phenomena.Modality.Studies.BarLevFox2020.UnivFCWorld.wAllP_AllQ}

def Phenomena.Modality.Studies.BarLevFox2020.univFcAllBoth_f : Finset UnivFCWorld

Equations

• Phenomena.Modality.Studies.BarLevFox2020.univFcAllBoth_f = ∅

def Phenomena.Modality.Studies.BarLevFox2020.univFcSomePorQ_f : Finset UnivFCWorld

Equations

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

def Phenomena.Modality.Studies.BarLevFox2020.univFcSomeP_f : Finset UnivFCWorld

Equations

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

def Phenomena.Modality.Studies.BarLevFox2020.univFcSomeQ_f : Finset UnivFCWorld

Equations

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

def Phenomena.Modality.Studies.BarLevFox2020.univFcSomeBoth_f : Finset UnivFCWorld

Equations

• Phenomena.Modality.Studies.BarLevFox2020.univFcSomeBoth_f = ∅

def Phenomena.Modality.Studies.BarLevFox2020.universalFcALT_f : Finset (Finset UnivFCWorld)

The 8-element alternative set (Finset-typed) per paper eqn (55) p. 202.

Equations

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

def Phenomena.Modality.Studies.BarLevFox2020.universalFcPrejacent_f : Finset UnivFCWorld

The Finset-side prejacent.

Equations

• Phenomena.Modality.Studies.BarLevFox2020.universalFcPrejacent_f = Phenomena.Modality.Studies.BarLevFox2020.univFcAllPorQ_f

Per-alt Set/Finset bridge equations

theorem Phenomena.Modality.Studies.BarLevFox2020.univFcAllPorQ_eq : univFcAllPorQ = ↑univFcAllPorQ_f

theorem Phenomena.Modality.Studies.BarLevFox2020.univFcAllP_eq : univFcAllP = ↑univFcAllP_f

theorem Phenomena.Modality.Studies.BarLevFox2020.univFcAllQ_eq : univFcAllQ = ↑univFcAllQ_f

theorem Phenomena.Modality.Studies.BarLevFox2020.univFcAllBoth_eq : univFcAllBoth = ↑univFcAllBoth_f

theorem Phenomena.Modality.Studies.BarLevFox2020.univFcSomePorQ_eq : univFcSomePorQ = ↑univFcSomePorQ_f

theorem Phenomena.Modality.Studies.BarLevFox2020.univFcSomeP_eq : univFcSomeP = ↑univFcSomeP_f

theorem Phenomena.Modality.Studies.BarLevFox2020.univFcSomeQ_eq : univFcSomeQ = ↑univFcSomeQ_f

theorem Phenomena.Modality.Studies.BarLevFox2020.univFcSomeBoth_eq : univFcSomeBoth = ↑univFcSomeBoth_f

theorem Phenomena.Modality.Studies.BarLevFox2020.universalFcALT_eq : universalFcALT = Exhaustification.Innocent.asSetOfSets universalFcALT_f

ALT-level bridge: the Set-typed universalFcALT equals the asSetOfSets image of the Finset-typed universalFcALT_f. Lifts Finset-side membership facts to the Set-side substrate theorems.

theorem Phenomena.Modality.Studies.BarLevFox2020.universalFcPrejacent_eq : universalFcPrejacent = ↑universalFcPrejacent_f

Prejacent bridge.

Cell witness via Finset bridge

theorem Phenomena.Modality.Studies.BarLevFox2020.wAllP_AllQ_in_universal_fc_cell : Exhaustification.cell universalFcALT universalFcPrejacent UnivFCWorld.wAllP_AllQ

Cell witness for the universal-FC alternative set (paper eqn 56 p. 202 cell). wAllP_AllQ is in the cell. Proof: decide- checkable on the Finset side (Operators/Decidable.lean::cellFinset); lifted to Set via mem_cellFinset_iff + universalFcALT_eq / universalFcPrejacent_eq. Replaces ~250 LOC of manual MC-set + IE-structure proofs from earlier versions.

Innocent excludability theorems (cell-witness corollaries)

theorem Phenomena.Modality.Studies.BarLevFox2020.universalFcPrejacent_not_ie : ¬Exhaustification.IsInnocentlyExcludable universalFcALT universalFcPrejacent univFcAllPorQ

theorem Phenomena.Modality.Studies.BarLevFox2020.univFcAllP_not_ie : ¬Exhaustification.IsInnocentlyExcludable universalFcALT universalFcPrejacent univFcAllP

theorem Phenomena.Modality.Studies.BarLevFox2020.univFcAllQ_not_ie : ¬Exhaustification.IsInnocentlyExcludable universalFcALT universalFcPrejacent univFcAllQ

theorem Phenomena.Modality.Studies.BarLevFox2020.univFcSomePorQ_not_ie : ¬Exhaustification.IsInnocentlyExcludable universalFcALT universalFcPrejacent univFcSomePorQ

theorem Phenomena.Modality.Studies.BarLevFox2020.univFcSomeP_not_ie : ¬Exhaustification.IsInnocentlyExcludable universalFcALT universalFcPrejacent univFcSomeP

theorem Phenomena.Modality.Studies.BarLevFox2020.univFcSomeQ_not_ie : ¬Exhaustification.IsInnocentlyExcludable universalFcALT universalFcPrejacent univFcSomeQ

theorem Phenomena.Modality.Studies.BarLevFox2020.univFcAllBoth_is_ie : Exhaustification.IsInnocentlyExcludable universalFcALT universalFcPrejacent univFcAllBoth

univFcAllBoth IS innocently excludable: identically false on UnivFCWorld, so its negation is trivially consistent with any MC-set; maximality forces inclusion.

theorem Phenomena.Modality.Studies.BarLevFox2020.univFcSomeBoth_is_ie : Exhaustification.IsInnocentlyExcludable universalFcALT universalFcPrejacent univFcSomeBoth

univFcSomeBoth IS innocently excludable (parallel to AllBoth).

theorem Phenomena.Modality.Studies.BarLevFox2020.universal_fc (w : UnivFCWorld) : Exhaustification.exhIEII universalFcALT universalFcPrejacent w → univFcAllP w ∧ univFcAllQ w ∧ ¬univFcSomeBoth w

Bar-Lev/Fox universal free choice (paper eqn 57 p. 202). Exh^{IE+II}(◇∀x(P∨Q)) ⊨ ◇∀xP ∧ ◇∀xQ ∧ ¬◇∃x(P∧Q).

Three one-shot applications of the substrate-level cell-witness factorization theorems: exhIEII_implies_cell_witnessed_alt for the two universal-distributive non-IE alternatives, and exhIEII_negates_excludable for the existential-conjunctive IE alternative. The substrate factorization (Theories/Semantics/ Exhaustification/Operators/InnocentInclusion.lean) is what makes this main theorem a 3-line consequence of the cell witness.