Docs / Semantics / Exhaustification / Antiexhaustive

Antiexhaustive enrichment

import Linglib.Semantics.Exhaustification.Antiexhaustive · namespace Exhaustification

Source

This file defines Chierchia's antiexhaustive enrichment antiExh F D of a proposition F that depends on a domain: F D holds, and F holds of no nonempty subdomain without holding of every nonempty subdomain disjoint from it. The implicature is a zero-one law: the alternatives over the nonempty proper subdomains are all true or all false. Over an existential only the first case is consistent, which gives universal force over the domain; under an antitone operator the enrichment is vacuous; under a necessity modal the second case makes every member an option.

Main statements

References

Declarations

The antiexhaustive enrichment O⁻ of the domain-dependent proposition F over the domain D, (108c), holds where F D holds and F holds of no nonempty subdomain without holding of every nonempty subdomain disjoint from it.

def antiExhL37–41
{W : Type u_1} {E : Type u_2} (F : Finset E → Set W) (D : Finset E) :
Set W
  • antiExh F D = F D ∩ {w : W | ∀ S ⊆ D, ∀ T ⊆ D, S.Nonempty → T.Nonempty → Disjoint S T → w ∈ F S → w ∈ F T}

Used by antiExh_subset, mem_iff_mem_of_mem_antiExh, notMem_antiExh_of_singleton, mem_antiExh_iff, antiExh_eq_self, antiExh_biUnion, mem_antiExh_biUnion_iff, antiExh_biUnion_eq_inter_sInter, antiExh_eq_of_antitone, not_antiExh_ssubset_of_antitone, antiExh_ssubset, antiExh_preimage_biUnion, antiExh_core_biUnion_inter_dom_subset

Used in Chierchia2006

L43
L45–51
L53–55

The antiexhaustive implicature is a zero-one law: the alternatives over the nonempty proper subdomains are all true or all false.

theorem mem_antiExh_iffL62–76
{W : Type u_1} {E : Type u_2} {F : Finset E → Set W} {D : Finset E} {w : W} :
w ∈ antiExh F D ↔ w ∈ F D ∧ ((∀ S ⊂ D, S.Nonempty → w ∈ F S) ∨ ∀ S ⊂ D, S.Nonempty → w ∉ F S)

Built from

L78–81

Antiexhaustive enrichment gives an existential universal force over its domain, (63c)–(63d), which negation over σ denies, (64).

theorem antiExh_biUnionL85–95
{W : Type u_1} {E : Type u_2} {D : Finset E} (P : E → Set W) (hD : D.Nonempty) :
antiExh (fun (S : Finset E) => ⋃ a ∈ S, P a) D = ⋂ a ∈ D, P a

Built from

L97–112
L114–121

With σ over negation, (65)–(66), the statement entails every variant, so the free-choice implicature vanishes and any acts as a negative-polarity item.

theorem antiExh_eq_of_antitoneL123–127
{W : Type u_1} {E : Type u_2} {D : Finset E} (P : E → Set W) {C : Set W → Set W} (hC : Antitone C) :
antiExh (fun (S : Finset E) => C (⋃ a ∈ S, P a)) D = C (⋃ a ∈ D, P a)

Built from

L129–134
L136–140
L142–147
L149–161