Exhaustification over finite world types

Over a Fintype of worlds, with propositions as Finsets, compatibility, maximal compatibility, innocent excludability and the cell are decidable: every compatible set lies in excludables, so maximality is a search over its powerset. innocent packages innocent exclusion as an Excluder, and the structural theorems compute innocent.exh and tolerant.exh for alternative sets of a given shape. preFilter_can_create_implicature witnesses that removing a symmetric alternative before exclusion strengthens the result.

References

• [Fox07]
• [Spe16]
• [Chi13]
• [FK11]

Coercion

def Exhaustification.asSetOfSets {W : Type u_1} (E : Finset (Finset W)) : Set (Set W)

The alternatives of a finite family, as sets.

Equations

• Exhaustification.asSetOfSets E = (fun (s : Finset W) => ↑s) '' ↑E

@[simp]

theorem Exhaustification.mem_asSetOfSets {W : Type u_1} {E : Finset (Finset W)} {s : Set W} : s ∈ asSetOfSets E ↔ ∃ a ∈ E, ↑a = s

theorem Exhaustification.coe_univ_sdiff {W : Type u_1} [Fintype W] [DecidableEq W] (a : Finset W) : ↑(Finset.univ \ a) = (↑a)ᶜ

The complement of a Finset, as a set.

theorem Exhaustification.mem_inf_id_iff {W : Type u_1} [Fintype W] [DecidableEq W] {s : Finset (Finset W)} {w : W} : w ∈ s.inf id ↔ ∀ a ∈ s, w ∈ a

Membership in the intersection of a finite family.

Compatible sets

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

The prejacent with the complement of every alternative: every compatible set lies in it.

Equations

• Exhaustification.excludables ALT φ = insert φ (Finset.image (fun (a : Finset W) => Finset.univ \ a) ALT)

theorem Exhaustification.isCompatible_iff_finset {W : Type u_1} [Fintype W] [DecidableEq W] (ALT : Finset (Finset W)) (φ : Finset W) (E : Finset (Finset W)) : IsCompatible (asSetOfSets ALT) (↑φ) (asSetOfSets E) ↔ E ⊆ excludables ALT φ ∧ φ ∈ E ∧ (E.inf id).Nonempty

Compatibility over finite families is a Finset condition.

@[instance_reducible]

instance Exhaustification.decidableIsCompatible {W : Type u_1} [Fintype W] [DecidableEq W] (ALT : Finset (Finset W)) (φ : Finset W) (E : Finset (Finset W)) : Decidable (IsCompatible (asSetOfSets ALT) (↑φ) (asSetOfSets E))

Equations

• Exhaustification.decidableIsCompatible ALT φ E = decidable_of_iff (E ⊆ Exhaustification.excludables ALT φ ∧ φ ∈ E ∧ (E.inf id).Nonempty) ⋯

theorem Exhaustification.isMCSet_iff_finset {W : Type u_1} [Fintype W] [DecidableEq W] (ALT : Finset (Finset W)) (φ : Finset W) (E : Finset (Finset W)) : IsMCSet (asSetOfSets ALT) (↑φ) (asSetOfSets E) ↔ IsCompatible (asSetOfSets ALT) (↑φ) (asSetOfSets E) ∧ ∀ E' ∈ (excludables ALT φ).powerset, IsCompatible (asSetOfSets ALT) (↑φ) (asSetOfSets E') → E ⊆ E' → E' ⊆ E

Maximal compatibility is a search over the powerset of excludables.

@[instance_reducible]

instance Exhaustification.decidableIsMCSet {W : Type u_1} [Fintype W] [DecidableEq W] (ALT : Finset (Finset W)) (φ : Finset W) (E : Finset (Finset W)) : Decidable (IsMCSet (asSetOfSets ALT) (↑φ) (asSetOfSets E))

Equations

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

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

The propositions in every maximal compatible set, computed within excludables.

Equations

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

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

The innocently excludable alternatives of a finite family.

Equations

• Exhaustification.innocentlyExcludable ALT φ = {a ∈ ALT | Finset.univ \ a ∈ Exhaustification.ieFinset ALT φ}

theorem Exhaustification.innocentlyExcludable_subset {W : Type u_1} [Fintype W] [DecidableEq W] (ALT : Finset (Finset W)) (φ : Finset W) : innocentlyExcludable ALT φ ⊆ ALT

theorem Exhaustification.self_mem_ieFinset {W : Type u_1} [Fintype W] [DecidableEq W] (ALT : Finset (Finset W)) (φ : Finset W) : φ ∈ ieFinset ALT φ

The prejacent lies in every maximal compatible set.

Innocent excludability

theorem Exhaustification.isInnocentlyExcludable_iff {W : Type u_1} [Fintype W] [DecidableEq W] (ALT : Finset (Finset W)) (φ a : Finset W) : IsInnocentlyExcludable (asSetOfSets ALT) ↑φ ↑a ↔ a ∈ innocentlyExcludable ALT φ

Innocent excludability over a finite family is membership in innocentlyExcludable.

@[instance_reducible]

instance Exhaustification.decidableIsInnocentlyExcludable {W : Type u_1} [Fintype W] [DecidableEq W] (ALT : Finset (Finset W)) (φ a : Finset W) : Decidable (IsInnocentlyExcludable (asSetOfSets ALT) ↑φ ↑a)

Innocent excludability is decidable over finite families.

Equations

• Exhaustification.decidableIsInnocentlyExcludable ALT φ a = decidable_of_iff (a ∈ Exhaustification.innocentlyExcludable ALT φ) ⋯

The cell

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

The cell of the prejacent, as a Finset.

Equations

• Exhaustification.cellFinset ALT φ = {w : W | w ∈ φ ∧ (∀ a ∈ Exhaustification.innocentlyExcludable ALT φ, w ∉ a) ∧ ∀ r ∈ ALT \ Exhaustification.innocentlyExcludable ALT φ, w ∈ r}

theorem Exhaustification.mem_cellFinset_iff {W : Type u_1} [Fintype W] [DecidableEq W] (ALT : Finset (Finset W)) (φ : Finset W) (w : W) : w ∈ cellFinset ALT φ ↔ cell (asSetOfSets ALT) (↑φ) w

Membership in cellFinset is membership in the cell.

@[instance_reducible]

instance Exhaustification.decidableCell {W : Type u_1} [Fintype W] [DecidableEq W] (ALT : Finset (Finset W)) (φ : Finset W) (w : W) : Decidable (cell (asSetOfSets ALT) (↑φ) w)

The cell is decidable over finite families.

Equations

• Exhaustification.decidableCell ALT φ w = decidable_of_iff (w ∈ Exhaustification.cellFinset ALT φ) ⋯

The innocent excluder

def Exhaustification.innocent {W : Type u_2} [Fintype W] [DecidableEq W] : Excluder W

The innocent excluder ([Fox07]): innocent.exh ALT φ is exhIE over finite worlds.

Equations

• Exhaustification.innocent = { excluded := Exhaustification.innocentlyExcludable, excluded_subset := ⋯ }

theorem Exhaustification.innocent_exh_eq_phi_of_innocentlyExcludable_empty {W : Type u_1} [Fintype W] [DecidableEq W] {ALT : Finset (Finset W)} {φ : Finset W} (h : innocentlyExcludable ALT φ = ∅) : innocent.exh ALT φ = φ

With nothing innocently excludable, exhaustification is vacuous.

Tolerant exhaustification

theorem Exhaustification.tolerant_exh_eq_empty_of_covered {W : Type u_1} [Fintype W] [DecidableEq W] {ALT : Finset (Finset W)} {φ : Finset W} (h : ∀ w ∈ φ, ∃ α ∈ ALT, ¬φ ⊆ α ∧ w ∈ α) : tolerant.exh ALT φ = ∅

Tolerant exhaustification is contradictory when every prejacent world lies in a non-entailed alternative.

theorem Exhaustification.covered_of_tolerant_exh_eq_empty {W : Type u_1} [Fintype W] [DecidableEq W] {ALT : Finset (Finset W)} {φ : Finset W} (h : tolerant.exh ALT φ = ∅) (w : W) (hw : w ∈ φ) : ∃ α ∈ ALT, ¬φ ⊆ α ∧ w ∈ α

A contradictory tolerant exhaustification covers the prejacent by non-entailed alternatives.

theorem Exhaustification.tolerant_exh_eq_empty_iff {W : Type u_1} [Fintype W] [DecidableEq W] (ALT : Finset (Finset W)) (φ : Finset W) : tolerant.exh ALT φ = ∅ ↔ ∀ w ∈ φ, ∃ α ∈ ALT, ¬φ ⊆ α ∧ w ∈ α

Tolerant exhaustification is contradictory iff the non-entailed alternatives cover the prejacent.

Innocent exhaustification

theorem Exhaustification.tolerant_exh_subset_innocent_exh {W : Type u_1} [Fintype W] [DecidableEq W] (ALT : Finset (Finset W)) (φ : Finset W) : tolerant.exh ALT φ ⊆ innocent.exh ALT φ

The tolerant excluder denies every alternative the innocent one does.

theorem Exhaustification.innocent_exh_pairwise_disjoint_partial {W : Type u_1} [Fintype W] [DecidableEq W] {ALT : Finset (Finset W)} {φ : Finset W} (hcompat : (φ \ ALT.sup id).Nonempty) : innocent.exh ALT φ = φ \ ALT.sup id

When some prejacent world lies in no alternative, every alternative is innocently excludable and exhaustification removes their union.

theorem Exhaustification.innocent_exh_singleton_proper {W : Type u_1} [Fintype W] [DecidableEq W] {α φ : Finset W} (h : α ⊂ φ) : innocent.exh {α} φ = φ \ α

A single alternative strictly below the prejacent is denied.

theorem Exhaustification.innocent_exh_erase_entailed {W : Type u_1} [Fintype W] [DecidableEq W] {ALT : Finset (Finset W)} {a φ : Finset W} (h_entails : φ ⊆ a) (hphi_nonempty : φ.Nonempty) : innocent.exh ALT φ = innocent.exh (ALT.erase a) φ

An alternative entailed by the prejacent can be dropped without changing the exhaustification.

Filtering alternatives can strengthen

theorem Exhaustification.preFilter_can_create_implicature : ∃ (E : Excluder Bool) (ALT : Finset (Finset Bool)) (φ : Finset Bool) (ψ : Finset Bool) (P : Finset Bool → Bool), ¬E.exh ALT φ ⊆ ψ ∧ (E.preFilter P).exh ALT φ ⊆ ψ

Filtering the alternatives before exclusion can license an implicature the unfiltered excluder does not: removing one of two symmetric alternatives makes the other excludable ([FK11]'s formal alternative source can break symmetry).