Strategic Games @cite{fehr-schmidt-1999}

@cite{houlihan-kleiman-weiner-hewitt-tenenbaum-saxe-2023}

Multi-agent game infrastructure for social cognition.

Existing DecisionTheory.lean is single-agent: one decision-maker, one prior, one utility. But emotion prediction, politeness, and game-theoretic pragmatics all require strategic interaction — one agent's payoff depends on what another agent does.

This module provides:

• SymmetricGame: 2-player symmetric game with payoff matrix
• Base features (Money, AI, DI) as deterministic functions of action pairs
• Split-or-Steal (@cite{houlihan-kleiman-weiner-hewitt-tenenbaum-saxe-2023}) as a weak Prisoner's Dilemma

Connection to BToM

A SymmetricGame determines the utility field of a BToM generative model: the agent's Desire type becomes the Fehr-Schmidt preference weights (ω_Money, ω_AIA, ω_DIA), and the planModel implements expected-utility maximization over those weighted base features.

Connection to Pragmatics

Signaling games (@cite{franke-2011}, @cite{lewis-1969}) extend this to games where actions = utterances and payoffs depend on communicated information. The current module covers non-communicative games; signaling games are in Theories/Pragmatics/SignalingGames.lean.

inductive Pragmatics.GameTheory.Action2 : Type

Binary action in a 2-player game.

• cooperate : Action2
• defect : Action2

@[implicit_reducible]

instance Pragmatics.GameTheory.instDecidableEqAction2 : DecidableEq Action2

Equations

• Pragmatics.GameTheory.instDecidableEqAction2 x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Pragmatics.GameTheory.instReprAction2.repr : Action2 → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Pragmatics.GameTheory.instReprAction2 : Repr Action2

Equations

• Pragmatics.GameTheory.instReprAction2 = { reprPrec := Pragmatics.GameTheory.instReprAction2.repr }

@[implicit_reducible]

instance Pragmatics.GameTheory.instInhabitedAction2 : Inhabited Action2

Equations

• Pragmatics.GameTheory.instInhabitedAction2 = { default := Pragmatics.GameTheory.instInhabitedAction2.default }

def Pragmatics.GameTheory.instInhabitedAction2.default : Action2

Equations

• Pragmatics.GameTheory.instInhabitedAction2.default = Pragmatics.GameTheory.Action2.cooperate

@[implicit_reducible]

instance Pragmatics.GameTheory.instFintypeAction2 : Fintype Action2

Equations

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

structure Pragmatics.GameTheory.SymmetricGame : Type

A 2-player symmetric game: payoff a₁ a₂ is player 1's material payoff when player 1 plays a₁ and player 2 plays a₂.

Symmetric: player 2's payoff when (a₁, a₂) is played equals player 1's payoff when (a₂, a₁) is played.

• payoff : Action2 → Action2 → ℚ

def Pragmatics.GameTheory.SymmetricGame.otherPayoff (g : SymmetricGame) (a₁ a₂ : Action2) : ℚ

Player 2's payoff (by symmetry).

Equations

• g.otherPayoff a₁ a₂ = g.payoff a₂ a₁

def Pragmatics.GameTheory.SymmetricGame.di (g : SymmetricGame) (a₁ a₂ : Action2) : ℚ

Disadvantageous inequality for player 1 in outcome (a₁, a₂).

Equations

• g.di a₁ a₂ = Core.disadvantageousInequality (g.payoff a₁ a₂) (g.otherPayoff a₁ a₂)

def Pragmatics.GameTheory.SymmetricGame.ai (g : SymmetricGame) (a₁ a₂ : Action2) : ℚ

Advantageous inequality for player 1 in outcome (a₁, a₂).

Equations

• g.ai a₁ a₂ = Core.advantageousInequality (g.payoff a₁ a₂) (g.otherPayoff a₁ a₂)

def Pragmatics.GameTheory.SymmetricGame.baseFeatures (g : SymmetricGame) (a₁ a₂ : Action2) : ℚ × ℚ × ℚ

Base features: the three Fehr-Schmidt utility components. Returns (Money, AI, DI) — all deterministic given the action pair.

Equations

• g.baseFeatures a₁ a₂ = (g.payoff a₁ a₂, g.ai a₁ a₂, g.di a₁ a₂)

def Pragmatics.GameTheory.SymmetricGame.socialUtility (g : SymmetricGame) (a₁ a₂ : Action2) (ωMoney ωAIA ωDIA : ℚ) : ℚ

Weighted social utility for player 1 given Fehr-Schmidt weights.

U = ω_m · Money − ω_aia · AI − ω_dia · DI

Note the negative signs: AI and DI are costs.

Equations

• g.socialUtility a₁ a₂ ωMoney ωAIA ωDIA = ωMoney * g.payoff a₁ a₂ - ωAIA * g.ai a₁ a₂ - ωDIA * g.di a₁ a₂

theorem Pragmatics.GameTheory.SymmetricGame.socialUtility_eq_fehrSchmidt (g : SymmetricGame) (a₁ a₂ : Action2) (ωAIA ωDIA : ℚ) : g.socialUtility a₁ a₂ 1 ωAIA ωDIA = Core.fehrSchmidt (g.payoff a₁ a₂) (g.otherPayoff a₁ a₂) ωDIA ωAIA

Social utility with Fehr-Schmidt weights equals applying fehrSchmidt with rescaled parameters, when ωMoney = 1.

def Pragmatics.GameTheory.splitOrSteal (pot : ℚ) : SymmetricGame

The Split-or-Steal game from @cite{houlihan-kleiman-weiner-hewitt-tenenbaum-saxe-2023}.

A weak Prisoner's Dilemma: CC gives (pot/2, pot/2), CD gives (0, pot), DC gives (pot, 0), DD gives (0, 0). Unlike a standard PD, mutual defection yields the same payoff as being cooperated against — hence "weak."

Equations

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

theorem Pragmatics.GameTheory.splitOrSteal_cc_equal (pot : ℚ) : (splitOrSteal pot).payoff Action2.cooperate Action2.cooperate = (splitOrSteal pot).otherPayoff Action2.cooperate Action2.cooperate

CC: equal split, no inequality.

theorem Pragmatics.GameTheory.splitOrSteal_defect_weakly_dominates (pot : ℚ) (hpot : 0 < pot) (a₂ : Action2) : (splitOrSteal pot).payoff Action2.defect a₂ ≥ (splitOrSteal pot).payoff Action2.cooperate a₂

Defecting weakly dominates: ∀ a₂, payoff(D, a₂) ≥ payoff(C, a₂).

theorem Pragmatics.GameTheory.splitOrSteal_dc_ai (pot : ℚ) (hpot : 0 < pot) : (splitOrSteal pot).ai Action2.defect Action2.cooperate = pot

DC: defector gets everything — maximum advantageous inequality.

theorem Pragmatics.GameTheory.splitOrSteal_cd_di (pot : ℚ) (hpot : 0 < pot) : (splitOrSteal pot).di Action2.cooperate Action2.defect = pot

CD: cooperator gets nothing — maximum disadvantageous inequality.

theorem Pragmatics.GameTheory.splitOrSteal_cooperate_preferred_high_aia (pot : ℚ) (hpot : 0 < pot) (ωAIA : ℚ) (haia : ωAIA > 1) : (splitOrSteal pot).socialUtility Action2.cooperate Action2.cooperate 1 ωAIA 0 > (splitOrSteal pot).socialUtility Action2.defect Action2.cooperate 1 ωAIA 0

Despite weak dominance, a player with high enough AIA weight prefers to cooperate when the opponent cooperates.

CC: payoffs equal ⇒ AI = DI = 0 ⇒ socialUtility = pot/2. DC: payoff = pot, other = 0, AI = pot, DI = 0 ⇒ socialUtility = pot(1 − ωAIA). When ωAIA > 1/2: pot(1 − ωAIA) < pot/2, so cooperation is preferred.

This is the Fehr-Schmidt explanation of cooperation: an agent with high advantageous inequity aversion (AIA) — who dislikes getting more than others — will cooperate even though defection weakly dominates in material terms.