structure RSA.IBR.InterpGame : Type 1

Interpretation game (Franke §6): states are equivalence classes over alternative truth patterns.

• State : Type

  Type of states (equivalence classes of worlds)

• Message : Type

  Type of messages (alternative utterances)

• meaning : self.Message → self.State → Bool

  Semantic meaning: is message m true at state s?

• prior : self.State → ℚ

  Prior probability over states

• stateFintype : Fintype self.State

  Fintype instances

• messageFintype : Fintype self.Message
• stateDecEq : DecidableEq self.State
• messageDecEq : DecidableEq self.Message

def RSA.IBR.InterpGame.trueStates (G : InterpGame) (m : G.Message) : Finset G.State

States where message m is true

Equations

• G.trueStates m = {s : G.State | G.meaning m s = true}

def RSA.IBR.InterpGame.trueMessages (G : InterpGame) (s : G.State) : Finset G.Message

Messages true at state s

Equations

• G.trueMessages s = {m : G.Message | G.meaning m s = true}

def RSA.IBR.InterpGame.informativity (G : InterpGame) (m : G.Message) : ℚ

Informativity of a message (reciprocal of true states, as ratio)

Equations

• G.informativity m = if (G.trueStates m).card = 0 then 0 else 1 / ↑(G.trueStates m).card

structure RSA.IBR.HearerStrategy (G : InterpGame) : Type

A hearer strategy: P(state | message)

• respond : G.Message → G.State → ℚ

structure RSA.IBR.SpeakerStrategy (G : InterpGame) : Type

A speaker strategy: P(message | state)

• choose : G.State → G.Message → ℚ

def RSA.IBR.HearerStrategy.literal (G : InterpGame) : HearerStrategy G

Uniform distribution over states where m is true

Equations

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

def RSA.IBR.HearerStrategy.support {G : InterpGame} (H : HearerStrategy G) (m : G.Message) : Finset G.State

Support of hearer's response to message m

Equations

• H.support m = {s : G.State | H.respond m s > 0}

def RSA.IBR.SpeakerStrategy.support {G : InterpGame} (S : SpeakerStrategy G) (s : G.State) : Finset G.Message

Support of speaker's choice at state s

Equations

• S.support s = {m : G.Message | S.choose s m > 0}

def RSA.IBR.SpeakerStrategy.bestResponse (G : InterpGame) (H : HearerStrategy G) : SpeakerStrategy G

Best response speaker: choose messages that maximize hearer success

Equations

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

theorem RSA.IBR.SpeakerStrategy.bestResponse_nonneg (G : InterpGame) (H : HearerStrategy G) (s : G.State) (m : G.Message) : 0 ≤ (bestResponse G H).choose s m

Best response speaker always gives non-negative probabilities.

theorem RSA.IBR.SpeakerStrategy.bestResponse_false_zero (G : InterpGame) (H : HearerStrategy G) (s : G.State) (m : G.Message) (hFalse : G.meaning m s = false) : (bestResponse G H).choose s m = 0

Best response speaker gives zero probability to false messages.

theorem RSA.IBR.SpeakerStrategy.bestResponse_sum_le_one (G : InterpGame) (H : HearerStrategy G) (s : G.State) : ∑ m : G.Message, (bestResponse G H).choose s m ≤ 1

Best response speaker probabilities sum to at most 1 at any state.

For states with at least one true message, this is exactly 1 (uniform over optimal). For states with no true messages, this is 0.

def RSA.IBR.L0 (G : InterpGame) : HearerStrategy G

L₀: Literal listener (Franke Def. 22)

Equations

• RSA.IBR.L0 G = RSA.IBR.HearerStrategy.literal G

def RSA.IBR.hearerUpdate (G : InterpGame) (S : SpeakerStrategy G) : HearerStrategy G

Hearer update: Given speaker strategy, compute posterior.

L_{n+1}(s | m) ∝ S_n(m | s) · P(s)

This is Bayes' rule with the speaker strategy as likelihood.

Equations

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

def RSA.IBR.speakerUpdate (G : InterpGame) (H : HearerStrategy G) : SpeakerStrategy G

Speaker update: Best response to hearer strategy.

S_{n+1}(m | s) = argmax_m L_n(s | m)

Uniform over optimal messages.

Equations

• RSA.IBR.speakerUpdate G H = RSA.IBR.SpeakerStrategy.bestResponse G H

def RSA.IBR.ibrStep (G : InterpGame) (H : HearerStrategy G) : HearerStrategy G

One full IBR iteration step

Equations

• RSA.IBR.ibrStep G H = RSA.IBR.hearerUpdate G (RSA.IBR.speakerUpdate G H)

def RSA.IBR.ibrN (G : InterpGame) (n : ℕ) : HearerStrategy G

IBR reasoning for n iterations starting from L₀

Equations

• RSA.IBR.ibrN G 0 = RSA.IBR.L0 G
• RSA.IBR.ibrN G n_2.succ = RSA.IBR.ibrStep G (RSA.IBR.ibrN G n_2)

def RSA.IBR.S1 (G : InterpGame) : SpeakerStrategy G

S₁: First pragmatic speaker

Equations

• RSA.IBR.S1 G = RSA.IBR.speakerUpdate G (RSA.IBR.L0 G)

def RSA.IBR.L2 (G : InterpGame) : HearerStrategy G

L₂: First pragmatic listener

Equations

• RSA.IBR.L2 G = RSA.IBR.hearerUpdate G (RSA.IBR.S1 G)

def RSA.IBR.isIBRFixedPoint (G : InterpGame) (H : HearerStrategy G) : Prop

Check if hearer strategy is a fixed point of IBR

Equations

• RSA.IBR.isIBRFixedPoint G H = ∀ (m : G.Message) (s : G.State), H.respond m s = (RSA.IBR.ibrStep G H).respond m s

theorem RSA.IBR.fp_respond_nonneg (G : InterpGame) (H : HearerStrategy G) (hFP : isIBRFixedPoint G H) (hPriorNonneg : ∀ (s : G.State), G.prior s ≥ 0) (m : G.Message) (s : G.State) : H.respond m s ≥ 0

At a fixed point with non-negative priors, H.respond is non-negative.

This follows from the fact that H = ibrStep G H, and ibrStep uses hearerUpdate which gives non-negative values when priors are non-negative.

def RSA.IBR.pragmaticSupport (G : InterpGame) (H : HearerStrategy G) (m : G.Message) : Finset G.State

The pragmatic interpretation: support of the IBR fixed point listener

Equations

• RSA.IBR.pragmaticSupport G H m = H.support m

noncomputable def RSA.IBR.expectedGain (G : InterpGame) (S : SpeakerStrategy G) (H : HearerStrategy G) : ℚ

EG(S, R) = Σ_t Pr(t) × Σ_m S(t,m) × R(m,t): expected communication success.

Equations

• RSA.IBR.expectedGain G S H = ∑ t : G.State, G.prior t * ∑ m : G.Message, S.choose t m * H.respond m t

theorem RSA.IBR.eg_speaker_improvement (G : InterpGame) (S_old S_new : SpeakerStrategy G) (H : HearerStrategy G) (hBR : S_new = SpeakerStrategy.bestResponse G H) : expectedGain G S_old H ≤ expectedGain G S_new H

Lemma 3a: best-response speaker improves EG.

theorem RSA.IBR.eg_hearer_improvement (G : InterpGame) (S : SpeakerStrategy G) (H_old H_new : HearerStrategy G) (hBR : H_new = hearerUpdate G S) : expectedGain G S H_old ≤ expectedGain G S H_new

Lemma 3b: Bayesian hearer update improves EG.

theorem RSA.IBR.eg_bounded (G : InterpGame) (S : SpeakerStrategy G) (H : HearerStrategy G) (hPriorSum : Finset.univ.sum G.prior = 1) (hPriorNonneg : ∀ (s : G.State), G.prior s ≥ 0) : expectedGain G S H ≤ 1

Expected gain is bounded above by 1 (probability of perfect communication).

theorem RSA.IBR.ibr_reaches_fixed_point (G : InterpGame) : ∃ (n : ℕ), isIBRFixedPoint G (ibrN G n)

Theorem 3: IBR converges. EG is monotone increasing and bounded ⟹ fixed point.

def RSA.IBR.speakerOptionCount (G : InterpGame) (S : SpeakerStrategy G) (t : G.State) : ℕ

Number of messages the speaker uses at state t (|S(t)|).

Equations

• RSA.IBR.speakerOptionCount G S t = {m : G.Message | S.choose t m > 0}.card

theorem RSA.IBR.fp_prefers_fewer_options (G : InterpGame) (H : HearerStrategy G) (hFP : isIBRFixedPoint G H) (hFlatPrior : ∀ (t₁ t₂ : G.State), G.prior t₁ = G.prior t₂) (hPriorPos : ∀ (t : G.State), G.prior t > 0) (m : G.Message) (t₁ t₂ : G.State) (ht₁ : G.meaning m t₁ = true) (ht₂ : G.meaning m t₂ = true) : have S := speakerUpdate G H; H.respond m t₁ > H.respond m t₂ ↔ speakerOptionCount G S t₁ < speakerOptionCount G S t₂

At the fixed point with flat priors, fewer speaker options ↔ higher hearer probability (eq. 131).

theorem RSA.IBR.speaker_options_le_true_messages (G : InterpGame) (H : HearerStrategy G) (t : G.State) : have S := speakerUpdate G H; speakerOptionCount G S t ≤ (G.trueMessages t).card

Best-response speaker uses ⊆ true messages, so speakerOptionCount ≤ |trueMessages|.

IBR = EXH (Franke Main Result)

@cite{franke-2011} @cite{spector-2016}

The key insight of @cite{franke-2011} is that IBR reasoning yields exactly the same interpretation as exhaustive interpretation (exhMW).

Theorem (@cite{franke-2011}, Section 9.3): For an interpretation game G, the IBR fixed point listener's support for message m equals the set of minimal m-worlds relative to the alternative ordering.

In notation: support(L∞(· | m)) = exhMW(ALT, m)

This connects game-theoretic pragmatics to grammatical exhaustification.

Results from Section 10 and Appendix A

Equation (107): R₁ characterization R₁(m) = {t ∈ ⟦m⟧ | ¬∃t′ ∈ ⟦m⟧ : |R⁻¹₀(t′)| < |R⁻¹₀(t)|}

This selects states where fewest alternatives are true.

Fact 1 (Section 10): R₁(mₛ) ⊆ ExhMM(S) Under "homogeneity" of alternatives, R₁(mₛ) = ExhMM(S).

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

Fact 4 (Appendix A): ExhMM = ExhIE when Alt satisfies closure conditions.

def RSA.IBR.toAlternatives (G : InterpGame) : Set (Prop' G.State)

Convert interpretation game to alternative set for exhaustification. Converts Bool meaning to Prop' by using equality with true.

Equations

• RSA.IBR.toAlternatives G = {x : Prop' G.State | ∃ (m : G.Message), (fun (s : G.State) => G.meaning m s = true) = x}

def RSA.IBR.prejacent (G : InterpGame) (m : G.Message) : Prop' G.State

The prejacent proposition for a message (Bool → Prop conversion)

Equations

• RSA.IBR.prejacent G m s = (G.meaning m s = true)

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')

noncomputable def RSA.IBR.minAltCountStates (G : InterpGame) (m : G.Message) : Finset G.State

States with minimum alternative count among m-worlds.

Equations

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

theorem RSA.IBR.ltALT_implies_trueMessages_ssubset (G : InterpGame) (s' s : G.State) (hlt : s' <[toAlternatives G] s) : G.trueMessages s' ⊂ G.trueMessages s

Key lemma: s' <_ALT s implies trueMessages s' ⊂ trueMessages s.

This is the bridge between the <_ALT ordering and alternative counting.

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

theorem RSA.IBR.trueMessages_injective_of_homogeneous (G : InterpGame) (hGame : ∀ (s₁ s₂ : G.State), (∀ (m' : G.Message), G.meaning m' s₁ = G.meaning m' s₂) → s₁ = s₂) (s' s : G.State) (heq : G.trueMessages s' = G.trueMessages s) : s' = s

Under homogeneity, trueMessages determines states uniquely. This means: trueMessages s' = trueMessages s → s' = s

theorem RSA.IBR.trueMessages_ssubset_implies_ltALT (G : InterpGame) (_hGame : ∀ (s₁ s₂ : G.State), (∀ (m' : G.Message), G.meaning m' s₁ = G.meaning m' s₂) → s₁ = s₂) (s' s : G.State) (hss : G.trueMessages s' ⊂ G.trueMessages s) : s' <[toAlternatives G] s

Under homogeneity, strict subset of trueMessages implies <_ALT. Note: hGame is not actually used in this proof, but kept for consistency.

theorem RSA.IBR.r1_containedIn_exhMW (G : InterpGame) (m : G.Message) (s : G.State) (h : isMinimalByAltCount G m s) : NeoGricean.Exhaustivity.exhMW (toAlternatives G) (prejacent G m) s

Franke Fact 1: R₁ ⊆ ExhMW (containment, not equality).

This is the main soundness result: if s is selected by IBR level-1 reasoning (has minimum alternative count among m-worlds), then s is in ExhMW.

Why not equality? Franke notes (Section 10): "The reverse, however, is not necessarily the case: it may well be that two worlds w, v ∈ S are both minimal with respect to <_ALT, while w makes more alternatives true than v."

In other words:

• R₁ selects states with minimum |{A : A(s)}| among m-worlds
• ExhMW selects states minimal in <_ALT (subset ordering on alternatives)
• Minimum cardinality ⟹ minimal in subset ordering ✓
• Minimal in subset ordering ⟹ minimum cardinality ✗

For equality, we'd need <_ALT to be total on m-worlds (a "chain" structure). This is a stronger condition that doesn't always hold.

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.

This "chain condition" ensures that minimal cardinality ⟺ minimal in <_ALT.

When does this hold?

• When alternatives form a linear scale (e.g., ⟨some, most, all⟩)
• When alternatives are conjunctive closures of simpler alternatives
• When states are defined as equivalence classes by alternative patterns

When does this fail?

• When alternatives can be true independently (e.g., "red" and "tall")
• When the alternative space has incomparable elements

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 : NeoGricean.Exhaustivity.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 ↔ NeoGricean.Exhaustivity.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) : NeoGricean.Exhaustivity.exhMW (toAlternatives G) (prejacent G m) ⊆ₚ NeoGricean.Exhaustivity.exhIE (toAlternatives G) (prejacent G m)

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

This is the easier direction: minimal-models is always at least as strong as innocent exclusion.

Proof (from Franke Appendix A): If w ∈ ExhMM(S, Alt), then w is minimal w.r.t. <Alt in S. This means w makes a maximal set of alternatives false. So there exists A ∈ Max-CE(S, Alt) with w ∈ S ∧ ⋀{a∈A}¬a. Since IE = ⋂ Max-CE, w satisfies all propositions in IE. Hence w ∈ ExhIE(S, Alt).

This is already proved as prop6_exhMW_entails_exhIE in Exhaustivity/Basic.lean.

theorem RSA.IBR.fact4_exhMW_eq_exhIE_closed (G : InterpGame) (m : G.Message) (hClosed : NeoGricean.Exhaustivity.closedUnderConj (toAlternatives G)) : NeoGricean.Exhaustivity.exhMW (toAlternatives G) (prejacent G m) ≡ₚ NeoGricean.Exhaustivity.exhIE (toAlternatives G) (prejacent G m)

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

This is Spector's Theorem 9, referenced by Franke in Appendix A.

Condition: For all w, w' ∈ ExhMM(S, Alt), there exists A ∈ Alt such that A(w) ∧ A(w') entails A.

When Alt is closed under conjunction, this condition holds automatically because we can take A = A(w) ∧ A(w').

This is proved as theorem9_main in Exhaustivity/Basic.lean.

theorem RSA.IBR.ibr_equals_exhMW (G : InterpGame) (H : HearerStrategy G) (hFP : isIBRFixedPoint G H) (m : G.Message) (s : G.State) : H.respond m s > 0 ↔ NeoGricean.Exhaustivity.exhMW (toAlternatives G) (prejacent G m) s

IBR fixed point equals exhMW (Main theorem - @cite{franke-2011}, Section 9.3)

This is the central result connecting game theory to exhaustification. At the fixed point, the IBR listener's interpretation of message m is exactly the exhaustive interpretation exhMW(ALT, m).

Proof Strategy:

1. Non-minimal states eliminated: If s is non-minimal (∃s' < s with m(s')), then at s', there's a message m' true at s' but not at s (by definition of <). Message m' is more informative than m. So S_n prefers m' at s', leading to S_n(m|s') < 1. This propagates: L_{n+1}(s|m) decreases each iteration.

2. Minimal states preserved: If s is minimal among m-worlds, then at s, no "stronger" alternative is true, so m is optimal. S_n(m|s) = 1/|optimal|, and L_{n+1}(s|m) > 0 is maintained.

3. Convergence: By well-foundedness of < on finite sets, this stabilizes. The fixed point support equals the set of minimal m-worlds = exhMW.

Key Lemma: For any s in support(L_∞(·|m)):

• m(s) must be true (literal content)
• No s' < s can have m(s') true (minimality) This is exactly exhMW(ALT, m).

theorem RSA.IBR.ibr_fp_excludes_nonminimal (G : InterpGame) (H : HearerStrategy G) (hFP : isIBRFixedPoint G H) (hPriorNonneg : ∀ (s : G.State), G.prior s ≥ 0) (m : G.Message) (s : G.State) (_hs : G.meaning m s = true) (hNonMin : ∃ (s' : G.State), G.meaning m s' = true ∧ s' <[toAlternatives G] s) : H.respond m s = 0

At the fixed point, IBR excludes non-minimal states.

Note: This is stated for the FIXED POINT listener, not L2 specifically. L2 alone doesn't necessarily exclude all non-minimal states; the full elimination happens through iteration to the fixed point.

theorem RSA.IBR.ibr_fp_keeps_minimal (G : InterpGame) (H : HearerStrategy G) (hFP : isIBRFixedPoint G H) (m : G.Message) (s : G.State) (hs : G.meaning m s = true) (hMin : ¬∃ (s' : G.State), G.meaning m s' = true ∧ s' <[toAlternatives G] s) (_hPriorPos : G.prior s > 0) : H.respond m s > 0

At the fixed point, IBR keeps minimal states.

If s is minimal among m-worlds (no s' < s with m(s')), then the fixed point listener assigns positive probability to s given m.

RSA → IBR as α → ∞

RSA uses softmax instead of argmax:

• RSA S₁(m | s) ∝ exp(α · log L₀(s | m)) -- softmax
• IBR S₁(m | s) = argmax_m L₀(s | m) -- hard argmax

As the rationality parameter α → ∞, softmax becomes argmax. This connects the probabilistic RSA model to the deterministic IBR model.

noncomputable def RSA.IBR.falseMessageScore (G : InterpGame) : ℝ

Floor score for false messages. Uses -log(|State|) - 1, which is always below the minimum possible log-informativity for any true message.

Equations

• RSA.IBR.falseMessageScore G = -Real.log ↑(Fintype.card G.State) - 1

noncomputable def RSA.IBR.rsaS1Real (G : InterpGame) (α : ℝ) (s : G.State) : G.Message → ℝ

RSA S1 probability (real version for limit theorems).

RSA S1 is exactly softmax over log-informativity scores: rsaS1(m | s) = exp(α · log(inf(m))) / Σ exp(α · log(inf(m'))) = inf(m)^α / Σ inf(m')^α = softmax(log ∘ inf, α)(m)

Equations

• RSA.IBR.rsaS1Real G α s = Core.softmax (fun (m : G.Message) => if G.meaning m s = true then Real.log ↑(G.informativity m) else RSA.IBR.falseMessageScore G) α

theorem RSA.IBR.rsaS1_eq_softmax (G : InterpGame) [Nonempty G.Message] (α : ℝ) (s : G.State) : rsaS1Real G α s = Core.softmax (fun (m : G.Message) => if G.meaning m s = true then Real.log ↑(G.informativity m) else falseMessageScore G) α

RSA S1 equals softmax over log-informativity.

This is the key observation: RSA speaker choice is softmax with scores = log(informativity of message).

theorem RSA.IBR.rsa_to_ibr_limit (G : InterpGame) [Nonempty G.Message] (s : G.State) (m : G.Message) (hTrue : G.meaning m s = true) (hUnique : ∀ (m' : G.Message), m' ≠ m → G.meaning m' s = true → G.informativity m > G.informativity m') (hInfPos : 0 < G.informativity m) : Filter.Tendsto (fun (α : ℝ) => rsaS1Real G α s m) Filter.atTop (nhds 1)

As α → ∞, RSA S1 concentrates on optimal messages (IBR S1).

This follows directly from softmax_tendsto_hardmax:

• RSA S1 = softmax(log-informativity, α)
• As α → ∞, softmax → argmax
• argmax(log-informativity) = argmax(informativity) = IBR S1

The proof uses tendsto_softmax_infty_at_max from Limits.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 }

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.instReprScalarState : Repr ScalarState

Equations

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

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

Equations

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

instance RSA.IBR.instBEqScalarState : BEq ScalarState

Equations

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

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 }

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✝

instance RSA.IBR.instReprScalarMessage : Repr ScalarMessage

Equations

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

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.

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✝

instance RSA.IBR.instBEqFCMessage : BEq FCMessage

Equations

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

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

Equations

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

def RSA.IBR.freeChoiceGame : InterpGame

Free choice interpretation game

Equations

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

The Complete Chain

This section states the full limit theorem connecting RSA to EXH, combining:

• @cite{franke-2011}: RSA → IBR as α → ∞; IBR ≈ ExhMW (Appendix A)
• @cite{spector-2007}: Iterated exhaustification
• @cite{spector-2016}: Theorem 9 (ExhMW = ExhIE under closure)

The Chain

RSA S1 (softmax)
    │ α → ∞ [rsa_to_ibr_limit - PROVED]
    ↓
IBR S1 (argmax) = R₁
    │ Fact 1 [r1_subset_exhMW] (@cite{franke-2011} Appendix A)
    ↓
ExhMW (minimal worlds)
    │ Theorem 9 [fact4_exhMW_eq_exhIE_closed]
    ↓
ExhIE (innocent exclusion)

Results

1. rsa_to_ibr_limit (proved above): RSA S1 → IBR S1 as α → ∞
2. Fact 1 (r1_subset_exhMW): IBR R₁ ⊆ ExhMW (@cite{franke-2011} Appendix A)
3. Fact 3 (fact3_exhMW_subset_exhIE): ExhMW ⊆ ExhIE (@cite{franke-2011} Appendix A)
4. Theorem 9 (fact4_exhMW_eq_exhIE_closed): Under closure, ExhMW = ExhIE

Combined: Under closure, lim_{α→∞} RSA = IBR = ExhMW = ExhIE

Temperature Interpretation

• Temperature 1/α = 0 (α = ∞): deterministic selection (EXH/IBR)
• Temperature 1/α > 0 (α finite): probabilistic selection (RSA)

RSA and EXH are the same rational principle at different "temperatures"

theorem RSA.IBR.ibr_fp_equals_exhMW (G : InterpGame) (H : HearerStrategy G) (hFP : isIBRFixedPoint G H) (m : G.Message) (_hGame : ∀ (s₁ s₂ : G.State), (∀ (m' : G.Message), G.meaning m' s₁ = G.meaning m' s₂) → s₁ = s₂) (s : G.State) : H.respond m s > 0 ↔ NeoGricean.Exhaustivity.exhMW (toAlternatives G) (prejacent G m) s

IBR fixed point equals exhMW (Main theorem - @cite{franke-2011}, Section 9.3)

This combines:

• Equation (107): R₁ selects states with minimum alternative count
• Fact 1: Such states are exactly the minimal worlds

At the fixed point, the IBR listener's interpretation of message m is exactly the exhaustive interpretation exhMW(ALT, m).

theorem RSA.IBR.exhMW_eq_exhIE_under_closure (G : InterpGame) (m : G.Message) (hClosed : NeoGricean.Exhaustivity.closedUnderConj (toAlternatives G)) (s : G.State) : NeoGricean.Exhaustivity.exhMW (toAlternatives G) (prejacent G m) s ↔ NeoGricean.Exhaustivity.exhIE (toAlternatives G) (prejacent G m) s

When alternatives are closed under conjunction, ExhMW = ExhIE.

This is Spector's Theorem 9, already proved in Exhaustivity/Basic.lean. We re-export it here for the chain.

theorem RSA.IBR.ibr_fp_equals_exhIE (G : InterpGame) (H : HearerStrategy G) (hFP : isIBRFixedPoint G H) (m : G.Message) (hGame : ∀ (s₁ s₂ : G.State), (∀ (m' : G.Message), G.meaning m' s₁ = G.meaning m' s₂) → s₁ = s₂) (hClosed : NeoGricean.Exhaustivity.closedUnderConj (toAlternatives G)) (s : G.State) : H.respond m s > 0 ↔ NeoGricean.Exhaustivity.exhIE (toAlternatives G) (prejacent G m) s

When alternatives are closed under conjunction, IBR = exhIE.

This combines:

• ibr_fp_equals_exhMW: IBR fixed point = exhMW
• fact4_exhMW_eq_exhIE_closed: Under closure, exhMW = exhIE

Combined: Under closure, IBR = exhMW = exhIE

theorem RSA.IBR.rsa_to_exhMW_limit (G : InterpGame) [Nonempty G.Message] (m : G.Message) (s : G.State) (hTrue : G.meaning m s = true) (hMin : isMinimalByAltCount G m s) (hUnique : ∀ (m' : G.Message), m' ≠ m → G.meaning m' s = true → G.informativity m > G.informativity m') (hInfPos : 0 < G.informativity m) : Filter.Tendsto (fun (α : ℝ) => rsaS1Real G α s m) Filter.atTop (nhds 1)

The grand unification: RSA → ExhMW as α → ∞.

This combines:

• rsa_to_ibr_limit: RSA S1 → IBR S1 as α → ∞
• IBR fixed point = exhMW

Therefore: lim_{α→∞} support(RSA.L1(α, m)) = exhMW(ALT, m)

theorem RSA.IBR.rsa_to_exhIE_limit (G : InterpGame) [Nonempty G.Message] (m : G.Message) (s : G.State) (hTrue : G.meaning m s = true) (hMin : NeoGricean.Exhaustivity.exhIE (toAlternatives G) (prejacent G m) s) (hClosed : NeoGricean.Exhaustivity.closedUnderConj (toAlternatives G)) (hUnique : ∀ (m' : G.Message), m' ≠ m → G.meaning m' s = true → G.informativity m > G.informativity m') (hInfPos : 0 < G.informativity m) : Filter.Tendsto (fun (α : ℝ) => rsaS1Real G α s m) Filter.atTop (nhds 1)

The full limit theorem: RSA → ExhIE under closure as α → ∞.

This combines results from:

• @cite{franke-2011}: RSA → IBR (softmax → argmax), IBR = exhMW (Appendix A)
• @cite{spector-2007}: Iterated exhaustification
• @cite{spector-2016}: Theorem 9 (exhMW = exhIE under closure)

The chain:

1. RSA S1 → IBR S1 as α → ∞ (softmax → argmax)
2. IBR = exhMW (@cite{franke-2011} Appendix A, Fact 1)
3. exhMW = exhIE under closure (@cite{spector-2016} Theorem 9)

Therefore: Under closure, lim_{α→∞} RSA = exhIE

Epistemic Readings (Franke Section 3.2)

Franke distinguishes three epistemic readings of scalar implicatures:

1. Simple SI: "Some but not all" (most common)
2. Weak epistemic: "The speaker doesn't know that all"
3. Strong epistemic: "The speaker knows that not all"

These arise from different assumptions about speaker competence:

• Full competence → Simple SI
• No competence assumed → Weak epistemic
• Intermediate → Strong epistemic

IBR naturally handles these by adjusting the state space.

inductive RSA.IBR.CompetenceLevel : Type

Speaker competence level (Franke Section 3.2)

• full : CompetenceLevel
• uncertain : CompetenceLevel
• none : CompetenceLevel

instance RSA.IBR.instDecidableEqCompetenceLevel : DecidableEq CompetenceLevel

Equations

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

instance RSA.IBR.instReprCompetenceLevel : Repr CompetenceLevel

Equations

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

def RSA.IBR.instReprCompetenceLevel.repr : CompetenceLevel → ℕ → Std.Format

Equations

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

structure RSA.IBR.EpistemicState (S : Type) : Type

Epistemic state: combines world state with speaker knowledge. Used for epistemic readings of scalar implicatures.

• actualWorld : S
• speakerKnowledge : Set S

def RSA.IBR.toEpistemicGame (G : InterpGame) (comp : CompetenceLevel) : InterpGame

Build epistemic interpretation game from base game

Equations

• RSA.IBR.toEpistemicGame G RSA.IBR.CompetenceLevel.full = G
• RSA.IBR.toEpistemicGame G comp = G