Exhaustification

An exhaustification operator asserts a prejacent and denies a selection of its alternatives. This file defines the selection every theory of only and of exhaustification shares, the alternatives the prejacent does not entail, and the finite excluders that vary it.

excludes C p is the exclusion component, holding where every true alternative in C is entailed by p. It is the assertion of the entailment-scale only (Focus.Particles.only), as in Horn, Rooth and von Fintel, and exh C p, the prejacent together with the exclusion, is Chierchia's operator O. Exclusion is anti-additive in the prejacent (excludes_union). Over an Irredundant family, where each alternative has a world of its own, exclusion separates resolutions of the alternative set (Irredundant.excludes_injOn), and narrowing the alternatives weakens it (excludes_antitone). Read at a world, exh against a family of alternatives is exhAgainst the members the prejacent does not entail (mem_exh_range_iff_exhAgainst), over an irredundant family every other member (Irredundant.mem_exh_range_iff). Against the image or range of an indexed family, exh denies the members the prejacent does not entail (mem_exh_image_iff), decidably over finite worlds. When the prejacent is maximal among the alternatives, exclusion is Rooth's condition that every true alternative equals the prejacent (mem_excludes_iff_forall_eq).

An Excluder is a selection over finite world types, Excluder.exh the resulting operator, and tolerant is exh there, contradiction or not, after Chierchia. Excluder.restrict keeps only the relevant alternatives among those an excluder denies, after Magri, and can only weaken the result, while Excluder.preFilter removes alternatives before the excluder sees them and can strengthen it, the asymmetry Fox and Katzir state between contextual restriction and the formal alternative source. The innocent excluder is innocent in Finite.

References

• [Hor69]
• [Roo92]
• [vF99a]
• [Chi06]
• [Chi13]
• [Fox07]
• [FK11]
• [Mag09]

Exclusion and exhaustification

def Exhaustification.excludes {W : Type u_1} (C : Set (Set W)) (p : Set W) : Set W

excludes C p holds at the worlds where every true alternative in C is entailed by p.

Equations

• Exhaustification.excludes C p = {w : W | ∀ q ∈ C, w ∈ q → p ⊆ q}

@[simp]

theorem Exhaustification.mem_excludes {W : Type u_1} {C : Set (Set W)} {p : Set W} {w : W} : w ∈ excludes C p ↔ ∀ q ∈ C, w ∈ q → p ⊆ q

def Exhaustification.exh {W : Type u_1} (C : Set (Set W)) (p : Set W) : Set W

The prejacent p with every alternative it does not entail denied ([Chi06]'s O).

Equations

• Exhaustification.exh C p = p ∩ Exhaustification.excludes C p

@[simp]

theorem Exhaustification.mem_exh {W : Type u_1} {C : Set (Set W)} {p : Set W} {w : W} : w ∈ exh C p ↔ w ∈ p ∧ ∀ q ∈ C, w ∈ q → p ⊆ q

theorem Exhaustification.exh_subset {W : Type u_1} (C : Set (Set W)) (p : Set W) : exh C p ⊆ p

theorem Exhaustification.exh_subset_excludes {W : Type u_1} (C : Set (Set W)) (p : Set W) : exh C p ⊆ excludes C p

theorem Exhaustification.notMem_excludes {W : Type u_1} {C : Set (Set W)} {p q : Set W} {w : W} (hq : q ∈ C) (hw : w ∈ q) (h : ¬p ⊆ q) : w ∉ excludes C p

A true alternative the prejacent does not entail is excluded.

theorem Exhaustification.notMem_exh {W : Type u_1} {C : Set (Set W)} {p q : Set W} {w : W} (hq : q ∈ C) (hw : w ∈ q) (h : ¬p ⊆ q) : w ∉ exh C p

theorem Exhaustification.exh_subset_compl {W : Type u_1} {C : Set (Set W)} {p q : Set W} (hq : q ∈ C) (h : ¬p ⊆ q) : exh C p ⊆ qᶜ

Exhaustification denies every alternative the prejacent does not entail.

theorem Exhaustification.mem_exh_image_iff {W : Type u_1} {p : Set W} {w : W} {ι : Type u_2} {f : ι → Set W} {A : Set ι} : w ∈ exh (f '' A) p ↔ w ∈ p ∧ ∀ i ∈ A, w ∈ f i → p ⊆ f i

Against the image of an indexed family, exhaustification denies the members the prejacent does not entail.

theorem Exhaustification.mem_exh_range_iff {W : Type u_1} {p : Set W} {w : W} {ι : Type u_2} {f : ι → Set W} : w ∈ exh (Set.range f) p ↔ w ∈ p ∧ ∀ (i : ι), w ∈ f i → p ⊆ f i

Against the range of an indexed family, exhaustification denies the members the prejacent does not entail.

@[instance_reducible]

instance Exhaustification.instDecidablePredMemSetExhImageOfFintype {W : Type u_1} [Fintype W] {ι : Type u_2} [Fintype ι] {f : ι → Set W} [(i : ι) → DecidablePred fun (x : W) => x ∈ f i] {A : Set ι} [DecidablePred fun (x : ι) => x ∈ A] {p : Set W} [DecidablePred fun (x : W) => x ∈ p] : DecidablePred fun (x : W) => x ∈ exh (f '' A) p

Over finite worlds and indices, exhaustifying against an indexed family is decidable.

Equations

• Exhaustification.instDecidablePredMemSetExhImageOfFintype w = decidable_of_iff (w ∈ p ∧ ∀ i ∈ A, w ∈ f i → ∀ x ∈ p, x ∈ f i) ⋯

@[instance_reducible]

instance Exhaustification.instDecidablePredMemSetExhRangeOfFintype {W : Type u_1} [Fintype W] {ι : Type u_2} [Fintype ι] {f : ι → Set W} [(i : ι) → DecidablePred fun (x : W) => x ∈ f i] {p : Set W} [DecidablePred fun (x : W) => x ∈ p] : DecidablePred fun (x : W) => x ∈ exh (Set.range f) p

Equations

• Exhaustification.instDecidablePredMemSetExhRangeOfFintype w = decidable_of_iff (w ∈ p ∧ ∀ (i : ι), w ∈ f i → ∀ x ∈ p, x ∈ f i) ⋯

theorem Exhaustification.mem_excludes_of_forall_notMem {W : Type u_1} {C : Set (Set W)} {p : Set W} {w : W} (h : ∀ q ∈ C, ¬p ⊆ q → w ∉ q) : w ∈ excludes C p

Exclusion from refuting every alternative the prejacent does not entail.

theorem Exhaustification.excludes_eq_compl_sUnion {W : Type u_1} (C : Set (Set W)) (p : Set W) : excludes C p = (⋃₀ {q : Set W | q ∈ C ∧ ¬p ⊆ q})ᶜ

Exclusion denies the union of the alternatives the prejacent does not entail.

theorem Exhaustification.exh_eq_sdiff {W : Type u_1} (C : Set (Set W)) (p : Set W) : exh C p = p \ ⋃₀ {q : Set W | q ∈ C ∧ ¬p ⊆ q}

theorem Exhaustification.exh_eq_self_iff {W : Type u_1} {C : Set (Set W)} {p : Set W} : exh C p = p ↔ ∀ q ∈ C, (p ∩ q).Nonempty → p ⊆ q

Exhaustification is vacuous exactly when every alternative compatible with the prejacent is entailed by it.

theorem Exhaustification.exh_eq_self {W : Type u_1} {C : Set (Set W)} {p : Set W} (h : ∀ q ∈ C, p ⊆ q) : exh C p = p

Exhaustification cannot exhaustify away entailments.

theorem Exhaustification.excludes_antitone {W : Type u_1} {C C' : Set (Set W)} (h : C ⊆ C') (p : Set W) : excludes C' p ⊆ excludes C p

Narrowing the alternatives weakens the exclusion.

theorem Exhaustification.exh_antitone {W : Type u_1} {C C' : Set (Set W)} (h : C ⊆ C') (p : Set W) : exh C' p ⊆ exh C p

theorem Exhaustification.antitone_excludes {W : Type u_1} (C : Set (Set W)) : Antitone (excludes C)

Strengthening the prejacent strengthens the exclusion.

theorem Exhaustification.excludes_union {W : Type u_1} (C : Set (Set W)) (p q : Set W) : excludes C (p ∪ q) = excludes C p ∩ excludes C q

Exclusion is anti-additive in the prejacent.

theorem Exhaustification.mem_excludes_iff_forall_eq {W : Type u_1} {C : Set (Set W)} {p : Set W} {w : W} (h : ∀ q ∈ C, p ⊆ q → q = p) : w ∈ excludes C p ↔ ∀ q ∈ C, w ∈ q → q = p

When the prejacent is maximal among the alternatives, exclusion asks that every true alternative be the prejacent itself, [Roo92]'s semantics of only.

Irredundant alternatives

def Exhaustification.Irredundant {W : Type u_1} {ι : Type u_2} (f : ι → Set W) : Prop

A family of alternatives is irredundant when each member can hold while every other member fails, so that no member is covered by the union of the rest. Strictly weaker than the mutual exclusivity of partition semantics (irredundant_of_pairwise_disjoint).

Equations

• Exhaustification.Irredundant f = ∀ (i : ι), ∃ w ∈ f i, ∀ (j : ι), j ≠ i → w ∉ f j

theorem Exhaustification.irredundant_of_pairwise_disjoint {W : Type u_1} {ι : Type u_2} {f : ι → Set W} (hd : Pairwise fun (i j : ι) => Disjoint (f i) (f j)) (hne : ∀ (i : ι), (f i).Nonempty) : Irredundant f

Pairwise-disjoint nonempty alternatives are irredundant.

theorem Exhaustification.Irredundant.not_subset {W : Type u_1} {ι : Type u_2} {f : ι → Set W} (hf : Irredundant f) {i j : ι} (hij : i ≠ j) : ¬f i ⊆ f j

No member of an irredundant family entails another.

theorem Exhaustification.Irredundant.excludes_ne {W : Type u_1} {ι : Type u_2} {f : ι → Set W} (hf : Irredundant f) {i₀ j : ι} {s₁ s₂ : Finset ι} (hj₂ : j ∈ s₂) (hj₁ : j ∉ s₁) (hji : j ≠ i₀) : excludes (f '' ↑s₁) (f i₀) ≠ excludes (f '' ↑s₂) (f i₀)

Over an irredundant family, resolving the exclusion to alternative sets that differ beyond the prejacent yields distinct propositions, since the alternative present in one resolution and absent from the other separates them.

theorem Exhaustification.Irredundant.excludes_injOn {W : Type u_1} {ι : Type u_2} {f : ι → Set W} (hf : Irredundant f) (i₀ : ι) : Set.InjOn (fun (s : Finset ι) => excludes (f '' ↑s) (f i₀)) {s : Finset ι | i₀ ∈ s}

Over an irredundant family, exclusion is injective in the resolved alternative set, on resolutions containing the prejacent.

theorem Exhaustification.mem_exh_range_iff_exhAgainst {W : Type u_1} {ι : Type u_2} (f : ι → Set W) (i : ι) (w : W) : w ∈ exh (Set.range f) (f i) ↔ exhAgainst (fun (i j : ι) => ¬f i ⊆ f j) (fun (x : ι) => w ∈ f x) i

Exhaustifying a member of a family against the family denies exactly the members it does not entail.

theorem Exhaustification.Irredundant.mem_exh_range_iff {W : Type u_1} {ι : Type u_2} {f : ι → Set W} (hf : Irredundant f) (i : ι) (w : W) : w ∈ exh (Set.range f) (f i) ↔ exhAgainst (fun (x1 x2 : ι) => x1 ≠ x2) (fun (x : ι) => w ∈ f x) i

Over an irredundant family a member entails no other, so exhaustifying against the family is exhaustifying against independent rivals.

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

The worlds satisfying a Bool predicate.

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)

The alternative set of a list of Bool predicates.

Equations

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

@[simp]

theorem Exhaustification.altsFromPreds_singleton {W : Type u_1} [Fintype W] [DecidableEq W] (p : W → Bool) : altsFromPreds [p] = {predToFinset p}

altsFromPreds [p] is the singleton {predToFinset p}.

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

A choice, for each alternative set and prejacent, of the alternatives to deny.

• 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

The prejacent with every excluded alternative denied.

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.

Restricting the excluded alternatives

def Exhaustification.Excluder.restrict {W : Type u_1} [Fintype W] [DecidableEq W] (E : Excluder W) (R : Finset W → Bool) : Excluder W

Deny only the excluded alternatives satisfying R.

Equations

• E.restrict R = { excluded := fun (ALT : Finset (Finset W)) (φ : Finset W) => {a ∈ E.excluded ALT φ | R a = true}, excluded_subset := ⋯ }

@[simp]

theorem Exhaustification.Excluder.restrict_excluded {W : Type u_1} [Fintype W] [DecidableEq W] (E : Excluder W) (R : Finset W → Bool) (ALT : Finset (Finset W)) (φ : Finset W) : (E.restrict R).excluded ALT φ = {a ∈ E.excluded ALT φ | R a = true}

theorem Exhaustification.Excluder.restrict_const_true {W : Type u_1} [Fintype W] [DecidableEq W] (E : Excluder W) : (E.restrict fun (x : Finset W) => true) = E

A constantly-true relevance predicate leaves the excluder unchanged.

theorem Exhaustification.Excluder.exh_subset_restrict_exh {W : Type u_1} [Fintype W] [DecidableEq W] (E : Excluder W) (R : Finset W → Bool) (ALT : Finset (Finset W)) (φ : Finset W) : E.exh ALT φ ⊆ (E.restrict R).exh ALT φ

Restriction weakens the exhaustification.

theorem Exhaustification.Excluder.restrict_preserves_no_implicature {W : Type u_1} [Fintype W] [DecidableEq W] (E : Excluder W) (R : Finset W → Bool) (ALT : Finset (Finset W)) (φ ψ : Finset W) (h : ¬E.exh ALT φ ⊆ ψ) : ¬(E.restrict R).exh ALT φ ⊆ ψ

Restriction licenses no implicature the excluder does not ([FK11]'s contextual restriction cannot break symmetry).

Filtering the offered alternatives

def Exhaustification.Excluder.preFilter {W : Type u_1} [Fintype W] [DecidableEq W] (E : Excluder W) (P : Finset W → Bool) : Excluder W

Offer the excluder only the alternatives satisfying P.

Equations

• E.preFilter P = { excluded := fun (ALT : Finset (Finset W)) (φ : Finset W) => E.excluded ({a ∈ ALT | P a = true}) φ, excluded_subset := ⋯ }

@[simp]

theorem Exhaustification.Excluder.preFilter_excluded {W : Type u_1} [Fintype W] [DecidableEq W] (E : Excluder W) (P : Finset W → Bool) (ALT : Finset (Finset W)) (φ : Finset W) : (E.preFilter P).excluded ALT φ = E.excluded ({a ∈ ALT | P a = true}) φ

theorem Exhaustification.Excluder.preFilter_const_true {W : Type u_1} [Fintype W] [DecidableEq W] (E : Excluder W) : (E.preFilter fun (x : Finset W) => true) = E

A constantly-true pre-filter leaves the excluder unchanged.

The tolerant excluder

def Exhaustification.tolerant {W : Type u_1} [Fintype W] [DecidableEq W] : Excluder W

The tolerant excluder denies every alternative not entailed by the prejacent.

Equations

• Exhaustification.tolerant = { excluded := fun (ALT : Finset (Finset W)) (φ : Finset W) => {a ∈ ALT | ¬φ ⊆ a}, excluded_subset := ⋯ }

@[simp]

theorem Exhaustification.tolerant_excluded {W : Type u_1} [Fintype W] [DecidableEq W] (ALT : Finset (Finset W)) (φ : Finset W) : tolerant.excluded ALT φ = {a ∈ ALT | ¬φ ⊆ a}

theorem Exhaustification.mem_tolerant_excluded {W : Type u_1} [Fintype W] [DecidableEq W] {ALT : Finset (Finset W)} {φ a : Finset W} : a ∈ tolerant.excluded ALT φ ↔ a ∈ ALT ∧ ¬φ ⊆ a

theorem Exhaustification.mem_tolerant_exh_iff {W : Type u_1} [Fintype W] [DecidableEq W] (ALT : Finset (Finset W)) (φ : Finset W) {w : W} : w ∈ tolerant.exh ALT φ ↔ w ∈ φ ∧ ∀ a ∈ ALT, ¬φ ⊆ a → w ∉ a

Membership in the tolerant exhaustification.

theorem Exhaustification.entailed_not_excluded {W : Type u_1} [Fintype W] [DecidableEq W] {ALT : Finset (Finset W)} {φ a : Finset W} (h : φ ⊆ a) : a ∉ tolerant.excluded ALT φ

Alternatives entailed by the prejacent are kept, never negated.