Lean declarations

def PrisonersDilemma.PD EconCSLib @ cef01c7, EconCSLib.Examples.PrisonersDilemma

The Prisoner's Dilemma as a strategic game with natural number payoffs.

def PD : StrategicGame (Fin 2) ℕ where
  strategy := fun _ => PDMove
  payoff σ i :=
    match σ 0, σ 1 with
    | Cooperate, Cooperate => 3
    | Cooperate, Defect    => if i = 0 then 0 else 5
    | Defect,    Cooperate => if i = 0 then 5 else 0
    | Defect,    Defect    => 1

theorem PrisonersDilemma.pd_defect_weakly_dominant EconCSLib @ cef01c7, EconCSLib.Examples.PrisonersDilemma
```
theorem pd_defect_weakly_dominant : ∀ i : Fin 2, IsWeaklyDominant PD i Defect
```
theorem PrisonersDilemma.pd_defect_nash EconCSLib @ cef01c7, EconCSLib.Examples.PrisonersDilemma
T4b: (Defect, Defect) is a Nash equilibrium, by T3 (dominant profile → Nash).
```
theorem pd_defect_nash : IsNashEquilibrium PD (fun _ => Defect)
```
theorem PrisonersDilemma.pd_nash_unique EconCSLib @ cef01c7, EconCSLib.Examples.PrisonersDilemma
T4c: (Defect, Defect) is the *unique* pure Nash equilibrium.
```
theorem pd_nash_unique : ∀ σ : PD.Profile,
    IsNashEquilibrium PD σ → σ = fun _ => Defect
```
theorem PrisonersDilemma.pd_pareto_suboptimal EconCSLib @ cef01c7, EconCSLib.Examples.PrisonersDilemma
The social optimum (Cooperate, Cooperate) is Pareto-superior to the Nash outcome.
```
theorem pd_pareto_suboptimal :
    PD.payoff (fun _ => Cooperate) 0 > PD.payoff (fun _ => Defect) 0
```

Modules: EconCSLib.Examples.PrisonersDilemma

Prisoner's Dilemma

The Prisoner's Dilemma is a two-player strategic game where each player can Cooperate ($C$) or Defect ($D$). The Lean example uses this normalized payoff matrix:

	$C$	$D$
$C$	(3, 3)	(0, 5)
$D$	(5, 0)	(1, 1)

Defecting is a weakly dominant strategy for each player. The unique Nash equilibrium is $(D, D)$ with payoff $(1, 1)$, which is Pareto-dominated by $(C, C)$ with payoff $(3, 3)$.

References

[MSZ, Chapter 4] Maschler, Solan, and Zamir, Game Theory. Prisoner's Dilemma in utility units.

Prisoner's Dilemma

References

Also in