Pointwise exhaustification

Exhaustifying the member A i of a family of alternatives against a relation r asserts A i and denies each A j with r i j. Against the members the prejacent does not entail it is exh read at a world, in any model (Exhaustification.mem_exh_range_iff_exhAgainst); a theory that fixes which alternatives count as stronger states that relation outright, and its results then hold in every model. Against every other member it is pre-exhaustification against independent rivals, which holds of some member exactly when one member holds. Against the larger indices of a scale it denies just the next-stronger alternative on an entailment chain (exhAgainst_lt_iff_succ), and on a dense scale it cannot be satisfied, the crash Fox and Hackl derive for more than.

Main definitions

• Exhaustification.exhAgainst: assert a member of a family and deny its rivals.

Main results

• Exhaustification.exists_exhAgainst_ne_iff_existsUnique: against independent rivals, some member is exhaustified iff exactly one member holds.
• Exhaustification.exhAgainst_lt_iff_succ: on an entailment chain, exhaustification denies the next-stronger alternative.

References

• [Hor72]
• [Fox07]
• [FH06b]
• [Chi13]

def Exhaustification.exhAgainst {ι : Type u_1} (r : ι → ι → Prop) (A : ι → Prop) (i : ι) : Prop

Exhaustifying the member A i against the relation r asserts A i and denies every A j with r i j.

Equations

• Exhaustification.exhAgainst r A i = (A i ∧ ∀ (j : ι), r i j → ¬A j)

@[instance_reducible]

instance Exhaustification.instDecidableExhAgainstOfFintypeOfDecidableRelOfDecidablePred {ι : Type u_1} {r : ι → ι → Prop} {A : ι → Prop} {i : ι} [Fintype ι] [DecidableRel r] [DecidablePred A] : Decidable (exhAgainst r A i)

Equations

• Exhaustification.instDecidableExhAgainstOfFintypeOfDecidableRelOfDecidablePred = { decide := decide (A i) && decide (∀ (x : ι), r i x → ¬A x), reflects_decide := ⋯ }

Independent rivals

theorem Exhaustification.exists_exhAgainst_ne_iff_existsUnique {ι : Type u_1} {A : ι → Prop} : (∃ (i : ι), exhAgainst (fun (x1 x2 : ι) => x1 ≠ x2) A i) ↔ ∃! i : ι, A i

Some member is exhaustified against all the others iff exactly one member holds.

theorem Exhaustification.forall_not_exhAgainst_ne_iff {ι : Type u_1} {A : ι → Prop} : (∀ (i : ι), ¬exhAgainst (fun (x1 x2 : ι) => x1 ≠ x2) A i) ↔ ¬∃! i : ι, A i

Negating every member exhaustified against the others denies that exactly one holds.

Scales

theorem Exhaustification.exhAgainst_lt_iff_succ {ι : Type u_1} {A : ι → Prop} {i s : ι} [Preorder ι] (hA : Antitone A) (his : i < s) (hleast : ∀ (j : ι), i < j → s ≤ j) : exhAgainst (fun (x1 x2 : ι) => x1 < x2) A i ↔ A i ∧ ¬A s

On an entailment chain, exhaustifying A i against the stronger alternatives denies just the next-stronger one A s.

theorem Exhaustification.exhAgainst_lt_iff_succOrder {ι : Type u_1} {A : ι → Prop} {i : ι} [Preorder ι] [SuccOrder ι] [NoMaxOrder ι] (hA : Antitone A) : exhAgainst (fun (x1 x2 : ι) => x1 < x2) A i ↔ A i ∧ ¬A (Order.succ i)

On an entailment chain with successors, exhaustification denies the successor.

theorem Exhaustification.not_exhAgainst_lt_of_dense {ι : Type u_1} {A : ι → Prop} {i : ι} [Preorder ι] (hdense : A i → ∃ (j : ι), i < j ∧ A j) : ¬exhAgainst (fun (x1 x2 : ι) => x1 < x2) A i

Exhaustification cannot be satisfied when the prejacent always has a stronger true alternative, as on a dense scale.