Fox & Spector 2018: Economy and Embedded Exhaustification

@cite{fox-spector-2018}

Fox, D. & Spector, B. (2018). Economy and embedded exhaustification. Natural Language Semantics, 26(1), 1–50.

Core Argument

Where can exh be inserted in the parse tree? Fox & Spector propose an economy condition: exh is licensed only if it is neither incrementally vacuous nor incrementally weakening. This single constraint derives three previously independent generalizations:

1. Hurford's Constraint: disjunctions where one disjunct entails the other are infelicitous (unless rescued by embedded exh)
2. Singh's Asymmetry: "p or q, or both" is acceptable but "both, or p or q" is not (@cite{singh-2008})
3. Implicature Focus Generalization (IFG): embedded exh under DE operators requires focus on the scalar item

Formalized Results

• Economy condition (original and comparison-class formulations)
• Hurford's Constraint derived from economy (hurford_from_economy)
• Singh's Asymmetry from economy (singh_weak_exh_nonvacuous, singh_strong_exh_vacuous)
• exh is always globally weakening under DE (exh_weakening_under_de)
• More IE alternatives → stronger result (exhIE_stronger_of_more_IE)
• Under DE, more IE → weaker global result (de_weakening_of_more_IE)
• The exh–exh prediction: exh[¬exh(p∨q)] = p∧q (exh_exh_conjunctive)
• Bridge to Symmetry.lean: vacuous exh violates economy (vacuous_violates_economy)

Connection to the Symmetry Problem

Economy interacts with the symmetry problem (Symmetry.lean) indirectly. When symmetric alternatives S₁, S₂ are the only non-weaker alternatives, exh is vacuous (proved by symmetric_exhB_vacuous). Vacuous exh violates economy (vacuous_violates_economy), so the grammar rejects the parse rather than producing wrong results. But economy does not derive the correct SI — that requires @cite{katzir-2007}'s structural complexity restricting the alternative set (see Structural.lean).

Economy and structural complexity are complementary:

• @cite{katzir-2007} determines which alternatives enter the set → breaks symmetry → exh derives the correct SI
• Economy determines whether exh is licensed given those alternatives → blocks vacuous/weakening insertions

@[reducible, inline]

abbrev Implicature.FoxSpector2018.Continuation (World : Type u_2) : Type u_2

A continuation context represents "the rest of the sentence" after a parse point.

Equations

• Implicature.FoxSpector2018.Continuation World = (Prop' World → Prop' World)

def Implicature.FoxSpector2018.negCont {World : Type u_1} : Continuation World

Negation continuation.

Equations

• Implicature.FoxSpector2018.negCont = Exhaustification.pneg

structure Implicature.FoxSpector2018.ParsePoint (World : Type u_2) : Type u_2

A parse point: a proposition with alternatives and possible continuations.

• prop : Prop' World
• alts : Set (Prop' World)
• continuations : Set (Continuation World)

def Implicature.FoxSpector2018.isIncrementallyVacuous {World : Type u_1} (ALT : Set (Prop' World)) (φ : Prop' World) (conts : Set (Continuation World)) : Prop

Incremental vacuity: exh makes no difference for ANY continuation.

Equations

• Implicature.FoxSpector2018.isIncrementallyVacuous ALT φ conts = ∀ C ∈ conts, ∀ (w : World), C (Exhaustification.exhIE ALT φ) w ↔ C φ w

def Implicature.FoxSpector2018.isIncrementallyWeakening {World : Type u_1} (ALT : Set (Prop' World)) (φ : Prop' World) (conts : Set (Continuation World)) : Prop

Incremental weakening: exh weakens the meaning for ALL continuations. In DE contexts, local strengthening = global weakening.

Equations

• Implicature.FoxSpector2018.isIncrementallyWeakening ALT φ conts = ∀ C ∈ conts, C φ ⊆ₚ C (Exhaustification.exhIE ALT φ)

def Implicature.FoxSpector2018.economyConditionMet {World : Type u_1} (ALT : Set (Prop' World)) (φ : Prop' World) (conts : Set (Continuation World)) : Prop

Economy Condition on Exhaustification (definition 63): exh(φ) is licensed only if it is neither incrementally vacuous nor incrementally weakening.

Equations

• Implicature.FoxSpector2018.economyConditionMet ALT φ conts = (¬Implicature.FoxSpector2018.isIncrementallyVacuous ALT φ conts ∧ ¬Implicature.FoxSpector2018.isIncrementallyWeakening ALT φ conts)

Comparison-Class Economy

The refined economy condition compares exh_C(φ) not just against φ, but against exh_{C'}(φ) for every subset C' of alternatives. Economy bans adding alternatives that only weaken the result.

def Implicature.FoxSpector2018.isGloballyWeakening {World : Type u_1} (ALT : Set (Prop' World)) (φ : Prop' World) (S : Continuation World) : Prop

Global weakening (definition 84): exh is globally weakening if the sentence without exh entails the sentence with exh.

Equations

• Implicature.FoxSpector2018.isGloballyWeakening ALT φ S = ∀ (w : World), S φ w → S (Exhaustification.exhIE ALT φ) w

def Implicature.FoxSpector2018.isGloballyWeakeningGen {World : Type u_1} (ALT : Set (Prop' World)) (φ : Prop' World) (S : Continuation World) : Prop

Generalized global weakening (definition 86): exh_C is globally weakening if there exists C' with strictly fewer IE alternatives such that S(exh_{C'}(A)) entails S(exh_C(A)). Using fewer alternatives gives a stronger result.

Equations

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

Hurford's Constraint

"A disjunction of the form 'A or B' sounds redundant and is odd when one of the disjuncts entails the other."

Fox & Spector derive this from economy rather than stipulating it.

def Implicature.FoxSpector2018.hurfordViolation {World : Type u_1} (A B : Prop' World) : Prop

Hurford violation: one disjunct entails the other.

Equations

• Implicature.FoxSpector2018.hurfordViolation A B = ((A ⊆ₚ B) ∨ B ⊆ₚ A)

def Implicature.FoxSpector2018.satisfiesHC {World : Type u_1} (A B : Prop' World) : Prop

A disjunction satisfies Hurford's Constraint if neither disjunct entails the other.

Equations

• Implicature.FoxSpector2018.satisfiesHC A B = ((¬A ⊆ₚ B) ∧ ¬B ⊆ₚ A)

def Implicature.FoxSpector2018.isRescuedByExh {World : Type u_1} (ALT : Set (Prop' World)) (A B : Prop' World) : Prop

A Hurford disjunction can be rescued by embedding exh in the weaker disjunct if the exhaustified disjunct no longer entails the stronger one.

Equations

• Implicature.FoxSpector2018.isRescuedByExh ALT A B = ¬Exhaustification.exhIE ALT A ⊆ₚ B

def Implicature.FoxSpector2018.disjCont {World : Type u_1} (A : Prop' World) : Continuation World

The disjunction continuation: (λp. A ∨ p).

Equations

• Implicature.FoxSpector2018.disjCont A p = Implicature.FoxSpector2018.por✝ A p

theorem Implicature.FoxSpector2018.hurford_from_economy {World : Type u_1} (ALT : Set (Prop' World)) (A B : Prop' World) (hBA : B ⊆ₚ A) (_hstill : Exhaustification.exhIE ALT B ⊆ₚ A) : isIncrementallyWeakening ALT B {disjCont A}

Hurford from Economy: if B ⊆ A and exh(B) cannot break the entailment, then exh(B) is incrementally weakening in the disjunction context — economy blocks the parse.

This derives Hurford's Constraint from economy rather than stipulating it as a surface filter.

Singh's Asymmetry (@cite{singh-2008})

"Mary read [A or B] or [A and B]" ✓ (weak first) "Mary read [A and B] or [A or B]" # (strong first)

Economy derives this: exh on the weak disjunct is non-vacuous (derives exclusive or), while exh on the strong disjunct is vacuous (nothing to exclude).

theorem Implicature.FoxSpector2018.singh_weak_exh_nonvacuous {World : Type u_1} (ALT : Set (Prop' World)) (weak strong : Prop' World) (h_excludes : ∃ (w : World), weak w ∧ ¬Exhaustification.exhIE ALT weak w ∧ ¬strong w) : ¬isIncrementallyVacuous ALT weak {disjCont strong}

Singh weak-first: exh on the weak disjunct is non-vacuous when exh genuinely excludes something. Economy is met.

The hypothesis h_excludes says there is a world where the weak disjunct holds but neither the exhaustified weak nor the strong holds — this witnesses non-vacuity.

theorem Implicature.FoxSpector2018.singh_strong_exh_vacuous {World : Type u_1} (weak strong : Prop' World) (h_entails : strong ⊆ₚ weak) : Exhaustification.exhIE {weak, strong} strong ≡ₚ strong

Singh strong-first: exh on the strong disjunct is vacuous when strong entails weak. The only alternative (weak) cannot be excluded because its negation contradicts the prejacent. Economy is violated.

The proof constructs {strong} as the unique MC-set: adding ¬weak or ¬strong to the exclusion set makes it inconsistent (since strong entails weak, every strong-world is a weak-world).

DE Operators and Economy

A key observation: exh is always globally weakening under DE operators. Since exhIE entails its prejacent (it can only strengthen), DE reverses this, making the overall sentence weaker.

This means economy blocks exh under DE unless:

1. The DE scope is embedded under another DE operator (making the overall context UE), or
2. Two levels of exh are used: exh[DE[exh(S)]], where the inner exh strengthens, DE reverses, and the outer exh strengthens again (§7, §10 of the paper)

The second mechanism requires focus on the scalar item to provide the right alternatives for the inner exh — this derives the IFG.

def Implicature.FoxSpector2018.isDECont {World : Type u_1} (S : Continuation World) : Prop

A continuation is downward-entailing if it reverses entailment.

Equations

• Implicature.FoxSpector2018.isDECont S = ∀ (p q : Prop' World), (∀ (w : World), p w → q w) → ∀ (w : World), S q w → S p w

theorem Implicature.FoxSpector2018.negCont_is_DE {World : Type u_1} : isDECont Exhaustification.pneg

Negation is DE.

theorem Implicature.FoxSpector2018.prejacent_mem_IE {World : Type u_1} (ALT : Set (Prop' World)) (φ : Prop' World) : φ ∈ Exhaustification.IE ALT φ

The prejacent is always in IE (it belongs to every compatible set by definition, hence every MC-set).

theorem Implicature.FoxSpector2018.exhIE_entails_prejacent {World : Type u_1} (ALT : Set (Prop' World)) (φ : Prop' World) : Exhaustification.exhIE ALT φ ⊆ₚ φ

exhIE always entails its prejacent: exhaustification can only strengthen, never weaken.

theorem Implicature.FoxSpector2018.exh_weakening_under_de {World : Type u_1} (ALT : Set (Prop' World)) (φ : Prop' World) (S_cont : Continuation World) (hDE : isDECont S_cont) : isGloballyWeakening ALT φ S_cont

exh is always globally weakening under DE: since exhIE ALT φ ⊆ₚ φ and DE reverses entailment, S(φ) ⊆ₚ S(exhIE ALT φ).

This is the core observation behind the IFG: embedded exh under DE operators is blocked by economy unless focus provides the right alternative set (via a two-level exh mechanism).

theorem Implicature.FoxSpector2018.exhIE_stronger_of_more_IE {World : Type u_1} (ALT ALT' : Set (Prop' World)) (φ : Prop' World) (hIE : Exhaustification.IE ALT' φ ⊆ Exhaustification.IE ALT φ) : Exhaustification.exhIE ALT φ ⊆ₚ Exhaustification.exhIE ALT' φ

More IE alternatives means a stronger exhaustified meaning: if IE(ALT') ⊆ IE(ALT), then exhIE ALT φ ⊆ₚ exhIE ALT' φ. More requirements to satisfy → fewer satisfying worlds.

theorem Implicature.FoxSpector2018.de_weakening_of_more_IE {World : Type u_1} (S_cont : Continuation World) (hDE : isDECont S_cont) (ALT ALT' : Set (Prop' World)) (φ : Prop' World) (hIE : Exhaustification.IE ALT' φ ⊆ Exhaustification.IE ALT φ) (w : World) : S_cont (Exhaustification.exhIE ALT' φ) w → S_cont (Exhaustification.exhIE ALT φ) w

Under DE, more IE alternatives weakens the global result. If IE(ALT') ⊆ IE(ALT), then S(exhIE ALT' φ) ⊆ₚ S(exhIE ALT φ).

This captures the core of theorem (88): under DE operators, expanding the comparison class can only weaken the overall sentence. The full theorem (88) additionally handles the two-level exh structure exh_{OP(S)}(OP[exh_C(S)]), but this lemma is the key step.

exh–exh: Conjunctive Readings Under Negation

A key prediction (§11.1): when exh appears both above and below negation, the result is conjunctive:

exh[¬exh(p ∨ q)] = p ∧ q

"Jack didn't talk to Mary OR Sue" (with focused or) yields "Jack talked to both" — embedded exclusive disjunction under negation always produces a conjunctive reading.

The derivation: exh(¬exh(p ∨ q)) = ¬exh(p ∨ q) ∧ (p ∨ q) [exh negates ¬(p∨q)] = [¬(p∨q) ∨ (p∧q)] ∧ (p∨q) [expand ¬exh] = (p ∧ q) [simplify]

inductive Implicature.FoxSpector2018.PQWorld : Type

Four worlds for two atomic propositions p, q.

• pq : PQWorld
• p_only : PQWorld
• q_only : PQWorld
• neither : PQWorld

instance Implicature.FoxSpector2018.instReprPQWorld : Repr PQWorld

Equations

• Implicature.FoxSpector2018.instReprPQWorld = { reprPrec := Implicature.FoxSpector2018.instReprPQWorld.repr }

def Implicature.FoxSpector2018.instReprPQWorld.repr : PQWorld → ℕ → Std.Format

Equations

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

instance Implicature.FoxSpector2018.instDecidableEqPQWorld : DecidableEq PQWorld

Equations

• Implicature.FoxSpector2018.instDecidableEqPQWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Implicature.FoxSpector2018.instBEqPQWorld.beq : PQWorld → PQWorld → Bool

Equations

• Implicature.FoxSpector2018.instBEqPQWorld.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Implicature.FoxSpector2018.instBEqPQWorld : BEq PQWorld

Equations

• Implicature.FoxSpector2018.instBEqPQWorld = { beq := Implicature.FoxSpector2018.instBEqPQWorld.beq }

def Implicature.FoxSpector2018.instInhabitedPQWorld.default : PQWorld

Equations

• Implicature.FoxSpector2018.instInhabitedPQWorld.default = Implicature.FoxSpector2018.PQWorld.pq

instance Implicature.FoxSpector2018.instInhabitedPQWorld : Inhabited PQWorld

Equations

• Implicature.FoxSpector2018.instInhabitedPQWorld = { default := Implicature.FoxSpector2018.instInhabitedPQWorld.default }

theorem Implicature.FoxSpector2018.exh_p_or_q_is_exclusive (w : PQWorld) : Exhaustification.InnocentExclusion.exhB Implicature.FoxSpector2018.pqDomain✝ [Implicature.FoxSpector2018.p_or_q✝, Implicature.FoxSpector2018.p_and_q✝] Implicature.FoxSpector2018.p_or_q✝¹ w = (Implicature.FoxSpector2018.p_or_q✝² w && !Implicature.FoxSpector2018.p_and_q✝¹ w)

exh(p ∨ q) = exclusive or (with alternatives {p∨q, p∧q}).

theorem Implicature.FoxSpector2018.exh_exh_conjunctive (w : PQWorld) : Exhaustification.InnocentExclusion.exhB Implicature.FoxSpector2018.pqDomain✝ [Implicature.FoxSpector2018.neg_exh_p_or_q✝, Implicature.FoxSpector2018.neg_p_or_q✝] Implicature.FoxSpector2018.neg_exh_p_or_q✝¹ w = Implicature.FoxSpector2018.p_and_q✝ w

The exh–exh prediction: exh[¬exh(p∨q)] = p∧q.

The higher exh has alternatives {¬exh(p∨q), ¬(p∨q)}, where ¬(p∨q) is the version without the lower exh. Since ¬(p∨q) is strictly stronger, it is innocently excludable. Negating it adds (p∨q), which combined with ¬exh(p∨q) gives p∧q.

Economy and the Symmetry Problem

Economy interacts with the symmetry problem indirectly. When symmetric alternatives S₁, S₂ are the only non-weaker alternatives, exh is vacuous (symmetric_exhB_vacuous in Symmetry.lean). Vacuous exh violates economy, so the grammar rejects the parse rather than producing wrong results.

Economy and structural complexity are complementary:

• @cite{katzir-2007} determines which alternatives enter the set → breaks symmetry → exh derives the correct SI
• Economy determines whether exh is licensed given those alternatives → blocks vacuous/weakening insertions

theorem Implicature.FoxSpector2018.vacuous_violates_economy {World : Type u_1} (ALT : Set (Prop' World)) (φ : Prop' World) (conts : Set (Continuation World)) (_hne : conts.Nonempty) (hvac : Exhaustification.exhIE ALT φ ≡ₚ φ) (hext : ∀ C ∈ conts, ∀ (p q : Prop' World), (∀ (w : World), p w ↔ q w) → ∀ (w : World), C p w ↔ C q w) : ¬economyConditionMet ALT φ conts

Vacuous exhIE violates economy: if exhIE ≡ₚ φ, then exh is incrementally vacuous for all extensional continuations, so economy is not met.

The extensionality assumption (pointwise-equivalent inputs produce pointwise-equivalent outputs) holds for all natural language continuations: negation, quantifier restrictors, coordination, etc.