Pre-exhaustified alternatives

The grammatical theory of implicature negates pre-exhaustified subdomain alternatives, each alternative exhaustified against the alternative set before it is negated. preExhaustify O C collects the alternatives of C, each exhaustified by the operator O against C. Chierchia uses innocent exclusion, which Excluder.preExhaustify computes over finite worlds (asSetOfSets_preExhaustify_innocent). Over an irredundant family a pre-exhaustified alternative holds just where its own member holds and no other does (Irredundant.mem_exh_range_iff), the form exhAgainst (· ≠ ·) in which papers negate them under a modal.

Main definitions

• Exhaustification.preExhaustify: each alternative exhaustified against the set.
• Exhaustification.Excluder.preExhaustify: the same over finite worlds.

References

• [Chi13]
• [Fox07]

def Exhaustification.preExhaustify {W : Type u_1} (O : Set (Set W) → Set W → Set W) (C : Set (Set W)) : Set (Set W)

The alternatives of C, each exhaustified by O against C.

Equations

• Exhaustification.preExhaustify O C = O C '' C

def Exhaustification.Excluder.preExhaustify {W : Type u_1} [Fintype W] [DecidableEq W] (E : Excluder W) (ALT : Finset (Finset W)) : Finset (Finset W)

The alternatives of ALT, each exhaustified by the excluder E against ALT.

Equations

• E.preExhaustify ALT = Finset.image (E.exh ALT) ALT

theorem Exhaustification.asSetOfSets_preExhaustify_innocent {W : Type u_1} [Fintype W] [DecidableEq W] (ALT : Finset (Finset W)) : asSetOfSets (innocent.preExhaustify ALT) = preExhaustify exhIE (asSetOfSets ALT)

Pre-exhaustifying by the innocent excluder is pre-exhaustifying by innocent exclusion.