Exhaustification: abstract excluder

@cite{fox-2007} @cite{chierchia-2013} @cite{magri-2009} @cite{santorio-2018}

Different exhaustification theories disagree on which alternatives the operator should negate, but agree on the rest of the architecture: assert the prejacent and negate the chosen alternatives. This module factors out the agreement: an Excluder is a strategy for choosing alternatives, and Excluder.exh applies it.

Concrete excluders live in sibling modules:

• Innocent.lean — Fox 2007 innocent exclusion
• Tolerant.lean — Chierchia 2013 contradiction-tolerating exclusion
• Relevance.lean — Magri 2009 relevance-sensitive exclusion

Why a structure rather than a type class

Excluders are first-class data: a single semantic theory may invoke several (e.g. recursive exhaustification with two different excluders at two layers). They are not properties of a world type to be inferred by typeclass resolution.

def Exhaustification.predToFinset {W : Type u_1} [Fintype W] (p : W → Bool) : Finset W

Convert a Bool predicate on worlds to its support Finset.

Equations

• Exhaustification.predToFinset p = {w : W | p w = true}

def Exhaustification.altsFromPreds {W : Type u_1} [Fintype W] [DecidableEq W] (alts : List (W → Bool)) : Finset (Finset W)

Convert a list of Bool predicates to a Finset of supports. Uses DecidableEq (Finset W) (free from [DecidableEq W]); does NOT need DecidableEq (W → Bool).

Equations

• Exhaustification.altsFromPreds alts = (List.map Exhaustification.predToFinset alts).toFinset

structure Exhaustification.Excluder (W : Type u_2) [Fintype W] [DecidableEq W] : Type u_2

An exhaustification strategy: a choice, for each prejacent and alternative set, of which alternatives to negate.

Different theories instantiate excluded differently (Fox's innocent exclusion, Chierchia's contradiction-tolerating, Magri's relevance-sensitive, Santorio's stability). The excluded_subset field guarantees the strategy only picks alternatives that were offered.

• excluded : Finset (Finset W) → Finset W → Finset (Finset W)

  Given a prejacent φ and an alternative set ALT, return the alternatives whose negation should be conjoined with φ.

• excluded_subset (ALT : Finset (Finset W)) (φ : Finset W) : self.excluded ALT φ ⊆ ALT

  The strategy returns a sub-collection of the offered alternatives.

def Exhaustification.Excluder.exh {W : Type u_1} [Fintype W] [DecidableEq W] (E : Excluder W) (ALT : Finset (Finset W)) (φ : Finset W) : Finset W

Exhaustified meaning: assert the prejacent and negate every excluded alternative. A world w survives iff w ∈ φ and w ∉ a for every a ∈ E.excluded ALT φ.

Equations

• E.exh ALT φ = φ \ (E.excluded ALT φ).biUnion id

theorem Exhaustification.Excluder.exh_subset_phi {W : Type u_1} [Fintype W] [DecidableEq W] (E : Excluder W) (ALT : Finset (Finset W)) (φ : Finset W) : E.exh ALT φ ⊆ φ

The exhaustified meaning is contained in the prejacent.

theorem Exhaustification.Excluder.mem_exh_iff {W : Type u_1} [Fintype W] [DecidableEq W] (E : Excluder W) (ALT : Finset (Finset W)) (φ : Finset W) {w : W} : w ∈ E.exh ALT φ ↔ w ∈ φ ∧ ∀ a ∈ E.excluded ALT φ, w ∉ a

Membership characterization for exh.