Domain alternatives of a modalized existential

This file defines the modal profile of an existential claim ∃ x ∈ D, Q x evaluated under a Kripke accessibility relation, 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 yields Free Choice.

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.

References

• [kratzer-shimoyama-2002]
• [alonso-ovalle-menendez-benito-2010]
• [Chi13]

def Exhaustification.claim {W : Type u_1} {E : Type u_2} (Q : W → E → Prop) (S : Finset E) (v : W) : Prop

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

Equations

• Exhaustification.claim Q S v = ∃ x ∈ S, Q v x

def Exhaustification.FreeChoice {W : Type u_1} {E : Type u_2} (R : W → W → Prop) (w : W) (D : Finset E) (Q : W → E → Prop) : Prop

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

Equations

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

def Exhaustification.witnesses {W : Type u_1} {E : Type u_2} (D : Finset E) (Q : W → E → Prop) [(v : W) → DecidablePred (Q v)] (v : W) : Finset E

The witnesses of the existential claim at v.

Equations

• Exhaustification.witnesses D Q v = {x ∈ D | Q v x}

def Exhaustification.ModalVariation {W : Type u_1} {E : Type u_2} (R : W → W → Prop) (w : W) (D : Finset E) (Q : W → E → Prop) [(v : W) → DecidablePred (Q v)] : Prop

Modal Variation: the witnesses vary across the accessible worlds.

Equations

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

def Exhaustification.Uniqueness {W : Type u_1} {E : Type u_2} (R : W → W → Prop) (w : W) (D : Finset E) (Q : W → E → Prop) [(v : W) → DecidablePred (Q v)] : Prop

Uniqueness: at most one witness in each accessible world.

Equations

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

theorem Exhaustification.claim_iff_witnesses_nonempty {W : Type u_1} {E : Type u_2} (D : Finset E) (Q : W → E → Prop) [(v : W) → DecidablePred (Q v)] (v : W) : claim Q D v ↔ (witnesses D Q v).Nonempty

theorem Exhaustification.modalVariation_of_two {W : Type u_1} {E : Type u_2} (R : W → W → Prop) (w : W) (D : Finset E) (Q : W → E → Prop) [(v : W) → DecidablePred (Q v)] (hU : Uniqueness R w D Q) {a b : E} (ha : a ∈ D) (hb : b ∈ D) (hab : a ≠ b) (pa : ModalLogic.diamond R (fun (x : W) => Q x a) w) (pb : ModalLogic.diamond R (fun (x : W) => Q x b) w) : ModalVariation R w D Q

Two distinct possibilities give Modal Variation under uniqueness.

theorem Exhaustification.modalVariation_of_freeChoice {W : Type u_1} {E : Type u_2} (R : W → W → Prop) (w : W) (D : Finset E) (Q : W → E → Prop) [(v : W) → DecidablePred (Q v)] (hU : Uniqueness R w D Q) (hD : 1 < D.card) (h : FreeChoice R w D Q) : ModalVariation R w D Q

Under uniqueness, Free Choice on a domain with two members entails Modal Variation.

theorem Exhaustification.not_modalVariation_of_box_empty {W : Type u_1} {E : Type u_2} (R : W → W → Prop) (w : W) (D : Finset E) (Q : W → E → Prop) [(v : W) → DecidablePred (Q v)] (h : ModalLogic.box R (fun (v : W) => witnesses D Q v = ∅) w) : ¬ModalVariation R w D Q

Modal Variation fails when no accessible world has a witness.

Subdomain alternatives

inductive Exhaustification.Subdomains : Type

Which subdomains of the domain an item competes with.

• proper : Subdomains

  Every nonempty proper subdomain, for a domain widener.

• singletons : Subdomains

  The singleton subdomains, for an anti-singleton item.

@[instance_reducible]

instance Exhaustification.instDecidableEqSubdomains : DecidableEq Subdomains

Equations

• Exhaustification.instDecidableEqSubdomains x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Exhaustification.subdomainAlternatives {E : Type u_2} [DecidableEq E] : Subdomains → Finset E → Finset (Finset E)

The subdomain alternatives of D.

Equations

• Exhaustification.subdomainAlternatives Exhaustification.Subdomains.singletons x✝ = Finset.image (fun (x : E) => {x}) x✝
• Exhaustification.subdomainAlternatives Exhaustification.Subdomains.proper x✝ = {S ∈ x✝.powerset | S.Nonempty ∧ S ≠ x✝}

theorem Exhaustification.subdomainAlternatives_singletons_subset {E : Type u_2} (D : Finset E) [DecidableEq E] (hD : 1 < D.card) : subdomainAlternatives Subdomains.singletons D ⊆ subdomainAlternatives Subdomains.proper D

The singleton alternatives are among the proper ones.

def Exhaustification.AntiExhaustivity {W : Type u_1} {E : Type u_2} (R : W → W → Prop) (w : W) (D : Finset E) (Q : W → E → Prop) [DecidableEq E] (S : Finset E) : Prop

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

Equations

• Exhaustification.AntiExhaustivity R w D Q S = (ModalLogic.diamond R (Exhaustification.claim Q S) w → ModalLogic.diamond R (Exhaustification.claim Q (D \ S)) w)

theorem Exhaustification.exists_singleton_of_diamond {W : Type u_1} {E : Type u_2} (R : W → W → Prop) (w : W) (D : Finset E) (Q : W → E → Prop) [DecidableEq E] (h : ModalLogic.diamond R (claim Q D) w) : ∃ S ∈ subdomainAlternatives Subdomains.singletons D, ModalLogic.diamond R (claim Q S) w

Under a possibility modal the claim entails one of its singleton alternatives.

theorem Exhaustification.two_of_singletons {W : Type u_1} {E : Type u_2} (R : W → W → Prop) (w : W) (D : Finset E) (Q : W → E → Prop) [DecidableEq E] (h : ModalLogic.diamond R (claim Q D) w) (hs : ∀ S ∈ subdomainAlternatives Subdomains.singletons D, AntiExhaustivity R w D Q S) : ∃ a ∈ D, ∃ b ∈ D, a ≠ b ∧ ModalLogic.diamond R (fun (x : W) => Q x a) w ∧ ModalLogic.diamond R (fun (x : W) => Q x b) w

Negating the pre-exhaustified singleton alternatives makes at least two members possibilities.

theorem Exhaustification.modalVariation_of_singletons {W : Type u_1} {E : Type u_2} (R : W → W → Prop) (w : W) (D : Finset E) (Q : W → E → Prop) [DecidableEq E] [(v : W) → DecidablePred (Q v)] (hU : Uniqueness R w D Q) (h : ModalLogic.diamond R (claim Q D) w) (hs : ∀ S ∈ subdomainAlternatives Subdomains.singletons D, AntiExhaustivity R w D Q S) : ModalVariation R w D Q

Under uniqueness, negating the pre-exhaustified singleton alternatives yields Modal Variation.

theorem Exhaustification.modalVariation_of_box {W : Type u_1} {E : Type u_2} (R : W → W → Prop) (w : W) (D : Finset E) (Q : W → E → Prop) [DecidableEq E] [(v : W) → DecidablePred (Q v)] (hw : ∃ (v : W), R w v) (h : ModalLogic.box R (claim Q D) w) (hc : ∀ S ∈ subdomainAlternatives Subdomains.singletons D, ¬ModalLogic.box R (claim Q S) w) : ModalVariation R w D Q

Under a necessity modal, a true claim whose singleton alternatives are all false shows Modal Variation.

theorem Exhaustification.freeChoice_of_proper {W : Type u_1} {E : Type u_2} (R : W → W → Prop) (w : W) (D : Finset E) (Q : W → E → Prop) [DecidableEq E] (h : ModalLogic.diamond R (claim Q D) w) (hs : ∀ S ∈ subdomainAlternatives Subdomains.proper D, AntiExhaustivity R w D Q S) : FreeChoice R w D Q

Negating every pre-exhaustified proper alternative yields Free Choice.

Decidability

@[instance_reducible]

instance Exhaustification.instDecidableClaim {W : Type u_1} {E : Type u_2} (Q : W → E → Prop) [(v : W) → DecidablePred (Q v)] (S : Finset E) (v : W) : Decidable (claim Q S v)

Equations

• Exhaustification.instDecidableClaim Q S v = Exhaustification.instDecidableClaim._aux_1 Q S v

@[instance_reducible]

instance Exhaustification.instDecidableFreeChoice {W : Type u_1} {E : Type u_2} (R : W → W → Prop) (w : W) (D : Finset E) (Q : W → E → Prop) [Fintype W] [DecidableRel R] [(v : W) → DecidablePred (Q v)] : Decidable (FreeChoice R w D Q)

Equations

• Exhaustification.instDecidableFreeChoice R w D Q = Exhaustification.instDecidableFreeChoice._aux_1 R w D Q

@[instance_reducible]

instance Exhaustification.instDecidableModalVariationOfDecidableEq {W : Type u_1} {E : Type u_2} (R : W → W → Prop) (w : W) (D : Finset E) (Q : W → E → Prop) [DecidableEq E] [Fintype W] [DecidableRel R] [(v : W) → DecidablePred (Q v)] [DecidableEq W] : Decidable (ModalVariation R w D Q)

Equations

• Exhaustification.instDecidableModalVariationOfDecidableEq R w D Q = Exhaustification.instDecidableModalVariationOfDecidableEq._aux_1 R w D Q

@[instance_reducible]

instance Exhaustification.instDecidableUniqueness {W : Type u_1} {E : Type u_2} (R : W → W → Prop) (w : W) (D : Finset E) (Q : W → E → Prop) [Fintype W] [DecidableRel R] [(v : W) → DecidablePred (Q v)] : Decidable (Uniqueness R w D Q)

Equations

• Exhaustification.instDecidableUniqueness R w D Q = Exhaustification.instDecidableUniqueness._aux_1 R w D Q

@[instance_reducible]

instance Exhaustification.instDecidableAntiExhaustivity {W : Type u_1} {E : Type u_2} (R : W → W → Prop) (w : W) (D : Finset E) (Q : W → E → Prop) [DecidableEq E] [Fintype W] [DecidableRel R] [(v : W) → DecidablePred (Q v)] (S : Finset E) : Decidable (AntiExhaustivity R w D Q S)

Equations

• Exhaustification.instDecidableAntiExhaustivity R w D Q S = Exhaustification.instDecidableAntiExhaustivity._aux_1 R w D Q S