Documentation

Linglib.Theories.Semantics.Exhaustification.InnocentExclusion

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 #

SIs are derived by a covert exhaustivity operator exh in the grammar (not pragmatically via NG-MQ)
exh uses innocent exclusion (I-E): exclude only alternatives whose exclusion doesn't force including others
Recursive application of exh derives free choice (FC) for disjunction under existential modals: ◇(p∨q) ⟹ ◇p ∧ ◇q
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 Exhaustification/Operators.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 (ContextualRestriction.symmetry_problem). The problem of which alternatives enter the set is addressed by @cite{katzir-2007}'s structural complexity (Structural.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.InnocentExclusion.sublists {α : Type} :

List α → List (List α)

All sublists (power set) of a list.

Equations

One or more equations did not get rendered due to their size.
Exhaustification.InnocentExclusion.sublists [] = [[]]

Instances For

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

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.

Instances For

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

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.InnocentExclusion.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

Instances For

def Exhaustification.InnocentExclusion.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.

Instances For

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

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.

Instances For

def Exhaustification.InnocentExclusion.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.

Instances For

inductive Exhaustification.InnocentExclusion.PQWorld :

Four propositional worlds for examples with two atomic propositions.

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

Instances For

def Exhaustification.InnocentExclusion.instReprPQWorld.repr :

PQWorld → Nat → Std.Format

Equations

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

Instances For

instance Exhaustification.InnocentExclusion.instReprPQWorld :

Equations

Exhaustification.InnocentExclusion.instReprPQWorld = { reprPrec := Exhaustification.InnocentExclusion.instReprPQWorld.repr }

instance Exhaustification.InnocentExclusion.instDecidableEqPQWorld :

DecidableEq PQWorld

Equations

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

def Exhaustification.InnocentExclusion.instBEqPQWorld.beq :

PQWorld → PQWorld → Bool

Equations

Exhaustification.InnocentExclusion.instBEqPQWorld.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Exhaustification.InnocentExclusion.instBEqPQWorld :

Equations

Exhaustification.InnocentExclusion.instBEqPQWorld = { beq := Exhaustification.InnocentExclusion.instBEqPQWorld.beq }

def Exhaustification.InnocentExclusion.pqDomain :

Equations

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

Instances For

def Exhaustification.InnocentExclusion.pProp :

PQWorld → Bool

Equations

Instances For

def Exhaustification.InnocentExclusion.qProp :

PQWorld → Bool

Equations

Instances For

def Exhaustification.InnocentExclusion.pOrQ :

PQWorld → Bool

Equations

Instances For

def Exhaustification.InnocentExclusion.pAndQ :

PQWorld → Bool

Equations

Instances For

def Exhaustification.InnocentExclusion.disjAlts :

List (PQWorld → Bool)

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

Equations

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

Instances For

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.InnocentExclusion.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.InnocentExclusion.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.InnocentExclusion.disj_ie :

ieIndices pqDomain pOrQ disjAlts = [3]

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

theorem Exhaustification.InnocentExclusion.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.

instance Exhaustification.InnocentExclusion.instReprChW :

Repr Exhaustification.InnocentExclusion.ChW✝

Equations

Exhaustification.InnocentExclusion.instReprChW = { reprPrec := Exhaustification.InnocentExclusion.instReprChW.repr }

def Exhaustification.InnocentExclusion.instReprChW.repr :

Exhaustification.InnocentExclusion.ChW✝ → Nat → Std.Format

Equations

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

Instances For

instance Exhaustification.InnocentExclusion.instDecidableEqChW :

DecidableEq Exhaustification.InnocentExclusion.ChW✝

Equations

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

instance Exhaustification.InnocentExclusion.instBEqChW :

BEq Exhaustification.InnocentExclusion.ChW✝

Equations

Exhaustification.InnocentExclusion.instBEqChW = { beq := Exhaustification.InnocentExclusion.instBEqChW.beq }

def Exhaustification.InnocentExclusion.instBEqChW.beq :

Exhaustification.InnocentExclusion.ChW✝ → Exhaustification.InnocentExclusion.ChW✝ → Bool

Equations

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

Instances For

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.InnocentExclusion.chierchia_exh_preserves_reading :

exhB Exhaustification.InnocentExclusion.chDomain✝ Exhaustification.InnocentExclusion.chAlts✝ Exhaustification.InnocentExclusion.rOrSh✝ Exhaustification.InnocentExclusion.ChW.rOnly✝ = true

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

theorem Exhaustification.InnocentExclusion.chierchia_exh_negates_all (w : Exhaustification.InnocentExclusion.ChW✝) :

exhB Exhaustification.InnocentExclusion.chDomain✝ Exhaustification.InnocentExclusion.chAlts✝ Exhaustification.InnocentExclusion.rOrSh✝ w = true → Exhaustification.InnocentExclusion.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.InnocentExclusion.ModalW :

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

Instances For

instance Exhaustification.InnocentExclusion.instReprModalW :

Equations

Exhaustification.InnocentExclusion.instReprModalW = { reprPrec := Exhaustification.InnocentExclusion.instReprModalW.repr }

def Exhaustification.InnocentExclusion.instReprModalW.repr :

ModalW → Nat → Std.Format

Equations

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

Instances For

instance Exhaustification.InnocentExclusion.instDecidableEqModalW :

DecidableEq ModalW

Equations

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

instance Exhaustification.InnocentExclusion.instBEqModalW :

Equations

Exhaustification.InnocentExclusion.instBEqModalW = { beq := Exhaustification.InnocentExclusion.instBEqModalW.beq }

def Exhaustification.InnocentExclusion.instBEqModalW.beq :

ModalW → ModalW → Bool

Equations

Exhaustification.InnocentExclusion.instBEqModalW.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

def Exhaustification.InnocentExclusion.mDomain :

Equations

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

Instances For

def Exhaustification.InnocentExclusion.diamP :

ModalW → Bool

Equations

Instances For

def Exhaustification.InnocentExclusion.diamQ :

ModalW → Bool

Equations

Instances For

def Exhaustification.InnocentExclusion.diamPorQ :

ModalW → Bool

Equations

Instances For

def Exhaustification.InnocentExclusion.diamPandQ :

ModalW → Bool

Equations

Instances For

def Exhaustification.InnocentExclusion.modalAlts :

List (ModalW → Bool)

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

Equations

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

Instances For

theorem Exhaustification.InnocentExclusion.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.InnocentExclusion.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.InnocentExclusion.exhDiamP :

ModalW → Bool

Equations

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

Instances For

def Exhaustification.InnocentExclusion.exhDiamQ :

ModalW → Bool

Equations

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

Instances For

def Exhaustification.InnocentExclusion.exhDiamPandQ :

ModalW → Bool

Equations

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

Instances For

theorem Exhaustification.InnocentExclusion.exhDiamP_eq (w : ModalW) :

exhDiamP w = (diamP w && !diamQ w)

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

theorem Exhaustification.InnocentExclusion.exhDiamQ_eq (w : ModalW) :

exhDiamQ w = (diamQ w && !diamP w)

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

theorem Exhaustification.InnocentExclusion.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.InnocentExclusion.layer2Alts :

List (ModalW → Bool)

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

Equations

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

Instances For

def Exhaustification.InnocentExclusion.layer1Result :

ModalW → Bool

Layer 1 result as prejacent for layer 2.

Equations

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

Instances For

theorem Exhaustification.InnocentExclusion.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.InnocentExclusion.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.

Relevance-Sensitive EXH #

@cite{magri-2009} §3.2.3 (eq. 42) introduces a relevance-parameterized variant of EXH. A contextually supplied relevance relation R determines which alternatives are "active":

EXH_R(A)(p)(w) = p(w) ∧ ∀q ∈ I-E(p,A). (¬q(w) ∨ ¬R(q))

Alternatives that are not relevant are simply ignored — neither asserted nor negated. This explains why non-mismatching implicatures are optional (the alternative may be irrelevant in context), while mismatching implicatures are mandatory (the alternative is necessarily relevant by postulate (43b): relevance is closed under contextual equivalence, so a mismatching alternative — contextually equivalent to the prejacent — is always relevant).

def Exhaustification.InnocentExclusion.exhR {W : Type} (domain : List W) (alts : List (W → Bool)) (p : W → Bool) (relevant : Nat → Bool) :

W → Bool

Relevance-sensitive exhaustivity operator.

@cite{magri-2009} eq. (42): EXH_R asserts the prejacent and negates only those innocently excludable alternatives that are relevant. Irrelevant alternatives are skipped (the !relevant i disjunct trivializes the conjunct).

When relevant i = true for all i, this reduces to exhB.

Equations

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

Instances For

theorem Exhaustification.InnocentExclusion.exhR_all_relevant_eq_exhB {W : Type} (domain : List W) (alts : List (W → Bool)) (p : W → Bool) :

(exhR domain alts p fun (x : Nat) => true) = exhB domain alts p

When all alternatives are relevant, exhR reduces to exhB.

Universal relevance is the default: exhB is the special case of exhR where every alternative matters.