Jäger 2014: Rationalizable Signaling

[Jag14]'s iterated cautious response (ICR) model of game-theoretic pragmatics — the journal-mature version of [JE09]'s pragmatic rationalizability. A semantic game equips a signaling game with contexts (higher-order uncertainty about preferences), an exogenous interpretation function, and cost-separable sender utilities. Rational interlocutors iterate cautious responses (best responses to some full-support belief, following Pearce's rationalizability program) starting from the credulous receiver; the pragmatically rationalizable strategies are those recurring arbitrarily late in the iteration.

Main formalized results:

• SemanticGame, optimalActions (Def. 1, via Finset.argmax), senderBR/receiverBR (Def. 2), senderCR/receiverCR (Def. 3), the ICR sequence icrR/icrS (Def. 4), prsS/prsR (Def. 5), IsRationalizable (Def. 6).

• prs_rationalizable (the paper's Theorem 1): pragmatically rationalizable strategy pairs are rationalizable in the classical sense. The proof follows the paper — the ICR sequence is deterministic on a finite space, hence eventually periodic; beyond the periodic threshold every ICR stage lies inside the recurrence sets, so the recurrence sets themselves witness rationalizability.

• Best-response characterizations: mem_senderBR_iff and mem_receiverBR_iff reduce the function-space argmaxes of Def. 2 to pointwise argmaxes (per context/world for the sender; per context/signal against posterior-weighted masses for the receiver), via Finset.mem_argmax_comp_surjective and Finset.mem_argmax_pi_sum.

• prsS_eq_of_fixed/prsR_eq_of_fixed: at a fixed point of the ICR step the recurrence sets collapse to the fixed stage.

• Credible — Rabin-style message credibility (§4): a signal is credible iff all pragmatically rationalizable senders use it literally.

• division_of_pragmatic_labor (§5, Example 6): in the two-synonyms game with a costly marked form and a 3:1 prior, the pragmatically rationalizable strategies are exactly the Horn convention — the cheap form marks the frequent world and the costly form the rare one (both PRS sets are the identity strategies) — and both signals are credible.

The comparison with [Fra11]'s IBR model (the paper's §6: Franke's games are the type-matching specialization, and the models differ exactly in belief selection — uniform via the Principle of Insufficient Reason vs. all full-support beliefs) is a planned follow-up, along with the remaining §5 examples.

Beliefs

Probability distributions and full-support ("cautious") distributions, including versions supported on a given strategy set — Jäger's Δ(M) and int(Δ(M)).

def Jaeger2014.IsFullDist {M : Type u_1} [Fintype M] (q : M → ℝ) : Prop

Jäger's Δ(M) is mathlib's standard simplex, stdSimplex ℝ M; the full-support and support-restricted variants below have no mathlib counterpart and are stated relative to it. A full-support probability distribution: Jäger's int(Δ(M)).

Equations

• Jaeger2014.IsFullDist q = ((∀ (x : M), 0 < q x) ∧ ∑ x : M, q x = 1)

def Jaeger2014.IsDistOn {M : Type u_1} [Fintype M] (P : Set M) (q : M → ℝ) : Prop

A distribution supported inside P: Jäger's Δ(P) for P ⊆ M.

Equations

• Jaeger2014.IsDistOn P q = (q ∈ stdSimplex ℝ M ∧ ∀ x ∉ P, q x = 0)

def Jaeger2014.IsFullDistOn {M : Type u_1} [Fintype M] (P : Set M) (q : M → ℝ) : Prop

A distribution with support exactly P: Jäger's int(Δ(P))) for P ⊆ M — positive on P, zero off it.

Equations

• Jaeger2014.IsFullDistOn P q = ((∀ x ∈ P, 0 < q x) ∧ (∀ x ∉ P, q x = 0) ∧ ∑ x : M, q x = 1)

theorem Jaeger2014.IsFullDist.mem_stdSimplex {M : Type u_1} [Fintype M] {q : M → ℝ} (h : IsFullDist q) : q ∈ stdSimplex ℝ M

theorem Jaeger2014.IsFullDistOn.isDistOn {M : Type u_1} [Fintype M] {P P' : Set M} {q : M → ℝ} (h : IsFullDistOn P q) (hPP' : P ⊆ P') : IsDistOn P' q

A full-support-on-P distribution is supported inside any superset.

Semantic games

structure Jaeger2014.SemanticGame (C : Type u_2) (W : Type u_3) (F : Type u_4) (A : Type u_5) [Fintype W] : Type (max (max (max u_2 u_3) u_4) u_5)

A semantic game ([Jag14] §4): contexts C (higher-order uncertainty about preferences), worlds W, signals F, actions A; a positive prior over worlds; an exogenous interpretation function (meaning); receiver utilities, and cost-separable sender utilities (uS c w f a = vS c w a - cost f).

• prior : W → ℝ

  The receiver's prior probability over worlds (p*).

• prior_pos (w : W) : 0 < self.prior w

  All worlds have positive prior probability.

• prior_sum : ∑ w : W, self.prior w = 1

  The prior is a probability distribution.

• meaning : F → W → Prop

  The interpretation function ⟦·⟧: is signal f true at world w?

• vS : C → W → A → ℝ

  Context/outcome utilities of the sender.

• cost : F → ℝ

  Signalling costs.

• uR : C → W → A → ℝ

  The receiver's utility function.

• meaningDecidable (f : F) : DecidablePred (self.meaning f)

def Jaeger2014.SemanticGame.uS {C : Type u_2} {W : Type u_3} {F : Type u_4} {A : Type u_5} [Fintype W] (g : SemanticGame C W F A) (c : C) (w : W) (f : F) (a : A) : ℝ

The sender's utility function: outcome utility minus signalling cost.

Equations

• g.uS c w f a = g.vS c w a - g.cost f

def Jaeger2014.SemanticGame.extension {C : Type u_2} {W : Type u_3} {F : Type u_4} {A : Type u_5} [Fintype W] (g : SemanticGame C W F A) (f : F) : Finset W

The extension of a signal: the worlds at which it is true.

Equations

• g.extension f = Finset.filter (g.meaning f) Finset.univ

noncomputable def Jaeger2014.SemanticGame.optimalActions {C : Type u_2} {W : Type u_3} {F : Type u_4} {A : Type u_5} [Fintype W] [Fintype A] (g : SemanticGame C W F A) (c : C) (φ : Finset W) (p : W → ℝ) : Finset A

Def. 1: the receiver-optimal actions in context c when the belief p is updated with the proposition φ — the argmax of p-expected receiver utility over φ.

Equations

• g.optimalActions c φ p = Finset.univ.argmax fun (a : A) => ∑ w ∈ φ, p w * g.uR c w a

Best responses and cautious responses

Pure sender strategies are C → W → F, pure receiver strategies C → F → A. A receiver belief is a distribution over sender strategies plus a distribution over (sender) contexts; symmetrically for the sender. Cautious responses (Def. 3, after Pearce) are best responses to some full-support belief.

def Jaeger2014.SemanticGame.receiverBR {C : Type u_2} {W : Type u_3} {F : Type u_4} {A : Type u_5} [Fintype C] [Fintype W] [Fintype F] [Fintype A] [DecidableEq C] [DecidableEq W] [DecidableEq F] (g : SemanticGame C W F A) (σ : (C → W → F) → ℝ) (q : C → ℝ) : Set (C → F → A)

Def. 2 (receiver): r' is a best response to the belief (σ, q) iff in every own-context c it maximizes expected utility against the sender strategy distribution σ, context distribution q, and the prior.

Equations

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

def Jaeger2014.SemanticGame.senderBR {C : Type u_2} {W : Type u_3} {F : Type u_4} {A : Type u_5} [Fintype C] [Fintype W] [Fintype F] [Fintype A] [DecidableEq C] [DecidableEq W] [DecidableEq F] (g : SemanticGame C W F A) (ρ : (C → F → A) → ℝ) (q : C → ℝ) : Set (C → W → F)

Def. 2 (sender): s' is a best response to the belief (ρ, q) iff at every context/world pair it maximizes expected utility against the receiver strategy distribution ρ and context distribution q.

Equations

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

def Jaeger2014.SemanticGame.senderCR {C : Type u_2} {W : Type u_3} {F : Type u_4} {A : Type u_5} [Fintype C] [Fintype W] [Fintype F] [Fintype A] [DecidableEq C] [DecidableEq W] [DecidableEq F] (g : SemanticGame C W F A) (R : Set (C → F → A)) : Set (C → W → F)

Def. 3: cautious responses of the sender to a set R of receiver strategies — best responses to some belief with support exactly R and full-support context beliefs.

Equations

• g.senderCR R = {s : C → W → F | ∃ (ρ : (C → F → A) → ℝ) (q : C → ℝ), Jaeger2014.IsFullDistOn R ρ ∧ Jaeger2014.IsFullDist q ∧ s ∈ g.senderBR ρ q}

def Jaeger2014.SemanticGame.receiverCR {C : Type u_2} {W : Type u_3} {F : Type u_4} {A : Type u_5} [Fintype C] [Fintype W] [Fintype F] [Fintype A] [DecidableEq C] [DecidableEq W] [DecidableEq F] (g : SemanticGame C W F A) (S : Set (C → W → F)) : Set (C → F → A)

Def. 3: cautious responses of the receiver to a set S of sender strategies.

Equations

• g.receiverCR S = {r : C → F → A | ∃ (σ : (C → W → F) → ℝ) (q : C → ℝ), Jaeger2014.IsFullDistOn S σ ∧ Jaeger2014.IsFullDist q ∧ r ∈ g.receiverBR σ q}

The iterated cautious response sequence

def Jaeger2014.SemanticGame.Unexpected {C : Type u_2} {W : Type u_3} {F : Type u_4} (S : Set (C → W → F)) (f : F) : Prop

A signal is unexpected for a set S of sender strategies if no strategy in S ever uses it.

Equations

• Jaeger2014.SemanticGame.Unexpected S f = ∀ s ∈ S, ∀ (c : C) (w : W), s c w ≠ f

def Jaeger2014.SemanticGame.icrR {C : Type u_2} {W : Type u_3} {F : Type u_4} {A : Type u_5} [Fintype C] [Fintype W] [Fintype F] [Fintype A] [DecidableEq C] [DecidableEq W] [DecidableEq F] (g : SemanticGame C W F A) : ℕ → Set (C → F → A)

The receiver side of the ICR sequence (Def. 4). icrR 0 is the set of credulous strategies — pointwise optimal against the prior updated with the literal meaning. icrR (n+1) consists of the cautious responses to icrS n that moreover interpret unexpected signals as literally true under some consistent belief revision (a full-support prior updated with the signal's extension).

Equations

• One or more equations did not get rendered due to their size.
• g.icrR 0 = {r : C → F → A | ∀ (c : C) (f : F), r c f ∈ g.optimalActions c (g.extension f) g.prior}

def Jaeger2014.SemanticGame.icrS {C : Type u_2} {W : Type u_3} {F : Type u_4} {A : Type u_5} [Fintype C] [Fintype W] [Fintype F] [Fintype A] [DecidableEq C] [DecidableEq W] [DecidableEq F] (g : SemanticGame C W F A) (n : ℕ) : Set (C → W → F)

The sender side of the ICR sequence (Def. 4): cautious responses to the receiver's current stage.

Equations

• g.icrS n = g.senderCR (g.icrR n)

def Jaeger2014.SemanticGame.prsS {C : Type u_2} {W : Type u_3} {F : Type u_4} {A : Type u_5} [Fintype C] [Fintype W] [Fintype F] [Fintype A] [DecidableEq C] [DecidableEq W] [DecidableEq F] (g : SemanticGame C W F A) : Set (C → W → F)

Def. 5: pragmatically rationalizable sender strategies — those recurring arbitrarily late in the ICR sequence.

Equations

• g.prsS = {s : C → W → F | ∀ (n : ℕ), ∃ m > n, s ∈ g.icrS m}

def Jaeger2014.SemanticGame.prsR {C : Type u_2} {W : Type u_3} {F : Type u_4} {A : Type u_5} [Fintype C] [Fintype W] [Fintype F] [Fintype A] [DecidableEq C] [DecidableEq W] [DecidableEq F] (g : SemanticGame C W F A) : Set (C → F → A)

Def. 5: pragmatically rationalizable receiver strategies.

Equations

• g.prsR = {r : C → F → A | ∀ (n : ℕ), ∃ m > n, r ∈ g.icrR m}

def Jaeger2014.SemanticGame.IsRationalizable {C : Type u_2} {W : Type u_3} {F : Type u_4} {A : Type u_5} [Fintype C] [Fintype W] [Fintype F] [Fintype A] [DecidableEq C] [DecidableEq W] [DecidableEq F] (g : SemanticGame C W F A) (s : C → W → F) (r : C → F → A) : Prop

Def. 6 (after Osborne): a strategy pair is rationalizable iff it belongs to a pair of sets each of whose members is a best response to some belief supported inside the other set.

Equations

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

Theorem 1: pragmatic rationalizability implies rationalizability

The ICR sequence is a deterministic dynamical system on the finite space of strategy-set pairs, hence eventually periodic; beyond the periodic threshold every stage lies inside the recurrence sets prsS/prsR, which therefore witness rationalizability for every pragmatically rationalizable pair.

theorem Jaeger2014.SemanticGame.prs_rationalizable {C : Type u_2} {W : Type u_3} {F : Type u_4} {A : Type u_5} [Fintype C] [Fintype W] [Fintype F] [Fintype A] [DecidableEq C] [DecidableEq W] [DecidableEq F] (g : SemanticGame C W F A) {s : C → W → F} {r : C → F → A} (hs : s ∈ g.prsS) (hr : r ∈ g.prsR) : g.IsRationalizable s r

[Jag14], Theorem 1: pragmatically rationalizable strategy pairs are rationalizable. The recurrence sets themselves are the witness: every recurring sender strategy is a cautious (hence best) response to a belief supported on a late ICR receiver stage, which lies inside prsR; symmetrically for the receiver, whose late stages are cautious responses to late sender stages inside prsS.

Best-response characterizations

Def. 2's argmaxes range over whole strategy spaces, but the objectives are additively separable: the sender's depends only on the signal chosen at the quantified context/world, the receiver's is a sum of per-signal terms against posterior-weighted world masses. Finset.mem_argmax_comp_surjective and Finset.mem_argmax_pi_sum reduce both to pointwise argmaxes — the form in which the §5 examples are actually computed.

def Jaeger2014.SemanticGame.senderEU {C : Type u_2} {W : Type u_3} {F : Type u_4} {A : Type u_5} [Fintype C] [Fintype W] [Fintype F] [Fintype A] [DecidableEq C] [DecidableEq F] (g : SemanticGame C W F A) (ρ : (C → F → A) → ℝ) (q : C → ℝ) (c : C) (w : W) (f : F) : ℝ

The sender's expected utility of sending f at (c, w) under the belief (ρ, q).

Equations

• g.senderEU ρ q c w f = ∑ r : C → F → A, ρ r * ∑ c' : C, q c' * g.uS c w f (r c' f)

theorem Jaeger2014.SemanticGame.mem_senderBR_iff {C : Type u_2} {W : Type u_3} {F : Type u_4} {A : Type u_5} [Fintype C] [Fintype W] [Fintype F] [Fintype A] [DecidableEq C] [DecidableEq W] [DecidableEq F] (g : SemanticGame C W F A) (ρ : (C → F → A) → ℝ) (q : C → ℝ) (s' : C → W → F) : s' ∈ g.senderBR ρ q ↔ ∀ (c : C) (w : W), s' c w ∈ Finset.univ.argmax (g.senderEU ρ q c w)

Sender best responses, pointwise: s' is a best response iff at every context/world it picks a signal maximizing expected utility.

def Jaeger2014.SemanticGame.receiverEU {C : Type u_2} {W : Type u_3} {F : Type u_4} {A : Type u_5} [Fintype C] [Fintype W] [Fintype F] [DecidableEq C] [DecidableEq W] [DecidableEq F] (g : SemanticGame C W F A) (σ : (C → W → F) → ℝ) (q : C → ℝ) (c : C) (f : F) (a : A) : ℝ

The receiver's per-signal objective: expected utility of playing a on signal f, against the belief (σ, q) — the prior-weighted utility restricted to the occasions on which f is actually sent.

Equations

• g.receiverEU σ q c f a = ∑ s : C → W → F, σ s * ∑ c' : C, q c' * ∑ w : W, g.prior w * if s c' w = f then g.uR c w a else 0

theorem Jaeger2014.SemanticGame.mem_receiverBR_iff {C : Type u_2} {W : Type u_3} {F : Type u_4} {A : Type u_5} [Fintype C] [Fintype W] [Fintype F] [Fintype A] [DecidableEq C] [DecidableEq W] [DecidableEq F] (g : SemanticGame C W F A) (σ : (C → W → F) → ℝ) (q : C → ℝ) (r' : C → F → A) : r' ∈ g.receiverBR σ q ↔ ∀ (c : C) (f : F), r' c f ∈ Finset.univ.argmax (g.receiverEU σ q c f)

Receiver best responses, pointwise: r' is a best response iff at every context and signal it picks an action maximizing posterior-weighted expected utility.

Fixed points collapse the recurrence sets

theorem Jaeger2014.SemanticGame.prsR_eq_of_fixed {C : Type u_2} {W : Type u_3} {F : Type u_4} {A : Type u_5} [Fintype C] [Fintype W] [Fintype F] [Fintype A] [DecidableEq C] [DecidableEq W] [DecidableEq F] (g : SemanticGame C W F A) {n : ℕ} (hfix : g.icrR (n + 1) = g.icrR n) : g.prsR = g.icrR n

At a fixed point of the ICR step, the pragmatically rationalizable receiver strategies are exactly the fixed stage.

theorem Jaeger2014.SemanticGame.prsS_eq_of_fixed {C : Type u_2} {W : Type u_3} {F : Type u_4} {A : Type u_5} [Fintype C] [Fintype W] [Fintype F] [Fintype A] [DecidableEq C] [DecidableEq W] [DecidableEq F] (g : SemanticGame C W F A) {n : ℕ} (hfix : g.icrR (n + 1) = g.icrR n) : g.prsS = g.icrS n

At a fixed point of the ICR step, the pragmatically rationalizable sender strategies are exactly the fixed sender stage.

Message credibility

def Jaeger2014.SemanticGame.Credible {C : Type u_2} {W : Type u_3} {F : Type u_4} {A : Type u_5} [Fintype C] [Fintype W] [Fintype F] [Fintype A] [DecidableEq C] [DecidableEq W] [DecidableEq F] (g : SemanticGame C W F A) (f : F) : Prop

Rabin-style message credibility ([Jag14] §4): a signal is credible iff every pragmatically rationalizable sender strategy uses it according to its literal meaning.

Equations

• g.Credible f = ∀ s ∈ g.prsS, ∀ (c : C) (w : W), s c w = f → g.meaning f w

Support-restricted belief helpers

theorem Jaeger2014.IsFullDistOn.singleton_eq_one {M : Type u_1} [Fintype M] {r₀ : M} {ρ : M → ℝ} (h : IsFullDistOn {r₀} ρ) : ρ r₀ = 1

theorem Jaeger2014.sum_mul_of_fullDistOn_singleton {M : Type u_1} [Fintype M] {r₀ : M} {ρ : M → ℝ} (h : IsFullDistOn {r₀} ρ) (X : M → ℝ) : ∑ r : M, ρ r * X r = X r₀

A sum against a belief supported on a single strategy collapses to the value at that strategy.

theorem Jaeger2014.sum_mul_of_fullDistOn_pair {M : Type u_1} [Fintype M] [DecidableEq M] {a b : M} (hab : a ≠ b) {ρ : M → ℝ} (h : IsFullDistOn {a, b} ρ) (X : M → ℝ) : ∑ r : M, ρ r * X r = ρ a * X a + ρ b * X b

A sum against a belief supported on a pair collapses to the two terms.

theorem Jaeger2014.IsFullDistOn.pair_props {M : Type u_1} [Fintype M] [DecidableEq M] {a b : M} (hab : a ≠ b) {ρ : M → ℝ} (h : IsFullDistOn {a, b} ρ) : 0 < ρ a ∧ 0 < ρ b ∧ ρ a + ρ b = 1

The pair of weights of a full-support belief on a pair sums to 1, with both weights positive.

theorem Jaeger2014.isFullDistOn_pointMass {M : Type u_1} [Fintype M] [DecidableEq M] (r₀ : M) : IsFullDistOn {r₀} fun (r : M) => if r = r₀ then 1 else 0

The point mass on r₀ has full support on {r₀}.

theorem Jaeger2014.isFullDistOn_pairUniform {M : Type u_1} [Fintype M] [DecidableEq M] {a b : M} (hab : a ≠ b) : IsFullDistOn {a, b} fun (r : M) => if r = a then 1 / 2 else if r = b then 1 / 2 else 0

The uniform belief on a pair has full support on it.

theorem Jaeger2014.isFullDistOn_pairWeighted {M : Type u_1} [Fintype M] [DecidableEq M] {a b : M} (hab : a ≠ b) {t : ℝ} (h0 : 0 < t) (h1 : t < 1) : IsFullDistOn {a, b} fun (r : M) => if r = a then t else if r = b then 1 - t else 0

A weighted belief on a pair, with weight t on a and 1 - t on b, has full support on the pair whenever 0 < t < 1.

theorem Jaeger2014.pairWeighted_apply_right {M : Type u_1} [DecidableEq M] {a b : M} (hab : a ≠ b) {t : ℝ} : (if b = a then t else if b = b then 1 - t else 0) = 1 - t

The weight of a isFullDistOn_pairWeighted belief on its second point.

theorem Jaeger2014.isFullDist_unitOne : IsFullDist fun (x : Unit) => 1

The constant-one function is a full-support distribution over Unit.

theorem Jaeger2014.IsFullDist.unit_eq_one {q : Unit → ℝ} (h : IsFullDist q) : q () = 1

Horn's division of pragmatic labor ([Jag14] §5, Example 6)

Two worlds (world 0 frequent with prior 3/4, world 1 rare), two semantically equivalent signals (both tautologies), with signal 1 costlier by one util; matching utilities scaled by 5; a single context. The ICR trace R₀ … S₂ reaches a fixed point at the Horn convention: the cheap form marks the frequent world, the costly form the rare one — both PRS sets are the identity strategies.

noncomputable def Jaeger2014.Horn.game : SemanticGame Unit (Fin 2) (Fin 2) (Fin 2)

Example 6's semantic game.

Equations

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

Evaluating the ICR trace

Both signals are tautologous, the context is trivial, and only two strategies ever occur — fun _ _ => 0 and fun _ x => x — so every stage reduces to a pair of argmaxes over Fin 2 against a belief whose support is a singleton or that pair.

Expected-utility values against the trace's beliefs

The two recurring strategies

fun _ _ => 0 and fun _ x => x are the only functions in the trace; the support sets {h | h () 0 = 0} and {h | h () 0 = 0 ∧ h () 1 = 1} are their pair and their common identity element.

The sender stages S₀ and S₂

Against a receiver who ignores the signal (fun _ _ => 0) the sender always prefers the cheap form; against the literal receiver (fun _ x => x) the sender matches signal to world — the Horn convention.

The receiver stages R₁, R₂ and R₃

The credulous stage sends the cheap form at both worlds, so the cheap form's receiver is pinned to world 0 while the costly form is unexpected (any action survives, but the belief-revision clause is vacuously satisfiable). Once the sender separates, both forms are expected and the receiver reads each literally.

The sender stage S₁

Against a belief mixing the two receivers, the frequent world still fixes the cheap form, but the rare world's optimal form depends on how much mass the literal receiver carries — so both s () 1 = 0 and s () 1 = 1 survive, giving {s | s () 0 = 0}.

The receiver stage R₂

Once the sender separates the worlds, both forms are expected and each is read literally: the cheap form as the frequent world, the costly form as the rare one. No signal is unexpected, so the belief-revision clause is vacuous.

The fixed point R₃ = R₂

The separating sender is now stable: the receiver's cautious responses to it again read both forms literally, reproducing R₂.

theorem Jaeger2014.Horn.division_of_pragmatic_labor : game.prsS = {fun (x : Unit) (w : Fin 2) => w} ∧ game.prsR = {fun (x : Unit) (f : Fin 2) => f}

Horn's division of pragmatic labor ([Jag14] §5, Example 6): in the two-synonyms game, the pragmatically rationalizable strategies are exactly the Horn convention — the cheap form marks the frequent world and the costly form the rare one; both PRS sets are the identity strategies.