Fox and Spector (2018): Economy and Embedded Exhaustification

This file formalizes [FS18]'s economy condition on the exhaustivity operator: an occurrence of exh is licensed only if it is not incrementally weakening, that is, unless for every continuation of the sentence at that point eliminating it leaves the meaning unchanged or stronger (Licensed). The condition derives Singh's asymmetry between the two orders of a Hurford disjunction (singh_canonical, singh_reverse), its disappearance for distant entailing disjuncts (licensed_orRight_iff), and the ban on Hurford disjunctions under one downward-entailing operator but not two (not_licensed_of_forall_antitone, licensed_iff_of_forall_monotone). The comparison-class refinement of the condition, GloballyWeakeningCC, is what forces narrow focus under a downward-entailing operator: with more innocently excludable alternatives the two-layered exhaustification is weaker (op_exh_mono), and the exclusive construal of a disjunction under negation becomes conjunctive (exh_neg_exh, exh_neg_exh_or) though not under a negative quantifier (exh_no_exh).

Implementation notes

Sentences are propositions Set W; a continuation is a map on the meaning of the constituent, and the continuations available at a point are a set of such maps, so "incrementally" is quantification over that set. Downward-entailing operators are antitone maps and the paper's exhaustivity operator is Fox's innocent exclusion Exhaustification.exhIE. Focus and the Minimize Focus principle of §8 are not represented; the rows record the distribution of Hurford disjunctions by the paper's own classification of each sentence.

References

• [FS18]
• [CFS12]
• [Hur74]
• [Sin08]
• [GS12]
• [Sch08d]
• [Chi04b]

@[reducible, inline]

abbrev FoxSpector2018.Continuation (W : Type u_2) : Type u_2

A continuation is what the rest of the sentence does with the constituent's meaning.

Equations

• FoxSpector2018.Continuation W = (Set W → Set W)

The economy condition

def FoxSpector2018.GloballyVacuous {W : Type u_1} (S : Continuation W) (C : Set (Set W)) (A : Set W) : Prop

An occurrence of exh is globally vacuous when eliminating it does not change the truth conditions.

Equations

• FoxSpector2018.GloballyVacuous S C A = (S (Exhaustification.exhIE C A) = S A)

def FoxSpector2018.GloballyWeakening {W : Type u_1} (S : Continuation W) (C : Set (Set W)) (A : Set W) : Prop

An occurrence of exh is globally weakening when eliminating it does not alter or strengthens the truth conditions.

Equations

• FoxSpector2018.GloballyWeakening S C A = (S A ⊆ S (Exhaustification.exhIE C A))

def FoxSpector2018.IncrementallyVacuous {W : Type u_1} (conts : Set (Continuation W)) (C : Set (Set W)) (A : Set W) : Prop

An occurrence of exh is incrementally vacuous when it is vacuous for every continuation available at the point.

Equations

• FoxSpector2018.IncrementallyVacuous conts C A = ∀ S ∈ conts, FoxSpector2018.GloballyVacuous S C A

def FoxSpector2018.IncrementallyWeakening {W : Type u_1} (conts : Set (Continuation W)) (C : Set (Set W)) (A : Set W) : Prop

An occurrence of exh is incrementally weakening when it is weakening for every continuation available at the point.

Equations

• FoxSpector2018.IncrementallyWeakening conts C A = ∀ S ∈ conts, FoxSpector2018.GloballyWeakening S C A

def FoxSpector2018.Licensed {W : Type u_1} (conts : Set (Continuation W)) (C : Set (Set W)) (A : Set W) : Prop

By the economy condition, an occurrence of exh is licensed unless it is incrementally weakening.

Equations

• FoxSpector2018.Licensed conts C A = ¬FoxSpector2018.IncrementallyWeakening conts C A

theorem FoxSpector2018.GloballyVacuous.globallyWeakening {W : Type u_1} {S : Continuation W} {C : Set (Set W)} {A : Set W} (h : GloballyVacuous S C A) : GloballyWeakening S C A

theorem FoxSpector2018.not_licensed_of_incrementallyVacuous {W : Type u_1} {conts : Set (Continuation W)} {C : Set (Set W)} {A : Set W} (h : IncrementallyVacuous conts C A) : ¬Licensed conts C A

The first version of the condition, on vacuity, follows from the second.

theorem FoxSpector2018.not_licensed_of_eq {W : Type u_1} {conts : Set (Continuation W)} {C : Set (Set W)} {A : Set W} (h : Exhaustification.exhIE C A = A) : ¬Licensed conts C A

Vacuous exhaustification is never licensed.

theorem FoxSpector2018.globallyWeakening_of_antitone {W : Type u_1} {S : Continuation W} {C : Set (Set W)} {A : Set W} (hS : Antitone S) : GloballyWeakening S C A

Under a downward-entailing continuation, exh is always weakening.

theorem FoxSpector2018.globallyWeakening_iff_of_monotone {W : Type u_1} {S : Continuation W} {C : Set (Set W)} {A : Set W} (hS : Monotone S) : GloballyWeakening S C A ↔ GloballyVacuous S C A

Under an upward-entailing continuation, exh is weakening only when it is vacuous.

theorem FoxSpector2018.not_licensed_of_forall_antitone {W : Type u_1} {conts : Set (Continuation W)} {C : Set (Set W)} {A : Set W} (h : ∀ S ∈ conts, Antitone S) : ¬Licensed conts C A

Under a downward-entailing operator, exh is never licensed.

theorem FoxSpector2018.licensed_iff_of_forall_monotone {W : Type u_1} {conts : Set (Continuation W)} {C : Set (Set W)} {A : Set W} (h : ∀ S ∈ conts, Monotone S) : Licensed conts C A ↔ ∃ S ∈ conts, S (Exhaustification.exhIE C A) ≠ S A

Under upward-entailing continuations, as below two downward-entailing operators, exh is licensed exactly when it is not vacuous for one of them.

Hurford disjunctions

def FoxSpector2018.HurfordViolation {W : Type u_1} (p q : Set W) : Prop

Hurford's Constraint is violated when one disjunct entails the other.

Equations

• FoxSpector2018.HurfordViolation p q = (p ⊆ q ∨ q ⊆ p)

def FoxSpector2018.orLeft {W : Type u_1} : Set (Continuation W)

Any second disjunct may follow a first disjunct.

Equations

• FoxSpector2018.orLeft = Set.range fun (Y A : Set W) => A ∪ Y

def FoxSpector2018.orRight {W : Type u_1} (X : Set W) : Set (Continuation W)

Nothing follows a final disjunct after X.

Equations

• FoxSpector2018.orRight X = {fun (A : Set W) => X ∪ A}

theorem FoxSpector2018.licensed_orLeft {W : Type u_1} {C : Set (Set W)} {A : Set W} (h : Exhaustification.exhIE C A ≠ A) : Licensed orLeft C A

On a first disjunct, exh is licensed whenever it excludes something, since the empty second disjunct is a continuation on which it is not vacuous.

theorem FoxSpector2018.licensed_orRight_iff {W : Type u_1} {C : Set (Set W)} {A X : Set W} : Licensed (orRight X) C A ↔ ¬X ∪ A ⊆ X ∪ Exhaustification.exhIE C A

On a final disjunct, exh is licensed exactly when it strengthens the whole disjunction.

theorem FoxSpector2018.singh_canonical {W : Type u_1} {p q : Set W} (h : (p ∩ q).Nonempty) (h' : ((p ∪ q) \ (p ∩ q)).Nonempty) : Licensed orLeft {p ∪ q, p ∩ q} (p ∪ q)

In the canonical order of Singh's asymmetry, exhaustifying the weak disjunct of p or q, or both is licensed.

theorem FoxSpector2018.singh_reverse {W : Type u_1} {p q : Set W} (h' : ((p ∪ q) \ (p ∩ q)).Nonempty) : ¬Licensed (orRight (p ∩ q)) {p ∪ q, p ∩ q} (p ∪ q)

In the reverse order of Singh's asymmetry, exhaustifying the final weak disjunct of both, or p or q is vacuous, hence not licensed.

theorem FoxSpector2018.licensed_orRight_of_ssubset {W : Type u_1} {C : Set (Set W)} {p q : Set W} (h : q ∪ Exhaustification.exhIE C p ⊂ q ∪ p) : Licensed (orRight q) C p

For distant entailing disjuncts in reverse order, exh on the final weak disjunct is licensed when the exhaustified disjunction is strictly stronger than the bare one.

theorem FoxSpector2018.not_hurfordViolation_of_independent {W : Type u_1} {C : Set (Set W)} {p q : Set W} (h₁ : ¬Exhaustification.exhIE C p ⊆ q) (h₂ : ¬q ⊆ Exhaustification.exhIE C p) : ¬HurfordViolation (Exhaustification.exhIE C p) q

Exhaustifying the first disjunct restores Hurford's Constraint once the exhaustified disjunct and the second are logically independent.

theorem FoxSpector2018.not_licensed_neg {W : Type u_1} {C : Set (Set W)} {A : Set W} : ¬Licensed ((Set.range fun (r A : Set W) => (A ∪ r)ᶜ) ∪ Set.range fun (r A : Set W) => (A ∩ r)ᶜ) C A

Under negation, every continuation of a Hurford disjunction negates a disjunction or a conjunction containing the exhaustified disjunct, so exh is incrementally weakening.

The comparison class

def FoxSpector2018.excludable {W : Type u_1} (C : Set (Set W)) (A : Set W) : Set (Set W)

The innocently excludable alternatives.

Equations

• FoxSpector2018.excludable C A = {q : Set W | Exhaustification.IsInnocentlyExcludable C A q}

theorem FoxSpector2018.mem_excludable {W : Type u_1} {C : Set (Set W)} {A q : Set W} : q ∈ excludable C A ↔ Exhaustification.IsInnocentlyExcludable C A q

def FoxSpector2018.GloballyWeakeningCC {W : Type u_1} (S : Continuation W) (C : Set (Set W)) (A : Set W) : Prop

An occurrence of exh is globally weakening relative to the comparison class when some set of alternatives with strictly fewer innocently excludable members gives a result at least as strong.

Equations

• One or more equations did not get rendered due to their size.

theorem FoxSpector2018.GloballyWeakening.globallyWeakeningCC {W : Type u_1} {S : Continuation W} {C : Set (Set W)} {A : Set W} (h : GloballyWeakening S C A) (hne : (excludable C A).Nonempty) : GloballyWeakeningCC S C A

The comparison-class condition subsumes the earlier one, since the empty set of alternatives is a comparison.

theorem FoxSpector2018.exhIE_op {W : Type u_1} {S : Continuation W} {C : Set (Set W)} {A : Set W} (hne : (S (Exhaustification.exhIE C A) \ S A).Nonempty) : Exhaustification.exhIE {S (Exhaustification.exhIE C A), S A} (S (Exhaustification.exhIE C A)) = S (Exhaustification.exhIE C A) \ S A

Under a downward-entailing operator, exhaustifying against the un-exhaustified sentence denies it.

theorem FoxSpector2018.op_exh_mono {W : Type u_1} {S : Continuation W} {C C' : Set (Set W)} {A : Set W} (hOP : Antitone S) (hsub : excludable C' A ⊆ excludable C A) (hne : (S (Exhaustification.exhIE C A) \ S A).Nonempty) (hne' : (S (Exhaustification.exhIE C' A) \ S A).Nonempty) : Exhaustification.exhIE {S (Exhaustification.exhIE C' A), S A} (S (Exhaustification.exhIE C' A)) ⊆ Exhaustification.exhIE {S (Exhaustification.exhIE C A), S A} (S (Exhaustification.exhIE C A))

With more innocently excludable alternatives, the two-layered exhaustification under a downward-entailing operator is weaker, so economy forces the smaller alternative set, narrow focus. This is the theorem of §10.

Exhaustification under negation

theorem FoxSpector2018.exh_neg_exh {W : Type u_1} {C : Set (Set W)} {A : Set W} (hne : (A \ Exhaustification.exhIE C A).Nonempty) : Exhaustification.exhIE {(Exhaustification.exhIE C A)ᶜ, Aᶜ} (Exhaustification.exhIE C A)ᶜ = A \ Exhaustification.exhIE C A

Under negation, the exhaustified sentence exhaustified against the bare one yields what the inner exhaustification excluded, so the embedded implicature turns into its conjunctive dual.

theorem FoxSpector2018.exh_neg_exh_or {W : Type u_1} {p q : Set W} (h : (p ∩ q).Nonempty) (h' : ((p ∪ q) \ (p ∩ q)).Nonempty) : Exhaustification.exhIE {(Exhaustification.exhIE {p ∪ q, p ∩ q} (p ∪ q))ᶜ, (p ∪ q)ᶜ} (Exhaustification.exhIE {p ∪ q, p ∩ q} (p ∪ q))ᶜ = p ∩ q

An exclusive construal of a disjunction under negation is conjunctive.

theorem FoxSpector2018.exh_no_exh {W : Type u_1} {ι : Type u_2} {P Q : ι → Set W} (hQ : ∀ (x : ι), Q x ⊆ P x) (hne : ((⋃ (x : ι), P x \ Q x)ᶜ ∩ ⋃ (x : ι), Q x).Nonempty) : Exhaustification.exhIE {(⋃ (x : ι), P x \ Q x)ᶜ, (⋃ (x : ι), P x)ᶜ} (⋃ (x : ι), P x \ Q x)ᶜ = (⋃ (x : ι), P x \ Q x)ᶜ ∩ ⋃ (x : ι), Q x

Under a negative quantifier the construal is not conjunctive, since no individual has the weak property without the strong one, and some individual has the strong one.

The data

structure FoxSpector2018.Row : Type

A disjunction of the data records whether its disjuncts stand in entailment, whether a scalar alternative lets exhaustification break it, the order of the disjuncts, whether they are distant entailing disjuncts, and how many downward-entailing operators scope over it.

• hurford : Bool
• rescuable : Bool
• canonical : Bool
• distant : Bool
• de : ℕ
• judgment : Judgment

@[instance_reducible]

instance FoxSpector2018.instDecidableEqRow : DecidableEq Row

Equations

• FoxSpector2018.instDecidableEqRow = FoxSpector2018.instDecidableEqRow.decEq

def FoxSpector2018.instDecidableEqRow.decEq (x✝ x✝¹ : Row) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

def FoxSpector2018.yesNoTable : List (String × Bool)

Equations

• FoxSpector2018.yesNoTable = [("yes", true), ("no", false)]

def FoxSpector2018.Row.ofDatum (ex : Datum) : Option Row

Equations

• One or more equations did not get rendered due to their size.

def FoxSpector2018.rows : List Row

Equations

• FoxSpector2018.rows = List.filterMap FoxSpector2018.Row.ofDatum FoxSpector2018.Examples.all

theorem FoxSpector2018.rows_predicted (r : Row) : r ∈ rows → (r.judgment = Judgment.acceptable ↔ r.hurford = false ∨ r.rescuable = true ∧ (r.canonical = true ∨ r.distant = true) ∧ r.de ≠ 1)

Economy accounts for the distribution, a Hurford disjunction being acceptable when a scalar alternative lets exh break the entailment on a disjunct where it is licensed, the first one or a distant one, and no single downward-entailing operator makes it weakening.