Fox (2007): Free Choice and the Theory of Scalar Implicatures

From You may eat the cake or the ice-cream hearers infer that each option is allowed, though the sentence only says that one of them is. Fox derives this free choice inference by exhaustifying the sentence twice. The exhaustivity operator exhIE asserts its prejacent and denies the innocently excludable alternatives, those in every maximal set of alternatives that can be denied together consistently with the prejacent. exhIter C n applies it n times, each layer exhaustifying the previous layer's prejacent against the previous layer's alternatives.

The alternatives of a disjunction under an operator O are the disjunction, each disjunct and the conjunction, all under O. When O distributes over the disjunction but not over the conjunction, as possibility modals and existential quantifiers do, the second layer asserts each disjunct under O. A negated universal over a conjunction is the same case at the complements. When O does not distribute over the disjunction, as with necessity modals and universal quantifiers, the first layer denies both disjuncts instead, and plain disjunction stays exclusive at every layer.

Main statements

• exists_exhIter_eq: over finitely many alternatives, iterated exhaustification eventually stops changing.
• exhIter_two_eq_anEx: the second layer denies the exhaustification of every other alternative, whenever that is consistent.
• IsDiamond.exhIter_two_eq_iff: for a disjunction of two independent alternatives and a fourth alternative stronger than both, the second layer adds something exactly when the fourth is stronger than their conjunction.
• IsDiamond.disjoint_exhMW: exhaustifying by minimal worlds instead contradicts free choice.
• free_choice_permission, free_choice_not_required, existential_free_choice, conjunctive_free_choice: free choice under possibility modals, negated necessity modals, existential quantifiers and negated universal quantifiers.
• required_implicatures, universal_implicatures: under necessity modals and universal quantifiers, exhaustification denies both disjuncts.
• exclusive_or_of_one_le: plain disjunction is exclusive at every layer.
• singular_no_free_choice: a singular indefinite, whose alternatives include a plural one, has no free choice reading at any layer.
• embedded_scalar_implicature: for the reading or some of the homework, exhaustification denies all of the homework but not the reading.
• exhIE_infClosure_range, sauerland_exclusion_eq_empty: against the answers to a question, innocent exclusion yields exactly one, while denying every answer that passes Sauerland's test is contradictory.

Implementation notes

Propositions are sets of worlds, so the theorems hold over any model. Example numbers follow the published chapter. exhIter C 0 is the prejacent itself, so the paper's first layer is exhIter C 1. The sentence before (85) names the plural conjunctive alternative as excludable, but (85) needs the plural disjunctive one, which exhIE_singular shows is excludable too. The examples the paper leaves to scope or to an economy condition on exhaustification ((21), (34), (91b), (93c)) and the case it leaves open (92) are rows of Data.Examples.Fox2007 without a theorem.

TODO

• The paper equates the innocently excludable alternatives with those for which Sauerland's pragmatic system derives secondary implicatures. Stating this needs a belief operator.

References

• [Fox07]
• [Sau04]
• [KS17]
• [Chi04b]
• [GS84]
• [Sim05]
• [Zim00]

Recursive exhaustification

def Fox2007.exhIter {W : Type u_1} (C : Set (Set W)) : ℕ → Set W → Set W

Layer n + 1 of exhaustification exhaustifies layer n of the prejacent against layer n of every alternative; layer 0 is the prejacent itself.

Equations

• Fox2007.exhIter C 0 = id
• Fox2007.exhIter C n.succ = fun (p : Set W) => Exhaustification.exhIE (Fox2007.exhIter C n '' C) (Fox2007.exhIter C n p)

@[simp]

theorem Fox2007.exhIter_zero {W : Type u_1} (C : Set (Set W)) : exhIter C 0 = id

theorem Fox2007.exhIter_succ {W : Type u_1} (C : Set (Set W)) (n : ℕ) (p : Set W) : exhIter C (n + 1) p = Exhaustification.exhIE (exhIter C n '' C) (exhIter C n p)

@[simp]

theorem Fox2007.exhIter_one {W : Type u_1} (C : Set (Set W)) : exhIter C 1 = Exhaustification.exhIE C

theorem Fox2007.exhIter_two {W : Type u_1} (C : Set (Set W)) (p : Set W) : exhIter C 2 p = Exhaustification.exhIE (Exhaustification.exhIE C '' C) (Exhaustification.exhIE C p)

theorem Fox2007.exhIter_succ_subset {W : Type u_1} (C : Set (Set W)) (n : ℕ) (p : Set W) : exhIter C (n + 1) p ⊆ exhIter C n p

theorem Fox2007.antitone_exhIter {W : Type u_1} (C : Set (Set W)) (p : Set W) : Antitone fun (x : ℕ) => exhIter C x p

theorem Fox2007.exhIter_eq_of_succ_eq {W : Type u_1} {C : Set (Set W)} {n : ℕ} (h : ∀ q ∈ C, exhIter C (n + 1) q = exhIter C n q) {m : ℕ} (hm : n ≤ m) {q : Set W} (hq : q ∈ C) : exhIter C m q = exhIter C n q

Once a layer leaves every alternative unchanged, so do all later layers.

theorem Fox2007.exists_exhIter_eq {W : Type u_1} {C : Set (Set W)} (hC : C.Finite) : ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → ∀ q ∈ C, exhIter C m q = exhIter C n q

Over finitely many alternatives, iterated exhaustification of every alternative eventually stops changing, as Spector observed. Every layer is a union of classes of worlds verifying the same alternatives, and there are finitely many such unions.

def Fox2007.anEx {W : Type u_1} (C : Set (Set W)) (p : Set W) : Set W

The anti-exhaustivity reading asserts the exhaustified prejacent and denies the exhaustification of every other alternative that is not innocently excludable.

Equations

• Fox2007.anEx C p = Exhaustification.exhIE C p ∩ ⋂ q ∈ (C \ {q : Set W | Exhaustification.IsInnocentlyExcludable C p q}) \ {p}, (Exhaustification.exhIE C q)ᶜ

theorem Fox2007.anEx_eq {W : Type u_1} (C : Set (Set W)) (p : Set W) : anEx C p = Exhaustification.exhIE C p ∩ ⋂ q ∈ C \ {p}, (Exhaustification.exhIE C q)ᶜ

The anti-exhaustivity reading denies the exhaustification of every other alternative.

theorem Fox2007.anEx_insert {W : Type u_1} (p : Set W) {C₀ : Set (Set W)} (hp : p ∉ C₀) : anEx (insert p C₀) p = Exhaustification.exhIE (insert p C₀) p ∩ ⋂ q ∈ C₀, (Exhaustification.exhIE (insert p C₀) q)ᶜ

The anti-exhaustivity reading for alternatives listed apart from the prejacent.

theorem Fox2007.anEx_eq_exh {W : Type u_1} (C : Set (Set W)) (p : Set W) (h : (anEx C p).Nonempty) : anEx C p = Exhaustification.exh (Exhaustification.exhIE C '' C) (Exhaustification.exhIE C p)

A consistent anti-exhaustivity reading denies every exhaustified alternative that the exhaustified prejacent does not entail.

theorem Fox2007.exhIter_two_eq_anEx {W : Type u_1} (C : Set (Set W)) (p : Set W) (h : (anEx C p).Nonempty) : exhIter C 2 p = anEx C p

A consistent anti-exhaustivity reading is the second layer of exhaustification, as the paper's Appendix proves.

The diamond

structure Fox2007.IsDiamond {W : Type u_1} (w s n e : Set W) : Prop

Four alternatives form a diamond when the weakest w is the disjunction of the logically independent s and n, and the strongest e entails both.

• union : w = s ∪ n
• subset_left : e ⊆ s
• subset_right : e ⊆ n
• nonempty_sdiff_left : (s \ n).Nonempty
• nonempty_sdiff_right : (n \ s).Nonempty

theorem Fox2007.IsDiamond.symm {W : Type u_1} {w s n e : Set W} (h : IsDiamond w s n e) : IsDiamond w n s e

theorem Fox2007.IsDiamond.notMem {W : Type u_1} {w s n e : Set W} (h : IsDiamond w s n e) : w ∉ {s, n, e}

theorem Fox2007.IsDiamond.exhMW_eq {W : Type u_1} {w s n e : Set W} (h : IsDiamond w s n e) : Exhaustification.exhMW {w, s, n, e} w = symmDiff s n

The minimal worlds of the weakest alternative are those of exactly one middle alternative.

theorem Fox2007.IsDiamond.disjoint_exhMW {W : Type u_1} {w s n e : Set W} (h : IsDiamond w s n e) : Disjoint (Exhaustification.exhMW {w, s, n, e} w) (s ∩ n)

Exhaustification by minimal worlds contradicts the conjunction of the middle alternatives, so on a diamond it can never yield free choice.

theorem Fox2007.IsDiamond.isInnocentlyExcludable_iff {W : Type u_1} {w s n e : Set W} (h : IsDiamond w s n e) {q : Set W} (hq : q ∈ {w, s, n, e}) : Exhaustification.IsInnocentlyExcludable {w, s, n, e} w q ↔ q = e

Given the weakest alternative only the strongest is innocently excludable, since it alone fails at every minimal world.

theorem Fox2007.IsDiamond.exhIE_w {W : Type u_1} {w s n e : Set W} (h : IsDiamond w s n e) : Exhaustification.exhIE {w, s, n, e} w = w \ e

theorem Fox2007.IsDiamond.exhIE_s {W : Type u_1} {w s n e : Set W} (h : IsDiamond w s n e) : Exhaustification.exhIE {w, s, n, e} s = s \ n

Given a middle alternative, every alternative it does not entail is denied.

theorem Fox2007.IsDiamond.exhIE_n {W : Type u_1} {w s n e : Set W} (h : IsDiamond w s n e) : Exhaustification.exhIE {w, s, n, e} n = n \ s

theorem Fox2007.IsDiamond.exhIE_e {W : Type u_1} {w s n e : Set W} (h : IsDiamond w s n e) : Exhaustification.exhIE {w, s, n, e} e = e

The strongest alternative entails all the others, so exhaustifying it is vacuous.

theorem Fox2007.IsDiamond.image_exhIE {W : Type u_1} {w s n e : Set W} (h : IsDiamond w s n e) : Exhaustification.exhIE {w, s, n, e} '' {w, s, n, e} = {w \ e, s \ n, n \ s, e}

The alternatives of the second layer.

theorem Fox2007.IsDiamond.anEx_w {W : Type u_1} {w s n e : Set W} (h : IsDiamond w s n e) : anEx {w, s, n, e} w = (s ∩ n) \ e

The anti-exhaustivity reading of the weakest alternative asserts both middle alternatives and denies the strongest.

theorem Fox2007.IsDiamond.exhIter_two_eq {W : Type u_1} {w s n e : Set W} (h : IsDiamond w s n e) (hne : ((s ∩ n) \ e).Nonempty) : exhIter {w, s, n, e} 2 w = (s ∩ n) \ e

When the strongest alternative is stronger than the conjunction of the middle ones, the second layer asserts both and denies the strongest.

theorem Fox2007.IsDiamond.exhIter_two_eq_of_eq_inter {W : Type u_1} {w s n e : Set W} (h : IsDiamond w s n e) (he : e = s ∩ n) : exhIter {w, s, n, e} 2 w = symmDiff s n

When the strongest alternative is the conjunction of the middle ones, the second layer is the exclusive disjunction of the middle ones, as the first layer was.

theorem Fox2007.IsDiamond.exhIter_two_eq_iff {W : Type u_1} {w s n e : Set W} (h : IsDiamond w s n e) : exhIter {w, s, n, e} 2 w = Exhaustification.exhIE {w, s, n, e} w ↔ e = s ∩ n

The second layer adds nothing exactly when the strongest alternative is the conjunction of the middle ones.

Alternatives under an operator

def Fox2007.sauerlandAlt {W : Type u_1} {α : Type u_2} [Lattice α] (O : α → Set W) (a b : α) : Set (Set W)

The Sauerland alternatives of a disjunction under an operator O are the disjunction, each disjunct and the conjunction, each under O.

Equations

• Fox2007.sauerlandAlt O a b = {O (a ⊔ b), O a, O b, O (a ⊓ b)}

theorem Fox2007.isDiamond_sauerlandAlt {W : Type u_1} {α : Type u_2} [Lattice α] {O : α → Set W} {a b : α} (hO : Monotone O) (hab : O (a ⊔ b) ⊆ O a ∪ O b) (ha : (O a \ O b).Nonempty) (hb : (O b \ O a).Nonempty) : IsDiamond (O (a ⊔ b)) (O a) (O b) (O (a ⊓ b))

Under a monotone operator that distributes over the disjunction, the Sauerland alternatives form a diamond whenever each disjunct can hold under O without the other.

theorem Fox2007.free_choice {W : Type u_1} {α : Type u_2} [Lattice α] {O : α → Set W} {a b : α} (hO : Monotone O) (hab : O (a ⊔ b) ⊆ O a ∪ O b) (ha : (O a \ O b).Nonempty) (hb : (O b \ O a).Nonempty) (hfc : ((O a ∩ O b) \ O (a ⊓ b)).Nonempty) : exhIter (sauerlandAlt O a b) 2 (O (a ⊔ b)) = (O a ∩ O b) \ O (a ⊓ b)

Under a monotone operator that distributes over the disjunction, the second layer asserts each disjunct under O and denies the conjunction under O, whenever O does not distribute over that conjunction. This is free choice.

theorem Fox2007.exhIE_sauerlandAlt_of_not_subset {W : Type u_1} {α : Type u_2} [Lattice α] {O : α → Set W} {a b : α} (hO : Monotone O) (h : (O (a ⊔ b) \ (O a ∪ O b)).Nonempty) : Exhaustification.exhIE (sauerlandAlt O a b) (O (a ⊔ b)) = O (a ⊔ b) \ (O a ∪ O b)

Under a monotone operator that does not distribute over the disjunction, the first layer denies both disjuncts under O.

def Fox2007.hornAlt {W : Type u_1} {α : Type u_2} [Lattice α] (O O' : α → Set W) (a b : α) : Set (Set W)

The alternatives of O (a ⊔ b) generated by the Horn sets {O, O'} and Sauerland's {or, L, R, and} are the Sauerland alternatives under O and under O'.

Equations

• Fox2007.hornAlt O O' a b = {O (a ⊔ b), O a, O b, O (a ⊓ b), O' (a ⊔ b), O' a, O' b, O' (a ⊓ b)}

theorem Fox2007.finite_hornAlt {W : Type u_1} {α : Type u_2} [Lattice α] {O : α → Set W} {a b : α} {O' : α → Set W} : (hornAlt O O' a b).Finite

theorem Fox2007.hornAlt_comm {W : Type u_1} {α : Type u_2} [Lattice α] {O : α → Set W} {a b : α} {O' : α → Set W} : hornAlt O O' b a = hornAlt O O' a b

theorem Fox2007.exhIE_hornAlt_left {W : Type u_1} {α : Type u_2} [Lattice α] {O : α → Set W} {a b : α} {O' : α → Set W} (hO : Monotone O) (hO' : Monotone O') (ha : (O a \ (O b ∪ O' (a ⊔ b))).Nonempty) : Exhaustification.exhIE (hornAlt O O' a b) (O a) = O a \ (O b ∪ O' (a ⊔ b))

Exhaustifying the first disjunct under O denies everything it does not entail.

theorem Fox2007.isMinimalCover_hornAlt {W : Type u_1} {α : Type u_2} [Lattice α] {O : α → Set W} {a b : α} {O' : α → Set W} (hO : Monotone O) (hO' : Monotone O') (hab : O (a ⊔ b) ⊆ O a ∪ O b) {x y : W} (hx : x ∈ O a \ (O b ∪ O' (a ⊔ b))) (hy : y ∈ O b \ (O a ∪ O' (a ⊔ b))) : Exhaustification.IsMinimalCover (hornAlt O O' a b) (O (a ⊔ b)) {x, y}

A world where only the first disjunct holds under O and the disjunction fails under O', and its mirror image, represent the minimal worlds of the disjunction under O.

theorem Fox2007.exhIE_hornAlt {W : Type u_1} {α : Type u_2} [Lattice α] {O : α → Set W} {a b : α} {O' : α → Set W} (hO : Monotone O) (hO' : Monotone O') (hab : O (a ⊔ b) ⊆ O a ∪ O b) (ha : (O a \ (O b ∪ O' (a ⊔ b))).Nonempty) (hb : (O b \ (O a ∪ O' (a ⊔ b))).Nonempty) : Exhaustification.exhIE (hornAlt O O' a b) (O (a ⊔ b)) = O (a ⊔ b) \ (O (a ⊓ b) ∪ O' (a ⊔ b))

Exhaustifying the disjunction under O against the alternatives of both Horn sets denies the conjunction under O and the disjunction under O'.

theorem Fox2007.free_choice_hornAlt {W : Type u_1} {α : Type u_2} [Lattice α] {O : α → Set W} {a b : α} {O' : α → Set W} (hO : Monotone O) (hO' : Monotone O') (hab : O (a ⊔ b) ⊆ O a ∪ O b) (ha : (O a \ (O b ∪ O' (a ⊔ b))).Nonempty) (hb : (O b \ (O a ∪ O' (a ⊔ b))).Nonempty) (hfc : ((O a ∩ O b) \ (O (a ⊓ b) ∪ O' (a ⊔ b))).Nonempty) : exhIter (hornAlt O O' a b) 2 (O (a ⊔ b)) = (O a ∩ O b) \ (O (a ⊓ b) ∪ O' (a ⊔ b))

Against the alternatives of both Horn sets, the second layer asserts each disjunct under O and denies the conjunction under O and the disjunction under O'.

Plain disjunction

theorem Fox2007.isDiamond_or {W : Type u_1} {p q : Set W} (hp : (p \ q).Nonempty) (hq : (q \ p).Nonempty) : IsDiamond (p ∪ q) p q (p ∩ q)

theorem Fox2007.exh_or {W : Type u_1} {p q : Set W} (hp : (p \ q).Nonempty) (hq : (q \ p).Nonempty) : Exhaustification.exh {p ∪ q, p, q, p ∩ q} (p ∪ q) = ∅

Without innocent exclusion, denying every alternative the disjunction does not entail contradicts it.

theorem Fox2007.exclusive_or {W : Type u_1} {p q : Set W} (hp : (p \ q).Nonempty) (hq : (q \ p).Nonempty) : Exhaustification.exhIE {p ∪ q, p, q, p ∩ q} (p ∪ q) = symmDiff p q

Innocent exclusion denies only the conjunction of a disjunction, giving exclusive or.

theorem Fox2007.exclusive_or_of_one_le {W : Type u_1} {p q : Set W} (hp : (p \ q).Nonempty) (hq : (q \ p).Nonempty) {n : ℕ} (hn : 1 ≤ n) : exhIter {p ∪ q, p, q, p ∩ q} n (p ∪ q) = symmDiff p q

Plain disjunction is exclusive at every layer of exhaustification, so no layer yields the conjunctive reading.

Modals

theorem Fox2007.free_choice_permission {W : Type u_1} {R : SetRel W W} {p q : Set W} (hp : (R.preimage p \ R.preimage q).Nonempty) (hq : (R.preimage q \ R.preimage p).Nonempty) (h : ((R.preimage p ∩ R.preimage q) \ R.preimage (p ∩ q)).Nonempty) : exhIter {R.preimage (p ∪ q), R.preimage p, R.preimage q, R.preimage (p ∩ q)} 2 (R.preimage (p ∪ q)) = (R.preimage p ∩ R.preimage q) \ R.preimage (p ∩ q)

Free choice permission. Given a world where each option is allowed without the other and one where each is allowed but not both, the doubly exhaustified ◇(p ∨ q) asserts both permissions and denies the joint one.

theorem Fox2007.free_choice_permission_with_necessity {W : Type u_1} {R : SetRel W W} {p q : Set W} (hp : (R.preimage p \ (R.preimage q ∪ R.core (p ∪ q))).Nonempty) (hq : (R.preimage q \ (R.preimage p ∪ R.core (p ∪ q))).Nonempty) (h : ((R.preimage p ∩ R.preimage q) \ (R.preimage (p ∩ q) ∪ R.core (p ∪ q))).Nonempty) : exhIter {R.preimage (p ∪ q), R.preimage p, R.preimage q, R.preimage (p ∩ q), R.core (p ∪ q), R.core p, R.core q, R.core (p ∩ q)} 2 (R.preimage (p ∪ q)) = (R.preimage p ∩ R.preimage q) \ (R.preimage (p ∩ q) ∪ R.core (p ∪ q))

Against the necessity alternatives too, the doubly exhaustified ◇(p ∨ q) asserts both permissions and denies the joint permission and the requirement of the disjunction.

theorem Fox2007.free_choice_not_required {W : Type u_1} {R : SetRel W W} {p q : Set W} (hp : ((R.core p)ᶜ \ ((R.core q)ᶜ ∪ (R.preimage (p ∩ q))ᶜ)).Nonempty) (hq : ((R.core q)ᶜ \ ((R.core p)ᶜ ∪ (R.preimage (p ∩ q))ᶜ)).Nonempty) (h : (((R.core p)ᶜ ∩ (R.core q)ᶜ) \ ((R.core (p ∪ q))ᶜ ∪ (R.preimage (p ∩ q))ᶜ)).Nonempty) : exhIter {(R.core (p ∩ q))ᶜ, (R.core p)ᶜ, (R.core q)ᶜ, (R.core (p ∪ q))ᶜ, (R.preimage (p ∩ q))ᶜ, (R.preimage p)ᶜ, (R.preimage q)ᶜ, (R.preimage (p ∪ q))ᶜ} 2 (R.core (p ∩ q))ᶜ = ((R.core p)ᶜ ∩ (R.core q)ᶜ) \ ((R.core (p ∪ q))ᶜ ∪ (R.preimage (p ∩ q))ᶜ)

Free choice under a negated necessity modal. Against the alternatives under ¬□ and ¬◇, the doubly exhaustified ¬□(p ∧ q) asserts that neither conjunct is required, that their disjunction is required and that their conjunction is allowed. It is free choice permission for the negated conjuncts.

theorem Fox2007.required_implicatures {W : Type u_1} {R : SetRel W W} {p q : Set W} (h : (R.core (p ∪ q) \ (R.core p ∪ R.core q)).Nonempty) : Exhaustification.exhIE {R.core (p ∪ q), R.core p, R.core q, R.core (p ∩ q)} (R.core (p ∪ q)) = R.core (p ∪ q) \ (R.core p ∪ R.core q)

When □(p ∨ q) is consistent with denying □p and □q, exhaustification denies both, since a necessity modal does not distribute over disjunction.

theorem Fox2007.free_choice_of_disjoint {W : Type u_1} {R : SetRel W W} {p q : Set W} (hpq : Disjoint p q) (hp : (R.preimage p \ R.preimage q).Nonempty) (hq : (R.preimage q \ R.preimage p).Nonempty) (h : (R.preimage p ∩ R.preimage q).Nonempty) : exhIter {R.preimage (p ∪ q), R.preimage p, R.preimage q, R.preimage (p ∩ q)} 2 (R.preimage (p ∪ q)) = R.preimage p ∩ R.preimage q

Simons's reading. When the disjuncts are incompatible, as they are once each is exhaustified against the other, the joint alternative is empty, so free choice arrives without the anti-conjunctive inference.

Quantifiers

theorem Fox2007.existential_free_choice {W : Type u_1} {ι : Type u_2} {P Q : ι → Set W} (hp : ((⋃ (x : ι), P x) \ ⋃ (x : ι), Q x).Nonempty) (hq : ((⋃ (x : ι), Q x) \ ⋃ (x : ι), P x).Nonempty) (h : (((⋃ (x : ι), P x) ∩ ⋃ (x : ι), Q x) \ ⋃ (x : ι), P x ∩ Q x).Nonempty) : exhIter {⋃ (x : ι), P x ∪ Q x, ⋃ (x : ι), P x, ⋃ (x : ι), Q x, ⋃ (x : ι), P x ∩ Q x} 2 (⋃ (x : ι), P x ∪ Q x) = ((⋃ (x : ι), P x) ∩ ⋃ (x : ι), Q x) \ ⋃ (x : ι), P x ∩ Q x

Existential free choice. Given a witness for each disjunct but none for both, the doubly exhaustified ∃x (P x ∨ Q x) asserts witnesses for each disjunct and denies a joint one.

theorem Fox2007.existential_free_choice_with_universal {W : Type u_1} {ι : Type u_2} {P Q : ι → Set W} (hp : ((⋃ (x : ι), P x) \ ((⋃ (x : ι), Q x) ∪ ⋂ (x : ι), P x ∪ Q x)).Nonempty) (hq : ((⋃ (x : ι), Q x) \ ((⋃ (x : ι), P x) ∪ ⋂ (x : ι), P x ∪ Q x)).Nonempty) (h : (((⋃ (x : ι), P x) ∩ ⋃ (x : ι), Q x) \ ((⋃ (x : ι), P x ∩ Q x) ∪ ⋂ (x : ι), P x ∪ Q x)).Nonempty) : exhIter {⋃ (x : ι), P x ∪ Q x, ⋃ (x : ι), P x, ⋃ (x : ι), Q x, ⋃ (x : ι), P x ∩ Q x, ⋂ (x : ι), P x ∪ Q x, ⋂ (x : ι), P x, ⋂ (x : ι), Q x, ⋂ (x : ι), P x ∩ Q x} 2 (⋃ (x : ι), P x ∪ Q x) = ((⋃ (x : ι), P x) ∩ ⋃ (x : ι), Q x) \ ((⋃ (x : ι), P x ∩ Q x) ∪ ⋂ (x : ι), P x ∪ Q x)

Against the universal alternatives too, the doubly exhaustified ∃x (P x ∨ Q x) asserts witnesses for each disjunct and denies a joint witness and that everything satisfies the disjunction.

theorem Fox2007.conjunctive_free_choice {W : Type u_1} {ι : Type u_2} {P Q : ι → Set W} (hp : ((⋂ (x : ι), P x)ᶜ \ ((⋂ (x : ι), Q x)ᶜ ∪ (⋃ (x : ι), P x ∩ Q x)ᶜ)).Nonempty) (hq : ((⋂ (x : ι), Q x)ᶜ \ ((⋂ (x : ι), P x)ᶜ ∪ (⋃ (x : ι), P x ∩ Q x)ᶜ)).Nonempty) (h : (((⋂ (x : ι), P x)ᶜ ∩ (⋂ (x : ι), Q x)ᶜ) \ ((⋂ (x : ι), P x ∪ Q x)ᶜ ∪ (⋃ (x : ι), P x ∩ Q x)ᶜ)).Nonempty) : exhIter {(⋂ (x : ι), P x ∩ Q x)ᶜ, (⋂ (x : ι), P x)ᶜ, (⋂ (x : ι), Q x)ᶜ, (⋂ (x : ι), P x ∪ Q x)ᶜ, (⋃ (x : ι), P x ∩ Q x)ᶜ, (⋃ (x : ι), P x)ᶜ, (⋃ (x : ι), Q x)ᶜ, (⋃ (x : ι), P x ∪ Q x)ᶜ} 2 (⋂ (x : ι), P x ∩ Q x)ᶜ = ((⋂ (x : ι), P x)ᶜ ∩ (⋂ (x : ι), Q x)ᶜ) \ ((⋂ (x : ι), P x ∪ Q x)ᶜ ∪ (⋃ (x : ι), P x ∩ Q x)ᶜ)

Conjunctive free choice. Against the alternatives under ¬∀ and ¬∃, the doubly exhaustified ¬∀x (P x ∧ Q x) asserts that something lacks each conjunct, that everything has one of them and that something has both.

theorem Fox2007.universal_implicatures {W : Type u_1} {ι : Type u_2} {P Q : ι → Set W} (h : ((⋂ (x : ι), P x ∪ Q x) \ ((⋂ (x : ι), P x) ∪ ⋂ (x : ι), Q x)).Nonempty) : Exhaustification.exhIE {⋂ (x : ι), P x ∪ Q x, ⋂ (x : ι), P x, ⋂ (x : ι), Q x, ⋂ (x : ι), P x ∩ Q x} (⋂ (x : ι), P x ∪ Q x) = (⋂ (x : ι), P x ∪ Q x) \ ((⋂ (x : ι), P x) ∪ ⋂ (x : ι), Q x)

When ∀x (P x ∨ Q x) is consistent with denying ∀x P x and ∀x Q x, exhaustification denies both, since a universal quantifier does not distribute over disjunction.

def Fox2007.atLeastTwo {W : Type u_1} {ι : Type u_2} (P : ι → Set W) : Set W

At least two individuals satisfy P, the plural alternative of a singular indefinite.

Equations

• Fox2007.atLeastTwo P = {u : W | {x : ι | u ∈ P x}.Nontrivial}

theorem Fox2007.atLeastTwo_mono {W : Type u_1} {ι : Type u_2} : Monotone atLeastTwo

theorem Fox2007.exhIE_singular {W : Type u_1} {ι : Type u_2} {P Q : ι → Set W} (hP : ∃ (u : W), (∃! x : ι, u ∈ P x) ∧ ∀ (x : ι), u ∉ Q x) (hQ : ∃ (u : W), (∃! x : ι, u ∈ Q x) ∧ ∀ (x : ι), u ∉ P x) : Exhaustification.exhIE {⋃ (x : ι), P x ∪ Q x, ⋃ (x : ι), P x, ⋃ (x : ι), Q x, ⋃ (x : ι), P x ∩ Q x, atLeastTwo (P ⊔ Q), atLeastTwo P, atLeastTwo Q, atLeastTwo (P ⊓ Q)} (⋃ (x : ι), P x ∪ Q x) = (⋃ (x : ι), P x ∪ Q x) \ ((⋃ (x : ι), P x ∩ Q x) ∪ atLeastTwo (P ⊔ Q))

Exhaustifying a singular indefinite over a disjunction, against the alternatives of the indefinite and of its plural counterpart, denies a joint witness and a second witness. The hypotheses supply, for each disjunct, a world where exactly one individual satisfies it and none satisfies the other.

theorem Fox2007.singular_no_free_choice {W : Type u_1} {ι : Type u_2} {P Q : ι → Set W} (hP : ∃ (u : W), (∃! x : ι, u ∈ P x) ∧ ∀ (x : ι), u ∉ Q x) (hQ : ∃ (u : W), (∃! x : ι, u ∈ Q x) ∧ ∀ (x : ι), u ∉ P x) {n : ℕ} (hn : 1 ≤ n) : Disjoint (exhIter {⋃ (x : ι), P x ∪ Q x, ⋃ (x : ι), P x, ⋃ (x : ι), Q x, ⋃ (x : ι), P x ∩ Q x, atLeastTwo (P ⊔ Q), atLeastTwo P, atLeastTwo Q, atLeastTwo (P ⊓ Q)} n (⋃ (x : ι), P x ∪ Q x)) ((⋃ (x : ι), P x) ∩ ⋃ (x : ι), Q x)

A singular indefinite over a disjunction has no free choice reading, since every layer of exhaustification contradicts a witness for each disjunct.

Disjunction with an embedded scalar item

theorem Fox2007.embedded_scalar_implicature {W : Type u_1} {r sh ah : Set W} (hah : ah ⊆ sh) (hsh : (sh \ (r ∪ ah)).Nonempty) (hr : (r \ sh).Nonempty) : Exhaustification.exhIE {r ∪ sh, r, sh, r ∩ sh, r ∪ ah, r, ah, r ∩ ah} (r ∪ sh) = (r ∪ sh) \ (ah ∪ r ∩ sh)

Against the eight alternatives of Chierchia's John did the reading or some of the homework, innocent exclusion denies all of the homework and the conjunction but not the reading.

Answers to a question

def Fox2007.IsSauerlandExcludable {W : Type u_1} (C : Set (Set W)) (p q : Set W) : Prop

Sauerland's test lets an alternative the prejacent does not entail be excluded when denying it, given the prejacent, forces no other such alternative.

Equations

• Fox2007.IsSauerlandExcludable C p q = (q ∈ C ∧ ¬p ⊆ q ∧ ∀ r ∈ C, ¬p ⊆ r → ¬p \ q ⊆ r)

theorem Fox2007.isInnocentlyExcludable_conj {W : Type u_1} {ι : Type u_2} {a : ι → Set W} (ha : Exhaustification.Irredundant a) {S : Finset ι} {i j : ι} (hi : i ∈ S) (hj : j ∈ S) (hij : i ≠ j) : Exhaustification.IsInnocentlyExcludable (infClosure (Set.range a)) (⋃ (i : ι), a i) (⋂ k ∈ S, a k)

A group of two or more is innocently excludable given the existential answer.

theorem Fox2007.not_isInnocentlyExcludable_atom {W : Type u_1} {ι : Type u_2} {a : ι → Set W} (ha : Exhaustification.Irredundant a) (i : ι) : ¬Exhaustification.IsInnocentlyExcludable (infClosure (Set.range a)) (⋃ (i : ι), a i) (a i)

A single individual is not innocently excludable given the existential answer.

theorem Fox2007.exhIE_infClosure_range {W : Type u_1} {ι : Type u_2} {a : ι → Set W} (ha : Exhaustification.Irredundant a) [Fintype ι] [DecidableEq ι] : Exhaustification.exhIE (infClosure (Set.range a)) (⋃ (i : ι), a i) = {u : W | ∃! i : ι, u ∈ a i}

Exhaustifying the existential answer against its Hamblin alternatives yields exactly one, provided each individual can be the sole witness.

theorem Fox2007.exh_infClosure_range_eq_empty {W : Type u_1} {ι : Type u_2} {a : ι → Set W} (ha : Exhaustification.Irredundant a) {i j : ι} (hij : i ≠ j) : Exhaustification.exh (infClosure (Set.range a)) (⋃ (i : ι), a i) = ∅

With two individuals, denying every answer that the existential answer does not entail contradicts it.

theorem Fox2007.isSauerlandExcludable_infClosure_range {W : Type u_1} {ι : Type u_2} {a : ι → Set W} (ha : Exhaustification.Irredundant a) {i j k : ι} (hij : i ≠ j) (hik : i ≠ k) (hjk : j ≠ k) {q : Set W} (hq : q ∈ infClosure (Set.range a)) : IsSauerlandExcludable (infClosure (Set.range a)) (⋃ (i : ι), a i) q

With three individuals, every answer passes Sauerland's test.

theorem Fox2007.sauerland_exclusion_eq_empty {W : Type u_1} {ι : Type u_2} {a : ι → Set W} (ha : Exhaustification.Irredundant a) {i j k : ι} (hij : i ≠ j) (hik : i ≠ k) (hjk : j ≠ k) : Exhaustification.exh {q : Set W | IsSauerlandExcludable (infClosure (Set.range a)) (⋃ (i : ι), a i) q} (⋃ (i : ι), a i) = ∅

With three individuals, denying every answer that passes Sauerland's test contradicts the existential answer.

A finite model

def Fox2007.edges : List (ℕ × ℕ)

In this seven-world model every option is permitted from 0, only the first from 4, only the second from 5, and each but not both from 6.

Equations

• Fox2007.edges = [(0, 1), (0, 2), (0, 3), (4, 1), (5, 2), (6, 1), (6, 2)]

def Fox2007.R : SetRel (Fin 7) (Fin 7)

The accessibility relation of the model.

Equations

• Fox2007.R = {e : Fin 7 × Fin 7 | (↑e.1, ↑e.2) ∈ Fox2007.edges}

@[instance_reducible]

instance Fox2007.instDecidableMemProdFinOfNatNatSetRelRMk (w v : Fin 7) : Decidable ((w, v) ∈ R)

Equations

• Fox2007.instDecidableMemProdFinOfNatNatSetRelRMk w v = { decide := decide (List.elem (↑w, ↑v) Fox2007.edges = true), reflects_decide := ⋯ }

def Fox2007.p : Set (Fin 7)

The first option holds at worlds 1 and 3.

Equations

• Fox2007.p = {v : Fin 7 | ↑v ∈ [1, 3]}

def Fox2007.q : Set (Fin 7)

The second option holds at worlds 2 and 3.

Equations

• Fox2007.q = {v : Fin 7 | ↑v ∈ [2, 3]}

@[instance_reducible]

instance Fox2007.instDecidablePredFinOfNatNatMemSetP : DecidablePred fun (x : Fin 7) => x ∈ p

Equations

• Fox2007.instDecidablePredFinOfNatNatMemSetP v = { decide := decide (List.elem ↑v [1, 3] = true), reflects_decide := ⋯ }

@[instance_reducible]

instance Fox2007.instDecidablePredFinOfNatNatMemSetQ : DecidablePred fun (x : Fin 7) => x ∈ q

Equations

• Fox2007.instDecidablePredFinOfNatNatMemSetQ v = { decide := decide (List.elem ↑v [2, 3] = true), reflects_decide := ⋯ }