4. Quantifiers¶

Every proof so far has been about two named actions. Real game theory quantifies: a strategy is dominant when it does better against everything the opponent might do. In this chapter we say that in Lean, once, for any game, and then apply it to the Prisoner's Dilemma.

Create GameTheory/Dominance.lean, add it to GameTheory.lean, and begin:

import GameTheory.PrisonersDilemma

open Action

Importing our own module gives us Action, payoff, and everything they in turn imported, including norm_num.

A definition that is a statement¶

Here is strict dominance:

/-- One strategy strictly dominates another if it pays strictly more against
every strategy the opponent might choose. -/
def StrictlyDominates {Strategy : Type} (payoffs : Strategy → Strategy → ℝ)
    (better worse : Strategy) : Prop :=
  ∀ opponent : Strategy, payoffs worse opponent < payoffs better opponent

Compare this with payoff in chapter 2. That was a def whose type was ℝ, so it produced a number. This is a def whose type is Prop, so it produces a statement. StrictlyDominates payoff defect cooperate is not true or false in Lean's eyes until something proves it; it is a claim, sitting there, waiting.

Being able to define statements as freely as numbers is what makes it possible to build up game theory rather than merely check arithmetic, and it is why the convention is to name such definitions in upper camel case, as StrictlyDominates rather than strictlyDominates.

The definition is general. It does not mention Action and it does not mention our particular game. It takes any type of strategies at all, any payoff function on it, and two strategies to compare.

Implicit arguments¶

Notice the braces around {Strategy : Type} where the other arguments have parentheses. Braces make an argument implicit, meaning Lean works it out rather than making us write it. When we later write StrictlyDominates payoff defect cooperate, Lean sees that payoff has type Action → Action → ℝ and concludes that Strategy must be Action.

We can ask to see the arguments that are usually hidden by prefixing an @:

#check @StrictlyDominates

@StrictlyDominates : {Strategy : Type} → (Strategy → Strategy → ℝ) → Strategy → Strategy → Prop

Reading right to left: the whole thing produces a Prop, and to get there it consumes a type, a payoff function, and two strategies.

A universal statement¶

Now the Prisoner's Dilemma:

/-- In the Prisoner's Dilemma, defection strictly dominates cooperation. -/
theorem defect_strictlyDominates_cooperate :
    StrictlyDominates payoff defect cooperate := by
  intro opponent
  cases opponent
  · norm_num [payoff]
  · norm_num [payoff]

Follow the goal through the three tactics, because this is the pattern almost every later proof follows.

At the start the goal is the bare claim:

⊢ StrictlyDominates payoff defect cooperate

intro opponent is how one proves a statement beginning with ∀. To show that something holds for every opponent, take an arbitrary one, give it a name, and show it for that. Lean unfolds the definition to find the ∀ underneath, and the goal becomes:

opponent : Action
⊢ payoff cooperate opponent < payoff defect opponent

With the cursor on the cases line, the editor shows the same state. VS Code highlights opponent, marking what has changed since the previous tactic:

Something new has appeared above the turnstile. That is the context: the things we may now assume. We have an opponent's action, we know nothing about which one it is, and we must prove the inequality for it.

cases opponent uses the fact that Action was declared with exactly two constructors. There are only two ways an action can have come about, so it suffices to handle both, and the single goal becomes two:

case cooperate
⊢ payoff cooperate cooperate < payoff defect cooperate

case defect
⊢ payoff cooperate defect < payoff defect defect

The opponent has disappeared from the context, replaced in each goal by the concrete action of that case. Note that the second goal is exactly the theorem we proved in chapter 3.

Each · then focuses on one goal, and inside it norm_num [payoff] finishes the arithmetic as before: 3 is less than 5, and 0 is less than 1.

The bullet · is typed \. and is not decoration. It tells Lean that the tactics indented under it address one goal only, which keeps a long proof honest about which branch it is in.

Both cases at once¶

When the branches are proved the same way, repeating ourselves is tedious:

/-- The same proof, with both cases handled by a single tactic. -/
example : StrictlyDominates payoff defect cooperate := by
  intro opponent
  cases opponent <;> norm_num [payoff]

The <;> combinator runs the tactic on its right against every goal produced by the tactic on its left. It is idiomatic Lean and worth recognising, though we write the cases out when they differ, or when we want the proof to be readable as an argument rather than compact.

Where we are¶

We have made the step from talking about particular actions to quantifying over all of them, which needed one new idea in the definition, Prop, and two in the proof, intro and cases.

We can now say what it means for one strategy to beat another. In chapter 5 we say what it means for a strategy to be a Nash equilibrium, and what it means for it to be evolutionarily stable.