Pre-exhaustified alternatives and proper strengthening

[Chi13] [Fox07]

The grammatical theory of implicature negates pre-exhaustified domain alternatives: each alternative strengthened against its rivals before being negated. For a family A : ι → Prop, the pre-exhaustification of A i is "A i and no rival holds" — i.e. A i holds uniquely. Negating every pre-exhaustified alternative is therefore exactly the claim that no alternative holds uniquely (forall_not_preExh_iff): the combinatorial core of free-choice effects — plain, modal ([Chi13]), and epistemic (ignorance inferences, [Mih19]) — where the assertion supplies "at least one region is live" and unique-truth failure spreads possibility across all of them.

ProperlyStrengthens names the requirement some items impose on their exhaustification: the result must be strictly stronger than the prejacent. When every alternative is individually inconsistent with the prejacent, exhaustification is vacuous and the requirement fails (not_properlyStrengthens_of_iff) — the engine of anti-negativity (positive-polarity) verdicts.

Main definitions

• preExh: an alternative strengthened against its rivals
• ProperlyStrengthens: strict strengthening of a prejacent

Main results

• exists_preExh_iff_existsUnique, forall_not_preExh_iff: negating all pre-exhaustified alternatives = no alternative holds uniquely
• not_properlyStrengthens_of_iff: vacuous exhaustification fails proper strengthening

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

Pre-exhaustification of alternative i against its rivals: A i holds and no distinct alternative does.

Equations

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

@[implicit_reducible]

instance Exhaustification.instDecidablePreExhOfDecidableEqOfFintype {ι : Type u_1} {A : ι → Prop} [DecidableEq ι] [Fintype ι] [(i : ι) → Decidable (A i)] (i : ι) : Decidable (preExh A i)

Equations

• Exhaustification.instDecidablePreExhOfDecidableEqOfFintype i = Exhaustification.instDecidablePreExhOfDecidableEqOfFintype._aux_1 i

theorem Exhaustification.exists_preExh_iff_existsUnique {ι : Type u_1} {A : ι → Prop} : (∃ (i : ι), preExh A i) ↔ ∃! i : ι, A i

Some alternative is pre-exhaustifiedly true iff some alternative is uniquely true.

theorem Exhaustification.forall_not_preExh_iff {ι : Type u_1} {A : ι → Prop} : (∀ (i : ι), ¬preExh A i) ↔ ¬∃! i : ι, A i

Negating every pre-exhaustified alternative is exactly the denial that any alternative holds uniquely.

def Exhaustification.ProperlyStrengthens {α : Type u_2} (strong weak : α → Prop) : Prop

strong properly strengthens weak: it entails it, and excludes some possibility weak leaves open.

Equations

• Exhaustification.ProperlyStrengthens strong weak = ((∀ (x : α), strong x → weak x) ∧ ∃ (x : α), weak x ∧ ¬strong x)

theorem Exhaustification.not_properlyStrengthens_of_iff {α : Type u_2} {strong weak : α → Prop} (h : ∀ (x : α), strong x ↔ weak x) : ¬ProperlyStrengthens strong weak

Vacuous exhaustification — the strengthened meaning coincides with the prejacent — fails the proper-strengthening requirement.