Docs / Semantics / Exhaustification / InnocentInclusion

Innocent inclusion

import Linglib.Semantics.Exhaustification.InnocentInclusion · namespace Exhaustification

This file defines Bar-Lev and Fox's innocent inclusion, which runs after innocent exclusion. A set of alternatives is a consistent inclusion when its members can all be true together with the exhaustified prejacent; an alternative is innocently includable when it belongs to every maximal consistent inclusion. exhIEII asserts the prejacent, denies the innocently excludable alternatives and asserts the innocently includable ones. The cell of the prejacent asserts it, denies the excludable alternatives and asserts all the others; when the cell is consistent, exhIEII is the cell, and when it is not, as for simple disjunction, innocent inclusion adds nothing to innocent exclusion.

Main statements

Exhaustification.isInnocentlyIncludable_iff_of_cell_nonempty: when the cell is consistent, the innocently includable alternatives are exactly those not innocently excludable.
Exhaustification.exhIEII_eq_cell_of_cell_nonempty: when the cell is consistent, exhaustification is the cell.
Exhaustification.mem_cell_iff: the cell consists of the prejacent worlds verifying exactly the alternatives of the minimal verified sets.

References

Bar-Lev & Fox 2020, Free Choice, Simplification, and Innocent Inclusion formalized

Declarations

L39–42

L44–47

exhIEII ALT φ asserts the prejacent, denies the innocently excludable alternatives and asserts the innocently includable ones.

def exhIEII L49–53

{World : Type u_1} (ALT : Set (Set World)) (φ : Set World) :

Set World

The definition is too large to print here; read it in the source.

Used by mem_exhIEII_iff, exhIEII_eq_exhIE_inter, exhIEII_eq_cell_of_cell_nonempty, IsMinimalCover.exhIEII_eq, exhIEII_eq_diff_of_forall_subset, exhIEII_eq_self_of_forall_subset, exhIEII_singleton

Used in Semantics/Exhaustification/Disjunctive, Semantics/Exhaustification/DomainAlternatives, AghaJeretic2026, BarLev2021, BarLevFox2020 and 4 more

L55–57

L59–63

The cell of the prejacent in the partition the alternatives induce asserts the prejacent, denies the innocently excludable alternatives and asserts all the others.

def cell L65–69

{World : Type u_1} (ALT : Set (Set World)) (φ : Set World) :

Set World

The definition is too large to print here; read it in the source.

Used by mem_cell, isConsistentInclusion_of_cell_nonempty, isInnocentlyIncludable_iff_of_cell_nonempty, exhIEII_eq_cell_of_cell_nonempty, isInnocentlyIncludable_of_mem_cell, cell_eq_of_iff, cell_image_eq, IsMinimalCover.cell_eq, mem_cell_iff, cell_nonempty_iff

Used in Semantics/Exhaustification/Disjunctive, BarLevFox2020, Fox2018

When the cell is consistent, the innocently includable alternatives are exactly those that are not innocently excludable.

theorem isInnocentlyIncludable_iff_of_cell_nonempty L94–102

{World : Type u_1} {ALT : Set (Set World)} {φ : Set World} (h : (cell ALT φ).Nonempty) {a : Set World} :

IsInnocentlyIncludable ALT φ a ↔ a ∈ ALT ∧ ¬IsInnocentlyExcludable ALT φ a

Built from ,

When the cell is consistent, exhaustification is the cell.

theorem exhIEII_eq_cell_of_cell_nonempty L104–111

{World : Type u_1} (ALT : Set (Set World)) (φ : Set World) (h : (cell ALT φ).Nonempty) :

exhIEII ALT φ = cell ALT φ

Built from ,

L114–117

Cells from a characterization of innocent exclusion

L121–131

L133–146

Representative minimal worlds

Verified alternatives

The cell of the prejacent consists of the prejacent worlds verifying exactly the alternatives of the minimal verified sets.

theorem mem_cell_iff L225–246

{World : Type u_1} {ALT : Set (Set World)} {φ : Set World} {w : World} :

w ∈ cell 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}

Built from

L248–252