Spector (2007): Scalar Implicatures: Exhaustivity and Gricean Reasoning

This file formalizes the Gricean derivation of exhaustivity of [Spe07b]. The neo-Gricean rules infer from an utterance that the speaker does not believe any stronger scalar alternative and then, assuming the speaker maximally informed, that the alternative is false; on multiple disjunctions the second step yields unwanted negations, which the alternative-expanding repair of [Sau04] avoids only by an ad hoc scale. The paper replaces the two rules by one reasoning over the question under discussion, a partition ([GS84]): the speaker's information state, relativized to the question, entails the answer and no stronger member of the alternative set, and the hearer assumes the state maximally informed among such states. IsOptimal, optimalStates and maximalStates state this over any partition question, and Implicates what every maximal state entails.

For answers to a question about which atoms hold, states and answers are sets of valuations, the finest question applies, and the alternative set of a positive answer, one that favors no negative literal, is the set of positive answers. isOptimal_iff derives the paper's reduction of optimality to "the answer is the strongest positive proposition the state entails", Pos i = P, and maximalStates_eq its theorem: the unique maximal state is the minimal valuations of P (Minimal), so a positive answer implicates its exhaustification in the sense of Groenendijk and Stokhof. no_unwanted_negation checks the reasoning against the disjunction case: no optimal state for A or B decides A.

Implementation notes

Information states are consistent, so the contradiction is not a state; without this the degenerate case of a single atom would admit the empty state as optimal. Positivity follows the paper's main text, favoring a positive literal and no negative one, which entails the appendix's clause that the proposition is neither the tautology nor the contradiction. The appendix's syntactic theorems, that a proposition favors a literal exactly when every formula expressing it mentions the literal and that positive propositions are those expressible without negation, are not formalized, nor are the alternative sets the paper proposes for negative and quasi-positive answers. The paper's third fact, that removing a minimal valuation from a positive proposition leaves it positive, is bypassed: the proof of the theorem here goes through the reduction directly.

References

• [Spe07b]
• [GS84]
• [Sau04]

The Gricean reasoning over a partition question

def Spector2007.relativize {W : Type u_1} (Q : Setoid W) (i : Set W) : Set W

An information state relativized to the question is the union of the cells it meets.

Equations

• Spector2007.relativize Q i = {w : W | ∃ w' ∈ i, Q w' w}

theorem Spector2007.subset_relativize {W : Type u_1} (Q : Setoid W) (i : Set W) : i ⊆ relativize Q i

@[simp]

theorem Spector2007.relativize_bot {W : Type u_1} (i : Set W) : relativize ⊥ i = i

def Spector2007.StronglyRelevant {W : Type u_1} (Q : Setoid W) (α : Set W) : Prop

An answer is strongly relevant when it excludes a cell and does not cut across cells.

Equations

• Spector2007.StronglyRelevant Q α = ((∃ (w : W), Q.cell w ∩ α = ∅) ∧ ∀ (w : W), w ∈ α ↔ Q.cell w ⊆ α)

def Spector2007.IsOptimal {W : Type u_1} (Q : Setoid W) (S : Set (Set W)) (α i : Set W) : Prop

The answer α is optimal in state i with respect to the alternative set S when the relativized state entails α and no member of S it entails is stronger.

Equations

• Spector2007.IsOptimal Q S α i = (Spector2007.relativize Q i ⊆ α ∧ ∀ α' ∈ S, Spector2007.relativize Q i ⊆ α' → ¬α' ⊂ α)

def Spector2007.optimalStates {W : Type u_1} (Q : Setoid W) (S : Set (Set W)) (α : Set W) : Set (Set W)

The consistent states in which α is optimal.

Equations

• Spector2007.optimalStates Q S α = {i : Set W | i.Nonempty ∧ Spector2007.IsOptimal Q S α i}

def Spector2007.maximalStates {W : Type u_1} (Q : Setoid W) (S : Set (Set W)) (α : Set W) : Set (Set W)

The maximally informed optimal states are those no other optimal state is stronger than.

Equations

• Spector2007.maximalStates Q S α = {i : Set W | i ∈ Spector2007.optimalStates Q S α ∧ ∀ i' ∈ Spector2007.optimalStates Q S α, ¬Spector2007.relativize Q i' ⊂ Spector2007.relativize Q i}

def Spector2007.Implicates {W : Type u_1} (Q : Setoid W) (S : Set (Set W)) (α β : Set W) : Prop

An answer implicates what every maximally informed optimal state entails.

Equations

• Spector2007.Implicates Q S α β = ∀ i ∈ Spector2007.maximalStates Q S α, i ⊆ β

theorem Spector2007.maximalStates_subset {W : Type u_1} (Q : Setoid W) (S : Set (Set W)) (α : Set W) : maximalStates Q S α ⊆ optimalStates Q S α

Positive propositions

@[reducible, inline]

abbrev Spector2007.Valuation (Atom : Type u_1) : Type u_1

A valuation, the set of atoms it makes true.

Equations

• Spector2007.Valuation Atom = Finset Atom

@[reducible, inline]

abbrev Spector2007.Proposition (Atom : Type u_1) : Type u_1

A proposition, the set of valuations making it true.

Equations

• Spector2007.Proposition Atom = Set (Spector2007.Valuation Atom)

inductive Spector2007.Literal (Atom : Type u_1) : Type u_1

A literal is an atom or its negation.

• pos {Atom : Type u_1} (a : Atom) : Literal Atom
• neg {Atom : Type u_1} (a : Atom) : Literal Atom

def Spector2007.instDecidableEqLiteral.decEq {Atom✝ : Type u_1} [DecidableEq Atom✝] (x✝ x✝¹ : Literal Atom✝) : Decidable (x✝ = x✝¹)

Equations

• Spector2007.instDecidableEqLiteral.decEq (Spector2007.Literal.pos a) (Spector2007.Literal.pos b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Spector2007.instDecidableEqLiteral.decEq (Spector2007.Literal.pos a) (Spector2007.Literal.neg a_1) = isFalse ⋯
• Spector2007.instDecidableEqLiteral.decEq (Spector2007.Literal.neg a) (Spector2007.Literal.pos a_1) = isFalse ⋯
• Spector2007.instDecidableEqLiteral.decEq (Spector2007.Literal.neg a) (Spector2007.Literal.neg b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Spector2007.instDecidableEqLiteral {Atom✝ : Type u_1} [DecidableEq Atom✝] : DecidableEq (Literal Atom✝)

Equations

• Spector2007.instDecidableEqLiteral = Spector2007.instDecidableEqLiteral.decEq

def Spector2007.instReprLiteral.repr {Atom✝ : Type u_1} [Repr Atom✝] : Literal Atom✝ → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Spector2007.instReprLiteral {Atom✝ : Type u_1} [Repr Atom✝] : Repr (Literal Atom✝)

Equations

• Spector2007.instReprLiteral = { reprPrec := Spector2007.instReprLiteral.repr }

def Spector2007.Literal.atom {Atom : Type u_1} : Literal Atom → Atom

The atom of a literal.

Equations

• (Spector2007.Literal.pos a).atom = a
• (Spector2007.Literal.neg a).atom = a

def Spector2007.Literal.Holds {Atom : Type u_1} : Literal Atom → Valuation Atom → Prop

The literal holds in a valuation.

Equations

• (Spector2007.Literal.pos a).Holds x✝ = (a ∈ x✝)
• (Spector2007.Literal.neg a).Holds x✝ = (a ∉ x✝)

def Spector2007.Pos {Atom : Type u_1} (P : Proposition Atom) : Proposition Atom

The positive extension of P collects all supersets of its valuations.

Equations

• Spector2007.Pos P = {V : Spector2007.Valuation Atom | ∃ V' ∈ P, V' ⊆ V}

theorem Spector2007.subset_Pos {Atom : Type u_1} (P : Proposition Atom) : P ⊆ Pos P

theorem Spector2007.Pos_mono {Atom : Type u_1} {P P' : Proposition Atom} (h : P ⊆ P') : Pos P ⊆ Pos P'

theorem Spector2007.Pos_setOf_minimal {Atom : Type u_1} (P : Proposition Atom) : Pos {V : Valuation Atom | Minimal (fun (x : Valuation Atom) => x ∈ P) V} = Pos P

Keeping only the minimal valuations does not change the positive extension, the paper's second fact.

theorem Spector2007.setOf_minimal_subset_of_Pos_eq {Atom : Type u_1} {P i : Proposition Atom} (h : Pos i = P) : {V : Valuation Atom | Minimal (fun (x : Valuation Atom) => x ∈ P) V} ⊆ i

The minimal valuations entail every state in which the answer is optimal.

def Spector2007.flip {Atom : Type u_1} [DecidableEq Atom] (V : Valuation Atom) (L : Literal Atom) : Valuation Atom

The valuation identical to V except on the atom of L.

Equations

• Spector2007.flip V L = if h : L.atom ∈ V then Finset.erase V L.atom else Finset.cons L.atom V h

def Spector2007.Favors {Atom : Type u_1} [DecidableEq Atom] (P : Proposition Atom) (L : Literal Atom) : Prop

P favors L when some valuation makes both true and flipping L makes P false.

Equations

• Spector2007.Favors P L = ∃ V ∈ P, L.Holds V ∧ Spector2007.flip V L ∉ P

def Spector2007.IsPositive {Atom : Type u_1} [DecidableEq Atom] (P : Proposition Atom) : Prop

A positive proposition favors a positive literal and no negative one.

Equations

• Spector2007.IsPositive P = ((∃ (a : Atom), Spector2007.Favors P (Spector2007.Literal.pos a)) ∧ ∀ (a : Atom), ¬Spector2007.Favors P (Spector2007.Literal.neg a))

def Spector2007.positives {Atom : Type u_1} [DecidableEq Atom] : Set (Proposition Atom)

The positive propositions, the alternative set of a positive answer.

Equations

• Spector2007.positives = {P : Spector2007.Proposition Atom | Spector2007.IsPositive P}

theorem Spector2007.IsPositive.cons_mem {Atom : Type u_1} [DecidableEq Atom] {P : Proposition Atom} (hP : IsPositive P) {V : Valuation Atom} (hV : V ∈ P) {a : Atom} (ha : a ∉ V) : Finset.cons a V ha ∈ P

A positive proposition contains the valuations extending its valuations by one atom, since otherwise it would favor the negation of that atom.

theorem Spector2007.IsPositive.mem_of_subset {Atom : Type u_1} [DecidableEq Atom] {P : Proposition Atom} (hP : IsPositive P) {V' V : Valuation Atom} (hV' : V' ∈ P) (hle : V' ⊆ V) : V ∈ P

A positive proposition is closed upward.

theorem Spector2007.IsPositive.nonempty {Atom : Type u_1} [DecidableEq Atom] {P : Proposition Atom} (hP : IsPositive P) : Set.Nonempty P

theorem Spector2007.IsPositive.ne_univ {Atom : Type u_1} [DecidableEq Atom] {P : Proposition Atom} (hP : IsPositive P) : P ≠ Set.univ

theorem Spector2007.isPositive_of_upward {Atom : Type u_1} [DecidableEq Atom] {P : Proposition Atom} (hne : Set.Nonempty P) (hnu : P ≠ Set.univ) (hup : ∀ V ∈ P, ∀ (V' : Valuation Atom), V ⊆ V' → V' ∈ P) : IsPositive P

A nonempty, non-universal, upward-closed proposition is positive: it favors the atoms of its minimal valuations and no negative literal.

theorem Spector2007.Pos_of_isPositive {Atom : Type u_1} [DecidableEq Atom] {P : Proposition Atom} (hP : IsPositive P) : Pos P = P

A positive proposition is its own positive extension, the paper's first fact.

theorem Spector2007.Pos_isPositive {Atom : Type u_1} [DecidableEq Atom] {i : Proposition Atom} (hi : Set.Nonempty i) (hnu : Pos i ≠ Set.univ) : IsPositive (Pos i)

The positive extension of a consistent state that does not exclude nothing is positive: the strongest positive proposition the state entails.

The reduction and the theorem

theorem Spector2007.isOptimal_iff {Atom : Type u_1} [DecidableEq Atom] {P i : Proposition Atom} (hP : IsPositive P) (hi : Set.Nonempty i) : IsOptimal ⊥ positives P i ↔ Pos i = P

A positive answer is optimal in a consistent state exactly when it is the strongest positive proposition the state entails, the paper's reduction.

theorem Spector2007.optimalStates_eq {Atom : Type u_1} [DecidableEq Atom] {P : Proposition Atom} (hP : IsPositive P) : optimalStates ⊥ positives P = {i : Proposition Atom | Set.Nonempty i ∧ Pos i = P}

theorem Spector2007.maximalStates_eq {Atom : Type u_1} [DecidableEq Atom] {P : Proposition Atom} (hP : IsPositive P) : maximalStates ⊥ positives P = {{V : Valuation Atom | Minimal (fun (x : Valuation Atom) => x ∈ P) V}}

For a positive answer the unique maximally informed optimal state is its exhaustification, the paper's theorem.

theorem Spector2007.implicates_setOf_minimal {Atom : Type u_1} [DecidableEq Atom] {P : Proposition Atom} (hP : IsPositive P) : Implicates ⊥ positives P {V : Valuation Atom | Minimal (fun (x : Valuation Atom) => x ∈ P) V}

A positive answer implicates its exhaustification, its minimal valuations.

Disjunction

def Spector2007.atomProp {Atom : Type u_1} (a : Atom) : Proposition Atom

The proposition that a holds.

Equations

• Spector2007.atomProp a = {V : Spector2007.Valuation Atom | a ∈ V}

def Spector2007.orProp {Atom : Type u_1} (a b : Atom) : Proposition Atom

A or B.

Equations

• Spector2007.orProp a b = {V : Spector2007.Valuation Atom | a ∈ V ∨ b ∈ V}

def Spector2007.exclOr {Atom : Type u_1} (a b : Atom) : Proposition Atom

Only A or only B.

Equations

• Spector2007.exclOr a b = {V : Spector2007.Valuation Atom | V = {a} ∨ V = {b}}

theorem Spector2007.orProp_isPositive {Atom : Type u_1} [DecidableEq Atom] (a b : Atom) : IsPositive (orProp a b)

theorem Spector2007.setOf_minimal_orProp {Atom : Type u_1} [DecidableEq Atom] (a b : Atom) : {V : Valuation Atom | Minimal (fun (x : Valuation Atom) => x ∈ orProp a b) V} = exclOr a b

The exhaustification of A or B is exclusive, only A or only B.

theorem Spector2007.orProp_implicates_exclOr {Atom : Type u_1} [DecidableEq Atom] (a b : Atom) : Implicates ⊥ positives (orProp a b) (exclOr a b)

A or B implicates only A or only B.

theorem Spector2007.no_unwanted_negation {Atom : Type u_1} [DecidableEq Atom] {a b : Atom} (hab : a ≠ b) {i : Proposition Atom} (hi : i ∈ optimalStates ⊥ positives (orProp a b)) : ¬i ⊆ atomProp a ∧ ¬i ⊆ (atomProp a)ᶜ

No state in which A or B is optimal decides A, so there is no unwanted negation: a state entailing A would have A as a better answer and one entailing not A would have B.