5. Two definitions¶
In this chapter we define symmetric Nash equilibrium and evolutionary stability, and check both against the Prisoner's Dilemma. As with strict dominance in chapter 4, the definitions are general: they take any type of strategies and any payoff function, and they say nothing about how the payoffs are computed. That generality is what makes the proof in chapter 6 possible.
Create GameTheory/Equilibria.lean, add it to GameTheory.lean, and begin:
Symmetric Nash equilibrium¶
A strategy is a symmetric Nash equilibrium when, with the opponent playing it, no deviation pays more than playing it too:
/-- A strategy is a symmetric Nash equilibrium if, when the opponent plays it,
no deviation pays strictly more than playing it too. -/
def IsSymmetricNash {Strategy : Type} (payoffs : Strategy → Strategy → ℝ)
(candidate : Strategy) : Prop :=
∀ deviation : Strategy, payoffs deviation candidate ≤ payoffs candidate candidate
Nothing here is new in Lean terms. It is a def producing a Prop, with an
implicit type of strategies, and a ∀ over deviations, exactly the shape of
StrictlyDominates. The symbol ≤ is typed \le.
We check only the first player's deviations. Since the game is symmetric, the second player's incentive is the same statement with the roles swapped, so a single inequality captures both.
Evolutionary stability¶
An evolutionarily stable strategy is harder to state. A resident strategy is stable if every mutant that differs from it either does strictly worse against the resident, or ties against the resident and then does strictly worse against itself than the resident does against it:
/-- A strategy is evolutionarily stable if every distinct mutant either does
strictly worse against the resident, or ties against the resident and then
does strictly worse against itself than the resident does against it. -/
def IsESS {Strategy : Type} (payoffs : Strategy → Strategy → ℝ)
(resident : Strategy) : Prop :=
∀ mutant : Strategy, mutant ≠ resident →
payoffs mutant resident < payoffs resident resident ∨
(payoffs mutant resident = payoffs resident resident ∧
payoffs mutant mutant < payoffs resident mutant)
This is the condition of Maynard Smith and Price, and it brings in four pieces
of logic. The symbol ≠, typed \ne, is inequality. The symbols ∨ and ∧,
typed \or and \and, are 'or' and 'and'. The arrow after mutant ≠
resident is implication: for every mutant, if it differs from the resident,
then the disjunction holds.
That the arrow for implication is the same arrow as for functions is not a
coincidence of notation. A proof of P → Q is a function that turns any proof
of P into a proof of Q. This is the same idea as in chapter 3, where a
statement was a type and a proof a value of it, and we will use it directly in
chapter 6.
Note that every inequality is written with the worse payoff on the left and
the better on the right, as in StrictlyDominates. Lean does not care, but a
reader scanning goal states does.
The hypothesis mutant ≠ resident looks like a technicality, and it is worth
seeing why it is not. Without it the resident is its own mutant, and the
definition asks for payoffs resident resident < payoffs resident resident
in one branch or the other. No strategy satisfies that, so the definition
would hold of nothing. Lean accepts the broken version without complaint,
because it is a perfectly good statement that happens to be false. This is
what chapter 2 meant by definitions being harder than proofs: Lean checks that
a definition makes sense, never that it says what we meant.
A definition that says yes¶
Mutual defection is a symmetric Nash equilibrium, proved exactly as dominance was:
/-- Mutual defection is a symmetric Nash equilibrium of the Prisoner's Dilemma. -/
theorem defect_isSymmetricNash : IsSymmetricNash payoff defect := by
intro deviation
cases deviation <;> norm_num [payoff]
After intro deviation the goal is
and the two cases are 0 ≤ 1 and 1 ≤ 1, which norm_num settles.
A definition that says no¶
One way to test a definition is to check that it rules out what it should. Mutual cooperation is not a Nash equilibrium, since a cooperator facing a cooperator gains by defecting:
/-- Mutual cooperation is not: a cooperator facing a cooperator gains by
defecting. -/
theorem not_cooperate_isSymmetricNash : ¬ IsSymmetricNash payoff cooperate := by
intro claim
have tempted := claim defect
norm_num [payoff] at tempted
The symbol ¬, typed \not, is negation, and in Lean ¬ P means P →
False. To prove it we assume P and derive a contradiction, which is why the
proof starts with intro, just as for an implication. After intro claim the
goal is:
claim says that no deviation beats cooperation. We apply it to the
deviation defect, and have records the result under a name:
claim : IsSymmetricNash payoff cooperate
tempted : payoff defect cooperate ≤ payoff cooperate cooperate
⊢ False
Note how claim defect is written. claim is a proof of a ∀ statement, and
a proof of a ∀ is a function: give it a particular deviation and it returns
the inequality for that deviation.
tempted says that 5 is at most 3. The final line runs norm_num on the
hypothesis rather than on the goal, which is what at tempted asks for. It
reduces tempted to False, and a hypothesis that is False proves any
goal, so the proof is finished.
An evolutionarily stable strategy¶
Finally, defection is an ESS:
/-- Defection is an evolutionarily stable strategy of the Prisoner's Dilemma. -/
theorem defect_isESS : IsESS payoff defect := by
intro mutant distinct
cases mutant
· left
norm_num [payoff]
· contradiction
A single intro can take several names. IsESS is a ∀ followed by an
implication, so intro mutant distinct names the mutant and the hypothesis
that it differs from the resident:
mutant : Action
distinct : mutant ≠ defect
⊢ payoff mutant defect < payoff defect defect ∨
payoff mutant defect = payoff defect defect ∧ payoff mutant mutant < payoff defect mutant
After cases mutant, the substitution reaches the hypothesis as well as the
goal:
case cooperate
distinct : cooperate ≠ defect
⊢ payoff cooperate defect < payoff defect defect ∨
payoff cooperate defect = payoff defect defect ∧ payoff cooperate cooperate < payoff defect cooperate
case defect
distinct : defect ≠ defect
⊢ payoff defect defect < payoff defect defect ∨
payoff defect defect = payoff defect defect ∧ payoff defect defect < payoff defect defect
In the first case the mutant cooperates and does strictly worse, so we want
the left side of the disjunction. left commits to it, leaving
which is, once more, the theorem of chapter 3.
The second case is more interesting. The goal there is false: it asks for
payoff defect defect < payoff defect defect in one form or another. We do
not prove it. Instead we notice that the hypothesis distinct claims
defect ≠ defect, which cannot hold, and contradiction closes any goal whose
context contains such an impossibility. The case is not true, it is
unreachable.
With the cursor on contradiction, the infoview shows both halves of the
situation: the hypothesis distinct : defect ≠ defect, and below it a goal
that asks for a payoff to be strictly less than itself:
Where we are¶
Both definitions exist, and both behave correctly on the Prisoner's Dilemma.
We have met three more tactics: left to choose a side of a disjunction,
have to name an intermediate fact, and contradiction to dismiss an
impossible case. We have also seen at, which aims a tactic at a hypothesis
rather than the goal. Most importantly, a proof of a ∀
can be applied like a function, which is the key step in chapter 6.
In chapter 6 we prove that every ESS is a symmetric Nash equilibrium, for every game at once.