Exhaustification over entailment chains

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

Scalar alternatives typically form an entailment chain: a family φ : ι → W → Prop over an ordered index, antitone in the index (higher index = stronger alternative). Exhaustifying a prejacent φ i against all stronger alternatives (exhChain) then collapses to negating the single next-stronger alternative, when one exists (exhChain_iff_succ); on a dense scale with no next alternative, exhaustification cannot be satisfied at all (exhChain_not_of_dense — [FH06b]'s Universal Density of Measurement crash).

The two lemmas are the two halves of one case split — does a next-stronger alternative exist? — instantiated across the numeral literature: Semantics.Numerals.exhNumeral (Horn's 'exactly', the step-1 instance on ℕ), granularity-g scalar alternatives in both bound directions (Studies/Mihoc2019), the dense crash (Studies/FoxHackl2006Numerals), and grain-size-indexed precisification families ([TD20]'s approximative just).

Main definitions

• exhChain: assert the prejacent, negate every strictly stronger alternative of the chain

Main results

• exhChain_iff_succ: on a chain, exhaustification = negating the next-stronger alternative
• exhChain_not_of_dense: with no next-stronger alternative, exhaustification is unsatisfiable

def Exhaustification.exhChain {ι : Type u_1} {W : Type u_2} [Preorder ι] (φ : ι → W → Prop) (i : ι) (w : W) : Prop

Exhaustification of the prejacent φ i against all strictly stronger alternatives of the family: assert φ i, negate φ j for every j > i.

Equations

• Exhaustification.exhChain φ i w = (φ i w ∧ ∀ (j : ι), i < j → ¬φ j w)

@[implicit_reducible]

instance Exhaustification.instDecidableExhChainOfDecidableEqOfFintypeOfDecidableLT {ι : Type u_1} {W : Type u_2} [Preorder ι] {φ : ι → W → Prop} {i : ι} {w : W} [DecidableEq ι] [Fintype ι] [DecidableLT ι] [(j : ι) → Decidable (φ j w)] : Decidable (exhChain φ i w)

Equations

• Exhaustification.instDecidableExhChainOfDecidableEqOfFintypeOfDecidableLT = Exhaustification.instDecidableExhChainOfDecidableEqOfFintypeOfDecidableLT._aux_1

theorem Exhaustification.exhChain_iff_succ {ι : Type u_1} {W : Type u_2} [Preorder ι] {φ : ι → W → Prop} {i s : ι} {w : W} (hanti : ∀ ⦃j k : ι⦄, j ≤ k → ∀ (w : W), φ k w → φ j w) (his : i < s) (hleast : ∀ (j : ι), i < j → s ≤ j) : exhChain φ i w ↔ φ i w ∧ ¬φ s w

On an entailment chain — the family is antitone, so higher alternatives entail lower ones — exhaustification collapses to negating the next-stronger alternative: if s lies above i and below every other index above i, then negating φ s negates the whole upper set.

theorem Exhaustification.exhChain_not_of_dense {ι : Type u_1} {W : Type u_2} [Preorder ι] {φ : ι → W → Prop} {i : ι} {w : W} (hdense : ∀ (w : W), φ i w → ∃ (j : ι), i < j ∧ φ j w) : ¬exhChain φ i w

If every world verifying the prejacent verifies some strictly stronger alternative — as on a dense scale — chain-exhaustification is unsatisfiable: the [FH06b] density crash.