Docs / Semantics / Exhaustification / DomainAlternatives

Domain alternatives of a modalized existential

import Linglib.Semantics.Exhaustification.DomainAlternatives · namespace Exhaustification

This file defines the modal profile of an existential claim ∃ x ∈ D, Q x evaluated under an accessibility relation from an index, a world or an event, to worlds, and the subdomain alternatives whose exhaustification strengthens it. FreeChoice holds when every member of the domain is a witness in some accessible world and ModalVariation when the witnesses vary across the accessible worlds; subdomainAlternatives lists the subdomains an item competes with — every nonempty proper subdomain for a domain widener, the singletons for an anti-singleton item — and AntiExhaustivity S is the negation of the pre-exhaustified alternative for S: if S is possible, so is the rest of the domain. Negating the pre-exhaustified singleton alternatives yields Modal Variation, and negating all proper ones is Free Choice, Chierchia's antiexhaustive enrichment of the possibility of the claim.

Main definitions

claim, witnesses — the existential over a subdomain and its witnesses at a world.
FreeChoice, ModalVariation, Uniqueness — the modal components.
subdomainAlternatives — the singleton or proper subdomain alternatives.
AntiExhaustivity — the negated pre-exhaustified alternative, for a singleton the negated exhaustification against the other members (antiExhaustivity_singleton_iff).
RealizesWitnessSets — every set of witnesses is possible at some world.

Main results

freeChoice_iff_of_isGreatest — over a domain with a greatest member and a scope closed under parts, Free Choice is the possibility of the greatest member.
notMem_exhIE_subdomain_iff — anti-exhaustivity is the negated innocent pre-exhaustification against every subdomain alternative, in a model realizing every set of witnesses.
exh_subdomain_eq_empty — without innocent exclusion that pre-exhaustification is contradictory.
freeChoice_iff_forall_antiExhaustivity — where the claim is possible, Free Choice is anti-exhaustivity for every proper subdomain.
exhIEII_singletons_eq_freeChoice — innocent exclusion and inclusion yields free choice.

References

Kratzer & Shimoyama 2002, Indeterminate Pronouns: The View from Japanese formalized
Chierchia 2006, Broaden Your Views: Implicatures of Domain Widening and the “Logicality” of Language formalized
Alonso-Ovalle & Menéndez-Benito 2010, Modal Indefinites formalized
Chierchia 2013, Logic in Grammar: Polarity, Free Choice, and Intervention formalized
Fox 2007, Free Choice and the Theory of Scalar Implicatures formalized
Bar-Lev & Fox 2020, Free Choice, Simplification, and Innocent Inclusion formalized

Declarations

The existential claim over the subdomain S says that some member of S is a witness.

def claim L66–67

{W : Type u_2} {E : Type u_3} (Q : W → E → Prop) (S : Finset E) (v : W) :

Prop

claim Q S v = ∃ x ∈ S, Q v x

Used by claim_iff_witnesses_nonempty, diamond_claim_iff, sUnion_minimal_singletons, exhIE_singletons_eq, exhIEII_singletons_eq_freeChoice, AntiExhaustivity, exists_singleton_of_diamond, two_of_singletons, modalVariation_of_singletons, modalVariation_of_box, mem_exhIE_subdomain_iff, freeChoice_iff_forall_antiExhaustivity, notMem_exhIE_subdomain_iff, freeChoice_of_forall_notMem_exhIE, exh_subdomain_eq_empty, instDecidableClaim

Used in AlonsoOvalleMenendezBenito2010, AlonsoOvalleMoghiseh2025a, AlonsoOvalleRoyer2024

Free Choice holds when every member of the domain is a witness in some accessible world.

def FreeChoice L69–70

{W' : Type u_1} {W : Type u_2} {E : Type u_3} (R : SetRel W' W) (w : W') (D : Finset E) (Q : W → E → Prop) :

Prop

FreeChoice R w D Q = ∀ x ∈ D, ModalLogic.Diamond R (fun (x_1 : W) => Q x_1 x) w

Used by freeChoice_iff_of_isGreatest, modalVariation_of_freeChoice, exhIEII_singletons_eq_freeChoice, freeChoice_iff_forall_antiExhaustivity, freeChoice_of_forall_notMem_exhIE, instDecidableFreeChoice

Used in AlonsoOvalleMenendezBenito2010, AlonsoOvalleMoghiseh2025a, AlonsoOvalleRoyer2024, Mihoc2019

Over a domain with a greatest member, such as the sums of a number-neutral noun, Free Choice for a scope closed under parts says only that the greatest member is a witness in some accessible world.

theorem freeChoice_iff_of_isGreatest L72–77

{W' : Type u_1} {W : Type u_2} {E : Type u_3} (R : SetRel W' W) (w : W') (D : Finset E) (Q : W → E → Prop) [Preorder E] {m : E} (hm : IsGreatest (↑D) m) (hQ : ∀ (v : W), IsLowerSet {x : E | Q v x}) :

FreeChoice R w D Q ↔ ModalLogic.Diamond R (fun (x : W) => Q x m) w

Built from

The witnesses of the existential claim at v.

def witnesses L83–84

{W : Type u_2} {E : Type u_3} (D : Finset E) (Q : W → E → Prop) [(v : W) → DecidablePred (Q v)] (v : W) :

Finset E

witnesses D Q v = {x ∈ D | Q v x}

Used by ModalVariation, Uniqueness, claim_iff_witnesses_nonempty, not_modalVariation_of_box_empty

Used in AlonsoOvalleMenendezBenito2010

Modal Variation holds when the witnesses vary across the accessible worlds.

def ModalVariation L86–88

{W' : Type u_1} {W : Type u_2} {E : Type u_3} (R : SetRel W' W) (w : W') (D : Finset E) (Q : W → E → Prop) [(v : W) → DecidablePred (Q v)] :

Prop

ModalVariation R w D Q = ∃ (v : W), (w, v) ∈ R ∧ ∃ (v' : W), (w, v') ∈ R ∧ witnesses D Q v ≠ witnesses D Q v'

Built from

Used by modalVariation_of_two, modalVariation_of_freeChoice, not_modalVariation_of_box_empty, modalVariation_of_singletons, modalVariation_of_box, instDecidableModalVariationOfDecidableEq

Used in AlonsoOvalleMenendezBenito2010

Uniqueness holds when each accessible world has at most one witness.

def Uniqueness L90–91

{W' : Type u_1} {W : Type u_2} {E : Type u_3} (R : SetRel W' W) (w : W') (D : Finset E) (Q : W → E → Prop) [(v : W) → DecidablePred (Q v)] :

Prop

Uniqueness R w D Q = ModalLogic.Box R (fun (v : W) => (witnesses D Q v).card ≤ 1) w

Built from

Used by modalVariation_of_two, modalVariation_of_freeChoice, modalVariation_of_singletons, instDecidableUniqueness

Used in AlonsoOvalleMenendezBenito2010

Exhaustification in a model realizing every set of witnesses

When every set of witnesses is possible at some world, the characterizations of innocent exclusion and inclusion by verified alternatives compute the exhaustified readings of a modalized existential. Against the possibility of each member, innocent exclusion is vacuous (exhIE_singletons_eq) and innocent inclusion yields free choice without pre-exhaustification (exhIEII_singletons_eq_freeChoice).

A model realizes every set of witnesses when each nonempty set of members of the domain is the set of possible witnesses at some world.

def RealizesWitnessSets L124–127

{W' : Type u_1} {W : Type u_2} {E : Type u_3} (R : SetRel W' W) (D : Finset E) (Q : W → E → Prop) :

Prop

RealizesWitnessSets R D Q = ∀ L ⊆ D, L.Nonempty → ∃ (v : W'), ∀ x ∈ D, ModalLogic.Diamond R (fun (x_1 : W) => Q x_1 x) v ↔ x ∈ L

Used by sUnion_minimal_singletons, exhIE_singletons_eq, exhIEII_singletons_eq_freeChoice, mem_exhIE_subdomain_iff, notMem_exhIE_subdomain_iff, freeChoice_of_forall_notMem_exhIE, exh_subdomain_eq_empty

L133–135

L142–155

L157–162

Against the possibility of each member, innocent exclusion and inclusion strengthens the possibility of the claim exactly to free choice, without pre-exhaustification.

theorem exhIEII_singletons_eq_freeChoice L164–184

{W' : Type u_1} {W : Type u_2} {E : Type u_3} {R : SetRel W' W} {D : Finset E} {Q : W → E → Prop} (h : RealizesWitnessSets R D Q) (hD : D.Nonempty) :

exhIEII ((fun (x : E) => {v : W' | ModalLogic.Diamond R (fun (x_1 : W) => Q x_1 x) v}) '' ↑D) {v : W' | ModalLogic.Diamond R (claim Q D) v} = {w : W' | FreeChoice R w D Q}

Built from , ,

Subdomain alternatives

L190–196

The subdomain alternatives of D.

def subdomainAlternatives L200–203

{E : Type u_3} [DecidableEq E] :

Subdomains → Finset E → Finset (Finset E)

subdomainAlternatives Subdomains.singletons x✝ = Finset.image (fun (x : E) => {x}) x✝
subdomainAlternatives Subdomains.proper x✝ = Finset.Ioo ∅ x✝

Built from

Used by subdomainAlternatives_singletons_subset, exists_singleton_of_diamond, two_of_singletons, modalVariation_of_singletons, modalVariation_of_box, mem_subdomainAlternatives_proper, singleton_mem_subdomainAlternatives_proper, mem_exhIE_subdomain_iff, freeChoice_iff_forall_antiExhaustivity, notMem_exhIE_subdomain_iff, freeChoice_of_forall_notMem_exhIE, exh_subdomain_eq_empty

Used in AlonsoOvalleMenendezBenito2010, AlonsoOvalleMoghiseh2025a

L205–211

The negated pre-exhaustified alternative for S: if S is possible, so is the rest of the domain.

def AntiExhaustivity L213–216

{W' : Type u_1} {W : Type u_2} {E : Type u_3} (R : SetRel W' W) (w : W') (D : Finset E) (Q : W → E → Prop) [DecidableEq E] (S : Finset E) :

Prop

AntiExhaustivity R w D Q S = (ModalLogic.Diamond R (claim Q S) w → ModalLogic.Diamond R (claim Q (D \ S)) w)

Built from

Used by antiExhaustivity_singleton_iff, two_of_singletons, modalVariation_of_singletons, freeChoice_iff_forall_antiExhaustivity, notMem_exhIE_subdomain_iff, instDecidableAntiExhaustivity

Used in AlonsoOvalleMenendezBenito2010

For a singleton, anti-exhaustivity negates the possibility of its member exhaustified against the possibility of each other member of the domain.

theorem antiExhaustivity_singleton_iff L218–225

{W' : Type u_1} {W : Type u_2} {E : Type u_3} (R : SetRel W' W) (w : W') (D : Finset E) (Q : W → E → Prop) [DecidableEq E] {a : E} (ha : a ∈ D) :

AntiExhaustivity R w D Q {a} ↔ ¬exhAgainst (fun (x1 x2 : ↥D) => x1 ≠ x2) (fun (x : ↥D) => ModalLogic.Diamond R (fun (x_1 : W) => Q x_1 ↑x) w) ⟨a, ha⟩

Built from

Pre-exhaustified subdomain alternatives

Innocently pre-exhaustifying the possibility of a subdomain against every subdomain alternative denies the rest of the domain, so negating it is anti-exhaustivity (notMem_exhIE_subdomain_iff) and negating them all yields free choice (freeChoice_of_forall_notMem_exhIE). Without innocent exclusion the pre-exhaustification is contradictory (exh_subdomain_eq_empty).

L272–275

L277–283

L285–340

Where the claim is possible, Free Choice is anti-exhaustivity for every proper subdomain, since both are the antiexhaustive enrichment of the possibility of the claim.

theorem freeChoice_iff_forall_antiExhaustivity L342–352

{W' : Type u_1} {W : Type u_2} {E : Type u_3} {R : SetRel W' W} {w : W'} {D : Finset E} {Q : W → E → Prop} [DecidableEq E] (h : ModalLogic.Diamond R (claim Q D) w) :

FreeChoice R w D Q ↔ ∀ S ∈ subdomainAlternatives Subdomains.proper D, AntiExhaustivity R w D Q S

Built from , , ,

Negating the innocent pre-exhaustification of a proper subdomain is its anti-exhaustivity, in a model realizing every set of witnesses.

theorem notMem_exhIE_subdomain_iff L354–361

{W' : Type u_1} {W : Type u_2} {E : Type u_3} {R : SetRel W' W} {w : W'} {D : Finset E} {Q : W → E → Prop} [DecidableEq E] {S₀ : Finset E} (h : RealizesWitnessSets R D Q) (hS₀ : S₀ ∈ subdomainAlternatives Subdomains.proper D) :

w ∉ exhIE ((fun (S : Finset E) => {v : W' | ModalLogic.Diamond R (claim Q S) v}) '' ↑(subdomainAlternatives Subdomains.proper D)) {v : W' | ModalLogic.Diamond R (claim Q S₀) v} ↔ AntiExhaustivity R w D Q S₀

Built from , , ,

L363–370

Exhaustifying the possibility of a subdomain with two members against every subdomain alternative without innocent exclusion is contradictory, in a model realizing every set of witnesses.

theorem exh_subdomain_eq_empty L372–394

{W' : Type u_1} {W : Type u_2} {E : Type u_3} {R : SetRel W' W} {D : Finset E} {Q : W → E → Prop} [DecidableEq E] {S₀ : Finset E} (h : RealizesWitnessSets R D Q) (hS₀ : S₀ ∈ subdomainAlternatives Subdomains.proper D) (h2 : 1 < S₀.card) :

exh ((fun (S : Finset E) => {v : W' | ModalLogic.Diamond R (claim Q S) v}) '' ↑(subdomainAlternatives Subdomains.proper D)) {v : W' | ModalLogic.Diamond R (claim Q S₀) v} = ∅

Built from , ,

Decidability