Jäger (2014): Rationalizable Signaling

This file formalizes [Jag14], the iterated cautious response model of game-theoretic pragmatics. A semantic game equips a signaling game with contexts, the players' uncertainty about each other's preferences, an interpretation function and cost-separable sender utilities (SemanticGame). Following Pearce's rationalizability, a cautious response to a set of the opponent's strategies is a best response to some belief giving every member of the set positive probability, Definitions 2 and 3; the iterated cautious response sequence, Definition 4, starts from the credulous receiver, who acts on the literal meaning of each signal, and alternates cautious responses, the receiver reading an unexpected signal as true under some revised belief. The pragmatically rationalizable strategies are those recurring arbitrarily late in the sequence, Definition 5. Theorem 1, prs_rationalizable: they are rationalizable in the classical sense, Definition 6, since the sequence is a deterministic dynamical system on a finite space and so eventually periodic, its late stages lying inside the recurrence sets that witness rationalizability. The best responses of Definition 2 reduce to pointwise argmaxes (mem_senderBR_iff, mem_receiverBR_iff), the form in which Section 5 computes the examples, and at a fixed point the recurrence sets are the fixed stage (prsR_eq_of_fixed). Example 6, Horn's division of pragmatic labor, (4): with two synonymous signals, the costlier by one unit, and a 3:1 prior, the sequence reaches its fixed point at the convention that the cheap form marks the frequent world and the costly form the rare one (Horn.division_of_pragmatic_labor), the costly form being read as the rare world although, in the sense of Rabin's credibility recast in Section 7, it is not credible.

Implementation notes

• Beliefs are functions to ℝ; Δ(M) is mathlib's stdSimplex ℝ M, and the full-support and support-restricted variants int(Δ(M)) and Δ(P) are stated locally, the relative interior of the simplex having no lightweight mathlib form.
• Examples 1 to 5 and 7 to 10, including the comparison with [Fra11]'s iterated best response in Section 6, are not formalized; Section 5's linguistic examples are rows.

References

• [Jag14]
• [JE09]
• [Fra11]

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's message credibility recast in Section 7: a signal is credible iff at every stage every sender strategy uses it wherever it is true, ⟦f⟧ ⊆ s⁻¹(f).

Equations

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

Beliefs on a singleton and on a pair

A full-support belief on one strategy is its point mass, and on a pair of strategies a mixture with weights t and 1 - t for some 0 < t < 1; sums against such beliefs collapse to the support.

def Jaeger2014.mix {M : Type u_1} [DecidableEq M] (a b : M) (t : ℝ) : M → ℝ

The mixture of two point masses with weight t on a.

Equations

• Jaeger2014.mix a b t r = if r = a then t else if r = b then 1 - t else 0

theorem Jaeger2014.isFullDistOn_singleton_iff {M : Type u_1} [Fintype M] [DecidableEq M] {a : M} {ρ : M → ℝ} : IsFullDistOn {a} ρ ↔ ρ = Pi.single a 1

theorem Jaeger2014.isFullDistOn_pair_iff {M : Type u_1} [Fintype M] [DecidableEq M] {a b : M} {ρ : M → ℝ} (hab : a ≠ b) : IsFullDistOn {a, b} ρ ↔ ∃ (t : ℝ), 0 < t ∧ t < 1 ∧ ρ = mix a b t

theorem Jaeger2014.sum_mul_single {M : Type u_1} [Fintype M] [DecidableEq M] {a : M} (X : M → ℝ) : ∑ r : M, Pi.single a 1 r * X r = X a

theorem Jaeger2014.sum_mul_mix {M : Type u_1} [Fintype M] [DecidableEq M] {a b : M} (hab : a ≠ b) (t : ℝ) (X : M → ℝ) : ∑ r : M, mix a b t r * X r = t * X a + (1 - t) * X b

theorem Jaeger2014.isFullDist_unit_iff {q : Unit → ℝ} : IsFullDist q ↔ q = fun (x : Unit) => 1

Over a single context the only full-support belief is certainty.

theorem Jaeger2014.SemanticGame.mem_senderCR_iff {C : Type u_1} {W : Type u_2} {F : Type u_3} {A : Type u_4} [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)} {s : C → W → F} : s ∈ g.senderCR R ↔ ∃ (ρ : (C → F → A) → ℝ) (q : C → ℝ), IsFullDistOn R ρ ∧ IsFullDist q ∧ ∀ (c : C) (w : W), s c w ∈ Finset.univ.argmax (g.senderEU ρ q c w)

Cautious responses of the sender, pointwise.

theorem Jaeger2014.SemanticGame.mem_receiverCR_iff {C : Type u_1} {W : Type u_2} {F : Type u_3} {A : Type u_4} [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)} {r : C → F → A} : r ∈ g.receiverCR S ↔ ∃ (σ : (C → W → F) → ℝ) (q : C → ℝ), IsFullDistOn S σ ∧ IsFullDist q ∧ ∀ (c : C) (f : F), r c f ∈ Finset.univ.argmax (g.receiverEU σ q c f)

Cautious responses of the receiver, pointwise.

theorem Jaeger2014.SemanticGame.senderEU_single {C : Type u_1} {W : Type u_2} {F : Type u_3} {A : Type u_4} [Fintype C] [Fintype W] [Fintype F] [Fintype A] [DecidableEq C] [DecidableEq F] (g : SemanticGame C W F A) [DecidableEq A] (r₀ : C → F → A) (q : C → ℝ) (c : C) (w : W) (f : F) : g.senderEU (Pi.single r₀ 1) q c w f = ∑ c' : C, q c' * g.uS c w f (r₀ c' f)

The sender's expected utility against a single receiver strategy.

theorem Jaeger2014.SemanticGame.senderEU_mix {C : Type u_1} {W : Type u_2} {F : Type u_3} {A : Type u_4} [Fintype C] [Fintype W] [Fintype F] [Fintype A] [DecidableEq C] [DecidableEq F] (g : SemanticGame C W F A) [DecidableEq A] {r₀ r₁ : C → F → A} (h : r₀ ≠ r₁) (t : ℝ) (q : C → ℝ) (c : C) (w : W) (f : F) : g.senderEU (mix r₀ r₁ t) q c w f = t * ∑ c' : C, q c' * g.uS c w f (r₀ c' f) + (1 - t) * ∑ c' : C, q c' * g.uS c w f (r₁ c' f)

The sender's expected utility against a mixture of two receiver strategies.

theorem Jaeger2014.SemanticGame.receiverEU_single {C : Type u_1} {W : Type u_2} {F : Type u_3} {A : Type u_4} [Fintype C] [Fintype W] [Fintype F] [DecidableEq C] [DecidableEq W] [DecidableEq F] (g : SemanticGame C W F A) (s₀ : C → W → F) (q : C → ℝ) (c : C) (f : F) (a : A) : g.receiverEU (Pi.single s₀ 1) q c f a = ∑ c' : C, q c' * ∑ w : W, g.prior w * if s₀ c' w = f then g.uR c w a else 0

The receiver's expected utility against a single sender strategy.

theorem Jaeger2014.SemanticGame.receiverEU_mix {C : Type u_1} {W : Type u_2} {F : Type u_3} {A : Type u_4} [Fintype C] [Fintype W] [Fintype F] [DecidableEq C] [DecidableEq W] [DecidableEq F] (g : SemanticGame C W F A) {s₀ s₁ : C → W → F} (h : s₀ ≠ s₁) (t : ℝ) (q : C → ℝ) (c : C) (f : F) (a : A) : g.receiverEU (mix s₀ s₁ t) q c f a = (t * ∑ c' : C, q c' * ∑ w : W, g.prior w * if s₀ c' w = f then g.uR c w a else 0) + (1 - t) * ∑ c' : C, q c' * ∑ w : W, g.prior w * if s₁ c' w = f then g.uR c w a else 0

The receiver's expected utility against a mixture of two sender strategies.

Horn's division of pragmatic labor (Section 5, Example 6)

Two worlds, the first three times as likely as the second, two synonymous signals, both tautologies, the second costing one unit more, matching utilities of 5, one context. The sequence runs R₀ = {0}, S₀ = {0}, R₁ = {r | r 0 = 0}, S₁ = {s | s 0 = 0}, R₂ = S₂ = {id} and stays there; each stage is an argmax over Fin 2 against a belief on the one or two strategies of the previous stage.

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

Example 6's semantic game, Table 10.

Equations

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

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, Example 6: the pragmatically rationalizable strategies are the convention on which the cheap form marks the frequent world and the costly form the rare one, the identity strategies on both sides.

theorem Jaeger2014.Horn.not_credible_costly : ¬game.Credible 1

The costly form is not credible: at the stage S₁ the sender may still use the cheap form at the rare world, where the costly form is true; pragmatic rationalizability nevertheless fixes its reading.

structure Jaeger2014.Horn.Row : Type

A row of (4): the signal of Example 6 the sentence realizes and the world it is read as.

• signal : Fin 2
• world : Fin 2

def Jaeger2014.Horn.instDecidableEqRow.decEq (x✝ x✝¹ : Row) : Decidable (x✝ = x✝¹)

Equations

• Jaeger2014.Horn.instDecidableEqRow.decEq { signal := a, world := a_1 } { signal := b, world := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Jaeger2014.Horn.instDecidableEqRow : DecidableEq Row

Equations

• Jaeger2014.Horn.instDecidableEqRow = Jaeger2014.Horn.instDecidableEqRow.decEq

def Jaeger2014.Horn.Row.ofExample (e : Data.Examples.LinguisticExample) : Option Row

A row from the paper's features.

Equations

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

def Jaeger2014.Horn.rows : List Row

The two synonyms of (4).

Equations

• Jaeger2014.Horn.rows = List.filterMap Jaeger2014.Horn.Row.ofExample Jaeger2014.Examples.all

theorem Jaeger2014.Horn.readings_of_4 (r : Row) : r ∈ rows → ∀ ρ ∈ game.prsR, ρ () r.signal = r.world

Every pragmatically rationalizable receiver reads each form of (4) as the world the paper reports: the regular stop for the cheap form, the abnormal one for the costly form.