def RSA.IBR.alternativeCount (G : InterpGame) (s : G.State) : ℕ

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

Equations

• RSA.IBR.alternativeCount G s = (G.trueMessages s).card

def RSA.IBR.isMinimalByAltCount (G : InterpGame) (m : G.Message) (s : G.State) : 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

• RSA.IBR.isMinimalByAltCount G m s = (G.meaning m s = true ∧ ∀ (s' : G.State), G.meaning m s' = true → RSA.IBR.alternativeCount G s ≤ RSA.IBR.alternativeCount G s')

theorem RSA.IBR.r1_subset_exhMW (G : InterpGame) (m : G.Message) (s : G.State) (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".

def RSA.IBR.altOrderingTotalOnMessage (G : InterpGame) (m : G.Message) : 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

• RSA.IBR.altOrderingTotalOnMessage G m = ∀ (s s' : G.State), G.meaning m s = true → G.meaning m s' = true → G.trueMessages s ⊆ G.trueMessages s' ∨ G.trueMessages s' ⊆ G.trueMessages s

theorem RSA.IBR.exhMW_subset_r1_under_totality (G : InterpGame) (m : G.Message) (s : G.State) (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 RSA.IBR.r1_eq_exhMW_under_totality (G : InterpGame) (m : G.Message) (s : G.State) (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.

This is the precise condition under which Franke's Fact 1 becomes an equality.

theorem RSA.IBR.fact3_exhMW_subset_exhIE (G : InterpGame) (m : G.Message) : 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 prop6_exhMW_entails_exhIE in Exhaustification/Operators.lean.

theorem RSA.IBR.fact4_exhMW_eq_exhIE_closed (G : InterpGame) (m : G.Message) (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 theorem9_main in Exhaustification/Operators.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 RSA.IBR.ScalarState : Type

States for scalar implicature example

• someNotAll : ScalarState
• all : ScalarState

instance RSA.IBR.instDecidableEqScalarState : DecidableEq ScalarState

Equations

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

instance RSA.IBR.instFintypeScalarState : Fintype ScalarState

Equations

• RSA.IBR.instFintypeScalarState = { elems := { val := ↑RSA.IBR.ScalarState.enumList, nodup := RSA.IBR.ScalarState.enumList_nodup }, complete := RSA.IBR.instFintypeScalarState._proof_1 }

instance RSA.IBR.instReprScalarState : Repr ScalarState

Equations

• RSA.IBR.instReprScalarState = { reprPrec := RSA.IBR.instReprScalarState.repr }

def RSA.IBR.instReprScalarState.repr : ScalarState → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• RSA.IBR.instReprScalarState.repr RSA.IBR.ScalarState.all prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "RSA.IBR.ScalarState.all")).group prec✝

instance RSA.IBR.instBEqScalarState : BEq ScalarState

Equations

• RSA.IBR.instBEqScalarState = { beq := RSA.IBR.instBEqScalarState.beq }

def RSA.IBR.instBEqScalarState.beq : ScalarState → ScalarState → Bool

Equations

• RSA.IBR.instBEqScalarState.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

inductive RSA.IBR.ScalarMessage : Type

Messages for scalar implicature example

• some_ : ScalarMessage
• all : ScalarMessage

instance RSA.IBR.instDecidableEqScalarMessage : DecidableEq ScalarMessage

Equations

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

instance RSA.IBR.instFintypeScalarMessage : Fintype ScalarMessage

Equations

• RSA.IBR.instFintypeScalarMessage = { elems := { val := ↑RSA.IBR.ScalarMessage.enumList, nodup := RSA.IBR.ScalarMessage.enumList_nodup }, complete := RSA.IBR.instFintypeScalarMessage._proof_1 }

instance RSA.IBR.instReprScalarMessage : Repr ScalarMessage

Equations

• RSA.IBR.instReprScalarMessage = { reprPrec := RSA.IBR.instReprScalarMessage.repr }

def RSA.IBR.instReprScalarMessage.repr : ScalarMessage → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• RSA.IBR.instReprScalarMessage.repr RSA.IBR.ScalarMessage.all prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "RSA.IBR.ScalarMessage.all")).group prec✝

def RSA.IBR.instBEqScalarMessage.beq : ScalarMessage → ScalarMessage → Bool

Equations

• RSA.IBR.instBEqScalarMessage.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance RSA.IBR.instBEqScalarMessage : BEq ScalarMessage

Equations

• RSA.IBR.instBEqScalarMessage = { beq := RSA.IBR.instBEqScalarMessage.beq }

def RSA.IBR.scalarGame : InterpGame

Scalar implicature interpretation game

Equations

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

theorem RSA.IBR.scalarGame_is_scalar : isScalarGame scalarGame

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

theorem RSA.IBR.scalarGame_distinct (m₁ m₂ : scalarGame.Message) : scalarGame.trueStates m₁ = scalarGame.trueStates m₂ → m₁ = m₂

The scalar implicature game has distinct truth sets.

theorem RSA.IBR.scalarGame_is_eqclass : isEquivalenceClassGame scalarGame

The scalar game is an equivalence class game: each message level is a singleton.

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 RSA.IBR.FCState : Type

States for free choice example

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

instance RSA.IBR.instDecidableEqFCState : DecidableEq FCState

Equations

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

instance RSA.IBR.instFintypeFCState : Fintype FCState

Equations

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

instance RSA.IBR.instReprFCState : Repr FCState

Equations

• RSA.IBR.instReprFCState = { reprPrec := RSA.IBR.instReprFCState.repr }

def RSA.IBR.instReprFCState.repr : FCState → ℕ → Std.Format

Equations

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

instance RSA.IBR.instBEqFCState : BEq FCState

Equations

• RSA.IBR.instBEqFCState = { beq := RSA.IBR.instBEqFCState.beq }

def RSA.IBR.instBEqFCState.beq : FCState → FCState → Bool

Equations

• RSA.IBR.instBEqFCState.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

inductive RSA.IBR.FCMessage : Type

Messages for free choice example

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

instance RSA.IBR.instDecidableEqFCMessage : DecidableEq FCMessage

Equations

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

instance RSA.IBR.instFintypeFCMessage : Fintype FCMessage

Equations

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

instance RSA.IBR.instReprFCMessage : Repr FCMessage

Equations

• RSA.IBR.instReprFCMessage = { reprPrec := RSA.IBR.instReprFCMessage.repr }

def RSA.IBR.instReprFCMessage.repr : FCMessage → ℕ → Std.Format

Equations

• RSA.IBR.instReprFCMessage.repr RSA.IBR.FCMessage.mayA prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "RSA.IBR.FCMessage.mayA")).group prec✝
• RSA.IBR.instReprFCMessage.repr RSA.IBR.FCMessage.mayB prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "RSA.IBR.FCMessage.mayB")).group prec✝
• RSA.IBR.instReprFCMessage.repr RSA.IBR.FCMessage.mayAorB prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "RSA.IBR.FCMessage.mayAorB")).group prec✝
• RSA.IBR.instReprFCMessage.repr RSA.IBR.FCMessage.mayAandB prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "RSA.IBR.FCMessage.mayAandB")).group prec✝

def RSA.IBR.instBEqFCMessage.beq : FCMessage → FCMessage → Bool

Equations

• RSA.IBR.instBEqFCMessage.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance RSA.IBR.instBEqFCMessage : BEq FCMessage

Equations

• RSA.IBR.instBEqFCMessage = { beq := RSA.IBR.instBEqFCMessage.beq }

def RSA.IBR.freeChoiceGame : InterpGame

Free choice interpretation game

Equations

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