Fox 2007: Free Choice and the Theory of Scalar Implicatures

@cite{fox-2007}

Danny Fox, "Free Choice and the Theory of Scalar Implicatures." In Sauerland & Stateva (eds.), Presupposition and Implicature in Compositional Semantics, pp. 71--120. Palgrave Macmillan.

Core Ideas

1. SIs are derived by a covert exhaustivity operator exh in the grammar (not pragmatically via NG-MQ)
2. exh uses innocent exclusion (I-E): exclude only alternatives whose exclusion doesn't force including others
3. Recursive application of exh derives free choice (FC) for disjunction under existential modals: ◇(p∨q) ⟹ ◇p ∧ ◇q
4. The system resolves Chierchia's puzzle about embedded disjunction

Computable Algorithm

This file provides a computable (Bool/List) implementation of Fox's innocent exclusion algorithm, complementing the Set-theoretic version in Exhaustivity/Basic.lean (@cite{spector-2016}). The definitions are:

• nonWeakerIndices: NW(p, A) — alternatives not entailed by prejacent
• exclusionConsistent: consistency of {p} ∪ {¬q : q ∈ excl}
• maxConsistentExclusions: maximal consistent exclusion sets
• ieIndices: I-E(p, A) — innocently excludable alternatives
• exhB: the exhaustivity operator (Bool version)

Key Results

• disj_exh_eq_exor: Exh(Alt)(p∨q) = p ⊻ q (exclusive or)
• chierchia_puzzle_ie: exh resolves Chierchia's puzzle (§4)
• free_choice: Exh²(◇(p∨q)) = ◇p ∧ ◇q ∧ ¬◇(p∧q) (§7.2)

Connection to the Symmetry Problem

Innocent exclusion was designed to handle symmetric alternatives (see Symmetry.lean): when S₁, S₂ partition S's denotation, excluding both is inconsistent, so they land in different MCEs and neither is in I-E. This correctly predicts that exh is vacuous when the alternative set contains both symmetric partners (FoxKatzir2011.symmetry_problem). The problem of which alternatives enter the set is addressed by @cite{katzir-2007}'s structural complexity (StructuralAlternatives.lean).

Duality with Santorio 2018

Fox's innocent exclusion is the dual of @cite{santorio-2018}'s stability algorithm (footnote 40, p. 540). This duality is verified computationally in Semantics/Conditionals/AlternativeSensitive.lean, which imports this file and proves the correspondence.

def Exhaustification.Fox2007.sublists {α : Type} : List α → List (List α)

All sublists (power set) of a list.

Equations

• Exhaustification.Fox2007.sublists [] = [[]]
• Exhaustification.Fox2007.sublists (x_1 :: xs) = Exhaustification.Fox2007.sublists xs ++ List.map (fun (x : List α) => x_1 :: x) (Exhaustification.Fox2007.sublists xs)

def Exhaustification.Fox2007.nonWeakerIndices {W : Type} (domain : List W) (p : W → Bool) (alts : List (W → Bool)) : List Nat

Non-weaker alternatives (by index): alternatives not entailed by p. NW(p, A) = {q ∈ A : p ⊭ q}, i.e., there exists a world where p is true but q is false.

Equations

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

def Exhaustification.Fox2007.exclusionConsistent {W : Type} (domain : List W) (p : W → Bool) (alts : List (W → Bool)) (excl : List Nat) : Bool

Consistency of an exclusion: {p} ∪ {¬q : q ∈ excl} is satisfiable. There exists a world where p holds and all excluded alternatives are false.

Equations

• Exhaustification.Fox2007.exclusionConsistent domain p alts excl = domain.any fun (w : W) => p w && (List.filterMap (fun (i : Nat) => alts[i]?) excl).all fun (q : W → Bool) => !q w

def Exhaustification.Fox2007.maxConsistentExclusions {W : Type} (domain : List W) (p : W → Bool) (alts : List (W → Bool)) : List (List Nat)

Maximal consistent exclusions: maximal subsets A' ⊆ NW(p, A) such that {p} ∪ {¬q : q ∈ A'} is consistent.

These are Fox's MC-sets projected to the excludable alternatives. The intersection of all maximal exclusions gives I-E.

Equations

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

def Exhaustification.Fox2007.ieIndices {W : Type} (domain : List W) (p : W → Bool) (alts : List (W → Bool)) : List Nat

Innocently excludable alternatives (by index): those appearing in every maximal consistent exclusion.

I-E(p, A) = ⋂ {A' : A' is a maximal consistent exclusion}

An alternative is innocently excludable iff excluding it doesn't force including some other alternative — i.e., it can be excluded no matter which maximal exclusion we choose.

Equations

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

def Exhaustification.Fox2007.exhB {W : Type} (domain : List W) (alts : List (W → Bool)) (p : W → Bool) : W → Bool

The exhaustivity operator (computable Bool version).

⟦Exh⟧(A)(p)(w) ⟺ p(w) ∧ ∀q ∈ I-E(p, A). ¬q(w)

Asserts the prejacent and negates every innocently excludable alternative.

Equations

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

inductive Exhaustification.Fox2007.PQWorld : Type

Four propositional worlds for examples with two atomic propositions.

• pOnly : PQWorld
• qOnly : PQWorld
• both : PQWorld
• neither : PQWorld

instance Exhaustification.Fox2007.instReprPQWorld : Repr PQWorld

Equations

• Exhaustification.Fox2007.instReprPQWorld = { reprPrec := Exhaustification.Fox2007.instReprPQWorld.repr }

def Exhaustification.Fox2007.instReprPQWorld.repr : PQWorld → Nat → Std.Format

Equations

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

instance Exhaustification.Fox2007.instDecidableEqPQWorld : DecidableEq PQWorld

Equations

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

def Exhaustification.Fox2007.instBEqPQWorld.beq : PQWorld → PQWorld → Bool

Equations

• Exhaustification.Fox2007.instBEqPQWorld.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Exhaustification.Fox2007.instBEqPQWorld : BEq PQWorld

Equations

• Exhaustification.Fox2007.instBEqPQWorld = { beq := Exhaustification.Fox2007.instBEqPQWorld.beq }

def Exhaustification.Fox2007.pqDomain : List PQWorld

Equations

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

def Exhaustification.Fox2007.pProp : PQWorld → Bool

Equations

• Exhaustification.Fox2007.pProp Exhaustification.Fox2007.PQWorld.pOnly = true
• Exhaustification.Fox2007.pProp Exhaustification.Fox2007.PQWorld.both = true
• Exhaustification.Fox2007.pProp x✝ = false

def Exhaustification.Fox2007.qProp : PQWorld → Bool

Equations

• Exhaustification.Fox2007.qProp Exhaustification.Fox2007.PQWorld.qOnly = true
• Exhaustification.Fox2007.qProp Exhaustification.Fox2007.PQWorld.both = true
• Exhaustification.Fox2007.qProp x✝ = false

def Exhaustification.Fox2007.pOrQ : PQWorld → Bool

Equations

• Exhaustification.Fox2007.pOrQ Exhaustification.Fox2007.PQWorld.neither = false
• Exhaustification.Fox2007.pOrQ x✝ = true

def Exhaustification.Fox2007.pAndQ : PQWorld → Bool

Equations

• Exhaustification.Fox2007.pAndQ Exhaustification.Fox2007.PQWorld.both = true
• Exhaustification.Fox2007.pAndQ x✝ = false

def Exhaustification.Fox2007.disjAlts : List (PQWorld → Bool)

Sauerland alternatives for p∨q: {p∨q, p, q, p∧q}.

Equations

• Exhaustification.Fox2007.disjAlts = [Exhaustification.Fox2007.pOrQ, Exhaustification.Fox2007.pProp, Exhaustification.Fox2007.qProp, Exhaustification.Fox2007.pAndQ]

Simple Disjunction: p∨q → ExOR

With Sauerland alternatives Alt(p∨q) = {p∨q, p, q, p∧q}:

• NW(p∨q) = {p, q, p∧q} (none entailed by p∨q)
• Maximal consistent exclusions: {q, p∧q} and {p, p∧q} (can't exclude both p and q: (p∨q) ∧ ¬p ∧ ¬q is contradictory)
• I-E = {p∧q} (the only alternative in both exclusions)
• Exh(Alt)(p∨q) = (p∨q) ∧ ¬(p∧q) = exclusive or

theorem Exhaustification.Fox2007.disj_nonWeaker : nonWeakerIndices pqDomain pOrQ disjAlts = [1, 2, 3]

The non-weaker alternatives are p, q, and p∧q (indices 1, 2, 3).

theorem Exhaustification.Fox2007.disj_maxExclusions : maxConsistentExclusions pqDomain pOrQ disjAlts = [[2, 3], [1, 3]]

Two maximal consistent exclusions: {q, p∧q} and {p, p∧q}. Excluding both p and q simultaneously is inconsistent with p∨q.

theorem Exhaustification.Fox2007.disj_ie : ieIndices pqDomain pOrQ disjAlts = [3]

p∧q (index 3) is the only innocently excludable alternative.

theorem Exhaustification.Fox2007.disj_exh_eq_exor (w : PQWorld) : exhB pqDomain disjAlts pOrQ w = (pOrQ w && !pAndQ w)

Exh(Alt)(p∨q) = exclusive or: the prejacent conjoined with ¬(p∧q). This is the standard scalar implicature for disjunction.

Chierchia's Puzzle: Embedded Disjunction

@cite{chierchia-2004} observed that when a scalar item is embedded in a disjunction, the standard neo-Gricean system (NG-MQ) derives the wrong implicature.

Example: "John did the reading or some of the homework."

• r ∨ sh, with stronger alternative r ∨ ah (all homework)
• The correct SI: ¬ah (John didn't do ALL the homework)
• NG-MQ's SI: ¬(r ∨ ah) = ¬r ∧ ¬ah (too strong — negates r too!)

Fox's solution: exh correctly derives ¬ah without ¬r, because ah is the only innocently excludable alternative among the relevant ones.

def Exhaustification.Fox2007.instReprChW.repr : Exhaustification.Fox2007.ChW✝ → Nat → Std.Format

Equations

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

instance Exhaustification.Fox2007.instReprChW : Repr Exhaustification.Fox2007.ChW✝

Equations

• Exhaustification.Fox2007.instReprChW = { reprPrec := Exhaustification.Fox2007.instReprChW.repr }

instance Exhaustification.Fox2007.instDecidableEqChW : DecidableEq Exhaustification.Fox2007.ChW✝

Equations

• Exhaustification.Fox2007.instDecidableEqChW x✝ y✝ = if h : Exhaustification.Fox2007.ChW.ctorIdx✝ x✝ = Exhaustification.Fox2007.ChW.ctorIdx✝¹ y✝ then isTrue ⋯ else isFalse ⋯

instance Exhaustification.Fox2007.instBEqChW : BEq Exhaustification.Fox2007.ChW✝

Equations

• Exhaustification.Fox2007.instBEqChW = { beq := Exhaustification.Fox2007.instBEqChW.beq }

def Exhaustification.Fox2007.instBEqChW.beq : Exhaustification.Fox2007.ChW✝ → Exhaustification.Fox2007.ChW✝ → Bool

Equations

• Exhaustification.Fox2007.instBEqChW.beq x✝ y✝ = (Exhaustification.Fox2007.ChW.ctorIdx✝ x✝ == Exhaustification.Fox2007.ChW.ctorIdx✝¹ y✝)

theorem Exhaustification.Fox2007.chierchia_puzzle_ie : have ie := ieIndices Exhaustification.Fox2007.chDomain✝ Exhaustification.Fox2007.rOrSh✝ Exhaustification.Fox2007.chAlts✝; ie.contains 6 = true ∧ ie.contains 5 = true ∧ ie.contains 1 = false ∧ ie.contains 4 = false

Chierchia's puzzle: NG-MQ would derive SI = ¬(r∨ah) = ¬r ∧ ¬ah, which negates the first disjunct. Fox's exh correctly identifies that only ah (index 6) and r∧ah (index 5) are innocently excludable — NOT r or r∨ah.

theorem Exhaustification.Fox2007.chierchia_exh_preserves_reading : exhB Exhaustification.Fox2007.chDomain✝ Exhaustification.Fox2007.chAlts✝ Exhaustification.Fox2007.rOrSh✝ Exhaustification.Fox2007.ChW.rOnly✝ = true

exh correctly preserves the first disjunct's truth value: the exhaustified meaning is consistent with r being true.

theorem Exhaustification.Fox2007.chierchia_exh_negates_all (w : Exhaustification.Fox2007.ChW✝) : exhB Exhaustification.Fox2007.chDomain✝ Exhaustification.Fox2007.chAlts✝ Exhaustification.Fox2007.rOrSh✝ w = true → Exhaustification.Fox2007.allHW✝ w = false

exh correctly negates the stronger alternative: the exhaustified meaning entails ¬ah (not all homework).

Free Choice via Double Exhaustification

The key result: recursive exhaustification derives the conjunctive interpretation of disjunction under existential modals.

Layer 1: Exh(C)(◇(p∨q)) = ◇(p∨q) ∧ ¬◇(p∧q)

• Excludes ◇(p∧q) but NOT ◇p or ◇q (excluding one forces the other)
• Consistent with FC but doesn't assert it

Layer 2: Exh(C')[Exh(C)(◇(p∨q))] = ◇p ∧ ◇q ∧ ¬◇(p∧q)

• Alternatives are {Exh(C)(φ) : φ ∈ C}
• Exh(C)(◇p) = ◇p ∧ ¬◇q, Exh(C)(◇q) = ◇q ∧ ¬◇p
• Both are innocently excludable at the second layer
• Their exclusion forces ◇p ∧ ◇q — free choice!

inductive Exhaustification.Fox2007.ModalW : Type

Modal worlds: each represents which propositional situations are accessible. Named by which ◇-propositions they make true.

• seesP : ModalW
• seesQ : ModalW
• seesPQ : ModalW
• seesBoth : ModalW
• seesNothing : ModalW

def Exhaustification.Fox2007.instReprModalW.repr : ModalW → Nat → Std.Format

Equations

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

instance Exhaustification.Fox2007.instReprModalW : Repr ModalW

Equations

• Exhaustification.Fox2007.instReprModalW = { reprPrec := Exhaustification.Fox2007.instReprModalW.repr }

instance Exhaustification.Fox2007.instDecidableEqModalW : DecidableEq ModalW

Equations

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

def Exhaustification.Fox2007.instBEqModalW.beq : ModalW → ModalW → Bool

Equations

• Exhaustification.Fox2007.instBEqModalW.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Exhaustification.Fox2007.instBEqModalW : BEq ModalW

Equations

• Exhaustification.Fox2007.instBEqModalW = { beq := Exhaustification.Fox2007.instBEqModalW.beq }

def Exhaustification.Fox2007.mDomain : List ModalW

Equations

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

def Exhaustification.Fox2007.diamP : ModalW → Bool

Equations

• Exhaustification.Fox2007.diamP Exhaustification.Fox2007.ModalW.seesP = true
• Exhaustification.Fox2007.diamP Exhaustification.Fox2007.ModalW.seesPQ = true
• Exhaustification.Fox2007.diamP Exhaustification.Fox2007.ModalW.seesBoth = true
• Exhaustification.Fox2007.diamP x✝ = false

def Exhaustification.Fox2007.diamQ : ModalW → Bool

Equations

• Exhaustification.Fox2007.diamQ Exhaustification.Fox2007.ModalW.seesQ = true
• Exhaustification.Fox2007.diamQ Exhaustification.Fox2007.ModalW.seesPQ = true
• Exhaustification.Fox2007.diamQ Exhaustification.Fox2007.ModalW.seesBoth = true
• Exhaustification.Fox2007.diamQ x✝ = false

def Exhaustification.Fox2007.diamPorQ : ModalW → Bool

Equations

• Exhaustification.Fox2007.diamPorQ Exhaustification.Fox2007.ModalW.seesNothing = false
• Exhaustification.Fox2007.diamPorQ x✝ = true

def Exhaustification.Fox2007.diamPandQ : ModalW → Bool

Equations

• Exhaustification.Fox2007.diamPandQ Exhaustification.Fox2007.ModalW.seesBoth = true
• Exhaustification.Fox2007.diamPandQ x✝ = false

def Exhaustification.Fox2007.modalAlts : List (ModalW → Bool)

Sauerland alternatives under ◇: {◇(p∨q), ◇p, ◇q, ◇(p∧q)}.

Equations

• Exhaustification.Fox2007.modalAlts = [Exhaustification.Fox2007.diamPorQ, Exhaustification.Fox2007.diamP, Exhaustification.Fox2007.diamQ, Exhaustification.Fox2007.diamPandQ]

theorem Exhaustification.Fox2007.modal_ie_layer1 : ieIndices mDomain diamPorQ modalAlts = [3]

◇(p∧q) is the only innocently excludable alternative at layer 1. ◇p and ◇q cannot be innocently excluded: excluding ◇p while keeping ◇(p∨q) forces ◇q, and vice versa.

theorem Exhaustification.Fox2007.modal_exh1 (w : ModalW) : exhB mDomain modalAlts diamPorQ w = (diamPorQ w && !diamPandQ w)

Layer 1: Exh(C)(◇(p∨q)) = ◇(p∨q) ∧ ¬◇(p∧q). Consistent with FC (◇p ∧ ◇q) but doesn't yet assert it.

def Exhaustification.Fox2007.exhDiamP : ModalW → Bool

Equations

• Exhaustification.Fox2007.exhDiamP = Exhaustification.Fox2007.exhB Exhaustification.Fox2007.mDomain Exhaustification.Fox2007.modalAlts Exhaustification.Fox2007.diamP

def Exhaustification.Fox2007.exhDiamQ : ModalW → Bool

Equations

• Exhaustification.Fox2007.exhDiamQ = Exhaustification.Fox2007.exhB Exhaustification.Fox2007.mDomain Exhaustification.Fox2007.modalAlts Exhaustification.Fox2007.diamQ

def Exhaustification.Fox2007.exhDiamPandQ : ModalW → Bool

Equations

• Exhaustification.Fox2007.exhDiamPandQ = Exhaustification.Fox2007.exhB Exhaustification.Fox2007.mDomain Exhaustification.Fox2007.modalAlts Exhaustification.Fox2007.diamPandQ

theorem Exhaustification.Fox2007.exhDiamP_eq (w : ModalW) : exhDiamP w = (diamP w && !diamQ w)

Exh(C)(◇p) = ◇p ∧ ¬◇q: exhaustifying ◇p excludes ◇q.

theorem Exhaustification.Fox2007.exhDiamQ_eq (w : ModalW) : exhDiamQ w = (diamQ w && !diamP w)

Exh(C)(◇q) = ◇q ∧ ¬◇p: symmetric to ◇p.

theorem Exhaustification.Fox2007.exhDiamPandQ_eq (w : ModalW) : exhDiamPandQ w = diamPandQ w

Exh(C)(◇(p∧q)) = ◇(p∧q): no non-weaker alternatives (◇(p∧q) entails all of ◇p, ◇q, ◇(p∨q)).

def Exhaustification.Fox2007.layer2Alts : List (ModalW → Bool)

Layer 2 alternatives: {Exh(C)(φ) : φ ∈ C}.

Equations

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

def Exhaustification.Fox2007.layer1Result : ModalW → Bool

Layer 1 result as prejacent for layer 2.

Equations

• Exhaustification.Fox2007.layer1Result = Exhaustification.Fox2007.exhB Exhaustification.Fox2007.mDomain Exhaustification.Fox2007.modalAlts Exhaustification.Fox2007.diamPorQ

theorem Exhaustification.Fox2007.free_choice (w : ModalW) : exhB mDomain layer2Alts layer1Result w = (diamP w && diamQ w && !diamPandQ w)

Free Choice: double exhaustification yields ◇p ∧ ◇q ∧ ¬◇(p∧q).

Exh(C')[Exh(C)(◇(p∨q))] asserts:

• ◇p ∧ ◇q (free choice permission)
• ¬◇(p∧q) (anti-conjunctive inference)

The FC inference ◇p ∧ ◇q arises because the second layer excludes Exh(C)(◇p) = ◇p∧¬◇q and Exh(C)(◇q) = ◇q∧¬◇p, whose negation (given the prejacent) forces both ◇p and ◇q to hold.

theorem Exhaustification.Fox2007.fc_entails_both_disjuncts (w : ModalW) (h : exhB mDomain layer2Alts layer1Result w = true) : diamP w = true ∧ diamQ w = true

FC entails both disjuncts hold: the speaker has permission for each disjunct individually.