Franke 2011: Quantity implicatures and rational conversation

[Fra11], S&P 4(1): IBR (iterated best response) converges to exhaustive interpretation (exhMW; the paper writes ExhMM).

The IBR machinery (IBR.lean, ScalarGames.lean, Convergence.lean, RSABridge.lean) lives in this paper's directory over the shared InterpGame carrier. This file contains the exhaustification facts and worked examples:

• Facts 1, 3, 4 connecting IBR to the exhaustification literature
• Alternative counting (eq. (107)) and the R₁ characterization
• Concrete examples (scalar implicature, free choice disjunction)

Alternative counting ([Fra11] eq. (107))

def Franke2011.alternativeCount {T : Type u_1} {M : Type u_2} [Fintype M] (G : InterpGame T M) (s : T) : ℕ

Number of alternatives (messages) true at state s. This is |R⁻¹₀(s)| in Franke's notation.

Equations

• Franke2011.alternativeCount G s = (G.trueMessages s).card

def Franke2011.isMinimalByAltCount {T : Type u_1} {M : Type u_2} [Fintype M] (G : InterpGame T M) (m : M) (s : T) : Prop

A state s is minimal among m-worlds if no m-world has fewer true alternatives. This characterizes R₁(m) per equation (107).

Equations

• Franke2011.isMinimalByAltCount G m s = (G.meaning m s ∧ ∀ (s' : T), G.meaning m s' → Franke2011.alternativeCount G s ≤ Franke2011.alternativeCount G s')

Fact 1: R₁ ⊆ ExhMW ([Fra11] §10)

theorem Franke2011.r1_subset_exhMW {T : Type u_1} {M : Type u_2} [Fintype M] (G : InterpGame T M) (m : M) (s : T) (h : isMinimalByAltCount G m s) : Exhaustification.exhMW (toAlternatives G) (prejacent G m) s

Franke Fact 1 (containment direction): Level-1 receiver interpretation is contained in minimal-models exhaustification.

R₁(mₛ) ⊆ ExhMM(S)

Proof idea: If s is selected by R₁ (minimum alternative count), then s is minimal with respect to <_ALT because:

• s' <_ALT s means s' makes strictly fewer alternatives true
• But R₁ already selected for minimum alternative count
• So no such s' can exist among m-worlds

This is the containment direction; equality requires "homogeneity".

Conditions for the converse (ExhMW ⊆ R₁)

def Franke2011.altOrderingTotalOnMessage {T : Type u_1} {M : Type u_2} [Fintype M] (G : InterpGame T M) (m : M) : Prop

The alternative ordering is total on m-worlds if for any two states where m is true, one's true alternatives are a subset of the other's.

Equations

• Franke2011.altOrderingTotalOnMessage G m = ∀ (s s' : T), G.meaning m s → G.meaning m s' → G.trueMessages s ⊆ G.trueMessages s' ∨ G.trueMessages s' ⊆ G.trueMessages s

theorem Franke2011.exhMW_subset_r1_under_totality {T : Type u_1} {M : Type u_2} [Fintype M] [DecidableEq M] (G : InterpGame T M) (m : M) (s : T) (hTotal : altOrderingTotalOnMessage G m) (hmw : Exhaustification.exhMW (toAlternatives G) (prejacent G m) s) : isMinimalByAltCount G m s

Converse direction under totality: ExhMW ⊆ R₁.

When <_ALT is total on m-worlds, minimal in the subset ordering implies minimum cardinality.

theorem Franke2011.r1_eq_exhMW_under_totality {T : Type u_1} {M : Type u_2} [Fintype M] [DecidableEq M] (G : InterpGame T M) (m : M) (s : T) (hTotal : altOrderingTotalOnMessage G m) : isMinimalByAltCount G m s ↔ Exhaustification.exhMW (toAlternatives G) (prejacent G m) s

R₁ = ExhMW under totality: Full equivalence when alternatives form a chain.

Totality is a sufficient condition for [Fra11]'s Fact 1 to become an equality; the paper's own sufficient condition is "homogeneity" of the alternative set.

Fact 3: ExhMW ⊆ ExhIE ([Fra11] Appendix A)

theorem Franke2011.fact3_exhMW_subset_exhIE {T : Type u_1} {M : Type u_2} (G : InterpGame T M) (m : M) : Exhaustification.exhMW (toAlternatives G) (prejacent G m) ⊆ Exhaustification.exhIE (toAlternatives G) (prejacent G m)

Franke Fact 3 (Appendix A): ExhMW(S, Alt) ⊆ ExhIE(S, Alt)

This is already proved as exhMW_entails_exhIE in Exhaustification/Operators/Basic.lean.

Fact 4: ExhMW = ExhIE under closure ([Fra11] Appendix A)

theorem Franke2011.fact4_exhMW_eq_exhIE_closed {T : Type u_1} {M : Type u_2} (G : InterpGame T M) (m : M) (hClosed : Exhaustification.closedUnderConj (toAlternatives G)) : Exhaustification.exhMW (toAlternatives G) (prejacent G m) = Exhaustification.exhIE (toAlternatives G) (prejacent G m)

Franke Fact 4 (Appendix A): ExhMW = ExhIE when Alt is closed under ∧.

This is proved as exhMW_eq_exhIE_of_closedUnderConj in Exhaustification/Operators/Basic.lean.

Scalar Implicature Example (Franke Section 3.1)

The classic "some" vs "all" example:

• States: {some-not-all, all}
• Messages: {some, all}
• Meaning: some true at both; all true only at all

IBR derivation:

• L₀: "some" → uniform over both states
• S₁ at "all": says "all" (more informative)
• S₁ at "some-not-all": says "some" (only option)
• L₂: "some" → "some-not-all" (scalar implicature!)

inductive Franke2011.ScalarState : Type

States for scalar implicature example

• someNotAll : ScalarState
• all : ScalarState

@[implicit_reducible]

instance Franke2011.instDecidableEqScalarState : DecidableEq ScalarState

Equations

• Franke2011.instDecidableEqScalarState x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Franke2011.instFintypeScalarState : Fintype ScalarState

Equations

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

@[implicit_reducible]

instance Franke2011.instReprScalarState : Repr ScalarState

Equations

• Franke2011.instReprScalarState = { reprPrec := Franke2011.instReprScalarState.repr }

def Franke2011.instReprScalarState.repr : ScalarState → ℕ → Std.Format

Equations

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

inductive Franke2011.ScalarMessage : Type

Messages for scalar implicature example

• some_ : ScalarMessage
• all : ScalarMessage

@[implicit_reducible]

instance Franke2011.instDecidableEqScalarMessage : DecidableEq ScalarMessage

Equations

• Franke2011.instDecidableEqScalarMessage x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Franke2011.instFintypeScalarMessage : Fintype ScalarMessage

Equations

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

def Franke2011.instReprScalarMessage.repr : ScalarMessage → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Franke2011.instReprScalarMessage : Repr ScalarMessage

Equations

• Franke2011.instReprScalarMessage = { reprPrec := Franke2011.instReprScalarMessage.repr }

def Franke2011.scalarGame : InterpGame ScalarState ScalarMessage

Scalar implicature interpretation game

Equations

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

theorem Franke2011.scalarGame_is_scalar : isScalarGame scalarGame

The scalar implicature game IS a scalar game: truth sets are nested.

theorem Franke2011.scalarGame_distinct : Function.Injective scalarGame.trueStates

The scalar implicature game has distinct truth sets.

Free Choice Disjunction (Franke Section 3.3)

"You may have cake or ice cream" → You may have either one.

States: {only-A, only-B, either, both} Messages: {◇A, ◇B, ◇(A∨B), ◇(A∧B)}

The free choice inference emerges from IBR reasoning because:

• At "either" state, speaker uses ◇(A∨B) (most informative true message)
• L₂ infers "either" from ◇(A∨B) (scalar implicature pattern)

inductive Franke2011.FCState : Type

States for free choice example

• onlyA : FCState
• onlyB : FCState
• either : FCState
• both : FCState

@[implicit_reducible]

instance Franke2011.instDecidableEqFCState : DecidableEq FCState

Equations

• Franke2011.instDecidableEqFCState x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Franke2011.instFintypeFCState : Fintype FCState

Equations

• Franke2011.instFintypeFCState = { elems := { val := ↑Franke2011.FCState.enumList, nodup := Franke2011.FCState.enumList_nodup }, complete := Franke2011.instFintypeFCState._proof_1 }

@[implicit_reducible]

instance Franke2011.instReprFCState : Repr FCState

Equations

• Franke2011.instReprFCState = { reprPrec := Franke2011.instReprFCState.repr }

def Franke2011.instReprFCState.repr : FCState → ℕ → Std.Format

Equations

• Franke2011.instReprFCState.repr Franke2011.FCState.onlyA prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Franke2011.FCState.onlyA")).group prec✝
• Franke2011.instReprFCState.repr Franke2011.FCState.onlyB prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Franke2011.FCState.onlyB")).group prec✝
• Franke2011.instReprFCState.repr Franke2011.FCState.either prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Franke2011.FCState.either")).group prec✝
• Franke2011.instReprFCState.repr Franke2011.FCState.both prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Franke2011.FCState.both")).group prec✝

inductive Franke2011.FCMessage : Type

Messages for free choice example

• mayA : FCMessage
• mayB : FCMessage
• mayAorB : FCMessage
• mayAandB : FCMessage

@[implicit_reducible]

instance Franke2011.instDecidableEqFCMessage : DecidableEq FCMessage

Equations

• Franke2011.instDecidableEqFCMessage x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Franke2011.instFintypeFCMessage : Fintype FCMessage

Equations

• Franke2011.instFintypeFCMessage = { elems := { val := ↑Franke2011.FCMessage.enumList, nodup := Franke2011.FCMessage.enumList_nodup }, complete := Franke2011.instFintypeFCMessage._proof_1 }

def Franke2011.instReprFCMessage.repr : FCMessage → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Franke2011.instReprFCMessage.repr Franke2011.FCMessage.mayA prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Franke2011.FCMessage.mayA")).group prec✝
• Franke2011.instReprFCMessage.repr Franke2011.FCMessage.mayB prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Franke2011.FCMessage.mayB")).group prec✝

@[implicit_reducible]

instance Franke2011.instReprFCMessage : Repr FCMessage

Equations

• Franke2011.instReprFCMessage = { reprPrec := Franke2011.instReprFCMessage.repr }

def Franke2011.freeChoiceGame : InterpGame FCState FCMessage

Free choice interpretation game

Equations

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