EconCSLib.GameTheory.ExtensiveGame.Zermelo

Zermelo-style finite game results as two-player zero-sum consequences of backward induction and Kuhn's theorem.

Zermelo (1913) established determinacy for finite perfect-information two-player win/loss/draw games (Chess, in his original paper). Here we frame it as the special case of Kuhn's theorem where:

• N = Fin 2 — exactly two players,
• payoffs are in ℚ (any [LinearOrderedField U] would do),
• the game is zero-sum: payoff leaf 0 + payoff leaf 1 = 0 at every leaf.

Main definitions

• GameTree.IsZeroSum — the zero-sum predicate on a GameTree (Fin 2) ℚ
• GameTree.value₀ — the value of the game for Player 0.

Main results

• zermelo_determinacy — determinacy / saddle value: in a finite two-player zero-sum perfect-information game, optStrategy is a saddle point with value value₀ g. Player 0, by playing optStrategy, secures at least value₀ g against every opponent play; player 1, by playing optStrategy, holds player 0 to at most value₀ g. This is the genuine Zermelo content (the value is determined and both players have a pure optimal strategy).
• IsZeroSum.of_subtree — zero-sumness is inherited by every subgame.
• outcome_zero_sum — every strategy's terminal outcome is zero-sum in a zero-sum tree.
• value_zero_sum — backward induction preserves the zero-sum value invariant.
• value_one_eq_neg_value₀ — player 1's backward-induction value is the negative of player 0's value.
• value₀_Node_zero_isMax / value₀_Node_one_isMin — the local max/min behavior of the zero-sum value at player-0 and player-1 nodes.
• value₀_eq_outcome_and_zeroSum — optStrategy realizes the player-0 value and the value vector is zero-sum (packaging lemma; the saddle statement is zermelo_determinacy).
• zermelo_exists_pure_SPE / zermelo_exists_pure_NE — the Fin 2 / ℚ instances of Kuhn's existence theorem. Existence needs no zero-sum hypothesis; the zero-sum refinement is zermelo_determinacy.

References

• [Zermelo 1913] Über eine Anwendung der Mengenlehre auf die Theorie des Schachspiels, Proceedings of the Fifth International Congress of Mathematicians
• [MSZ] Maschler, Solan, Zamir, Game Theory, §3.6

Zero-sum condition

@[irreducible]

def GameTree.IsZeroSum : GameTree (Fin 2) ℚ → Prop

A 2-player GameTree valued in ℚ is zero-sum if at every leaf the two players' payoffs sum to zero.

Equations

• (GameTree.Leaf p).IsZeroSum = (p 0 + p 1 = 0)
• (GameTree.Node mover h t).IsZeroSum = (h.IsZeroSum ∧ ∀ c ∈ t, c.IsZeroSum)

theorem GameTree.IsZeroSum.head {m : Fin 2} {h : GameTree (Fin 2) ℚ} {t : List (GameTree (Fin 2) ℚ)} (hzs : (Node m h t).IsZeroSum) : h.IsZeroSum

The head child of a zero-sum node is zero-sum.

theorem GameTree.IsZeroSum.tail_mem {m : Fin 2} {h : GameTree (Fin 2) ℚ} {t : List (GameTree (Fin 2) ℚ)} {c : GameTree (Fin 2) ℚ} (hzs : (Node m h t).IsZeroSum) (hmem : c ∈ t) : c.IsZeroSum

Every tail child of a zero-sum node is zero-sum.

theorem GameTree.IsZeroSum.child_mem {m : Fin 2} {h : GameTree (Fin 2) ℚ} {t : List (GameTree (Fin 2) ℚ)} {c : GameTree (Fin 2) ℚ} (hzs : (Node m h t).IsZeroSum) (hmem : c ∈ h :: t) : c.IsZeroSum

Every child of a zero-sum node is zero-sum.

theorem GameTree.IsZeroSum.of_subtree {s g : GameTree (Fin 2) ℚ} (hzs : g.IsZeroSum) (hsub : s.Subtree g) : s.IsZeroSum

Zero-sumness is inherited by subgames.

Existence (instances of Kuhn's theorem)

Existence of a pure SPE / Nash equilibrium is Kuhn's theorem; it holds for any finite perfect-information game and does not use the zero-sum hypothesis. These two declarations are just the Fin 2 / ℚ instances, kept as named entry points. The genuinely zero-sum result — that the game has a determined value realized by a saddle point — is zermelo_determinacy below.

theorem GameTree.zermelo_exists_pure_SPE (g : GameTree (Fin 2) ℚ) : ∃ (σ : Strategy (Fin 2) ℚ), IsSubgamePerfectOn σ g

Pure root-scoped subgame-perfect existence for a finite two-player game on ℚ: the Fin 2 / ℚ instance of Kuhn_exists_SPE_on. Zero-sum is not needed for existence; see zermelo_determinacy for the zero-sum refinement.

theorem GameTree.zermelo_exists_pure_NE (g : GameTree (Fin 2) ℚ) : ∃ (σ : Strategy (Fin 2) ℚ), IsNashEquilibrium σ g

Pure root Nash existence for a finite two-player game on ℚ: the Fin 2 / ℚ instance of Kuhn_exists_NE. Zero-sum is not needed.

Backward-induction value in zero-sum games

def GameTree.value₀ (g : GameTree (Fin 2) ℚ) : ℚ

Minimax value for player 0 in a two-player zero-sum game.

Under zero-sum, this fully determines both players' values (player 1's value = -value₀).

Equations

• g.value₀ = g.value 0

theorem GameTree.value₀_Leaf (p : Fin 2 → ℚ) (_h : (Leaf p).IsZeroSum) : (Leaf p).value₀ = p 0

At a zero-sum leaf, value₀ equals player 0's payoff and -value₀ equals player 1's.

theorem GameTree.value_zero_sum (g : GameTree (Fin 2) ℚ) (hzs : g.IsZeroSum) : g.value 0 + g.value 1 = 0

Backward induction preserves the zero-sum invariant: if every terminal payoff vector is zero-sum, then the selected backward-induction value vector is zero-sum as well.

theorem GameTree.value_one_eq_neg_value₀ (g : GameTree (Fin 2) ℚ) (hzs : g.IsZeroSum) : g.value 1 = -g.value₀

In a zero-sum game, player 1's backward-induction value is determined by player 0's value.

Local max-min structure

theorem GameTree.value₀_Node_eq_some_child (m : Fin 2) (h : GameTree (Fin 2) ℚ) (t : List (GameTree (Fin 2) ℚ)) : ∃ c ∈ h :: t, (Node m h t).value₀ = c.value₀

At any decision node, the backward-induction value₀ is realized by one of the node's children.

theorem GameTree.value₀_Node_zero_ge_child (h : GameTree (Fin 2) ℚ) (t : List (GameTree (Fin 2) ℚ)) (c : GameTree (Fin 2) ℚ) (hmem : c ∈ h :: t) : c.value₀ ≤ (Node 0 h t).value₀

At a player-0 node, value₀ is at least the value₀ of every child.

theorem GameTree.value₀_Node_one_le_child (h : GameTree (Fin 2) ℚ) (t : List (GameTree (Fin 2) ℚ)) (hzs : (Node 1 h t).IsZeroSum) (c : GameTree (Fin 2) ℚ) (hmem : c ∈ h :: t) : (Node 1 h t).value₀ ≤ c.value₀

At a zero-sum player-1 node, value₀ is no greater than the value₀ of every child. Equivalently, player 1's local maximization of their own value is player 0's local minimization.

theorem GameTree.value₀_Node_zero_isMax (h : GameTree (Fin 2) ℚ) (t : List (GameTree (Fin 2) ℚ)) : ∃ c ∈ h :: t, (Node 0 h t).value₀ = c.value₀ ∧ ∀ d ∈ h :: t, d.value₀ ≤ c.value₀

At a player-0 node, some child realizes the node's value₀, and that value is at least every child's value₀.

theorem GameTree.value₀_Node_one_isMin (h : GameTree (Fin 2) ℚ) (t : List (GameTree (Fin 2) ℚ)) (hzs : (Node 1 h t).IsZeroSum) : ∃ c ∈ h :: t, (Node 1 h t).value₀ = c.value₀ ∧ ∀ d ∈ h :: t, c.value₀ ≤ d.value₀

At a zero-sum player-1 node, some child realizes the node's value₀, and that value is no greater than every child's value₀.

Backward-induction outcome in zero-sum games

theorem GameTree.outcome_zero_sum (σ : Strategy (Fin 2) ℚ) (g : GameTree (Fin 2) ℚ) (hzs : g.IsZeroSum) : outcome σ g 0 + outcome σ g 1 = 0

In a zero-sum tree, the terminal outcome of any strategy is zero-sum: following any strategy ends at some leaf, and every leaf of a zero-sum tree is zero-sum. This is the strategy-level analogue of value_zero_sum.

theorem GameTree.outcome_optStrategy_zero_sum (g : GameTree (Fin 2) ℚ) (hzs : g.IsZeroSum) : outcome optStrategy g 0 + outcome optStrategy g 1 = 0

The terminal outcome reached by the backward-induction strategy is zero-sum whenever the game tree is zero-sum.

theorem GameTree.outcome_optStrategy_one_eq_neg_value₀ (g : GameTree (Fin 2) ℚ) (hzs : g.IsZeroSum) : outcome optStrategy g 1 = -g.value₀

In a zero-sum game, the backward-induction outcome for player 1 is the negative of player 0's backward-induction value.

Value realization

theorem GameTree.value₀_eq_optStrategy_outcome (g : GameTree (Fin 2) ℚ) : g.value₀ = outcome optStrategy g 0

The backward-induction strategy realizes value₀ for player 0.

theorem GameTree.value₀_eq_outcome_and_zeroSum (g : GameTree (Fin 2) ℚ) (hzs : g.IsZeroSum) : g.value₀ = outcome optStrategy g 0 ∧ g.value 1 = -g.value₀

Packaging lemma: the backward-induction strategy realizes player 0's value, and the value vector is zero-sum. This is not the minimax statement — it has no quantification over opponent strategies. The genuine saddle / security statement is zermelo_determinacy.

Determinacy (the saddle value)

The genuine Zermelo content. Combining subgame perfection of optStrategy (optStrategy_isSubgamePerfect) with the zero-sum invariant gives a saddle point: value₀ g is simultaneously what player 0 can secure and what player 1 can hold player 0 to.

theorem GameTree.value₀_le_outcome_of_iVariant_one (g : GameTree (Fin 2) ℚ) (hzs : g.IsZeroSum) {σ' : Strategy (Fin 2) ℚ} (hiv : IVariant 1 optStrategy σ') : g.value₀ ≤ outcome σ' g 0

Player 0's security. If player 0 plays optStrategy (so the deviating profile σ' is a 1-variant, leaving player 0's choices fixed), then player 0's payoff is at least value₀ g against every play of player 1.

Proof: subgame perfection at player 1 caps outcome σ' g 1 ≤ value g 1 = -value₀ g; the zero-sum identity outcome σ' g 0 = -outcome σ' g 1 then forces outcome σ' g 0 ≥ value₀ g.

theorem GameTree.outcome_le_value₀_of_iVariant_zero (g : GameTree (Fin 2) ℚ) {σ' : Strategy (Fin 2) ℚ} (hiv : IVariant 0 optStrategy σ') : outcome σ' g 0 ≤ g.value₀

Player 1's security. If player 1 plays optStrategy (so σ' is a 0-variant, leaving player 1's choices fixed), then player 0's payoff is at most value₀ g against every play of player 0. Immediate from subgame perfection at player 0; no zero-sum hypothesis is needed for this direction.

theorem GameTree.zermelo_determinacy (g : GameTree (Fin 2) ℚ) (hzs : g.IsZeroSum) : (∀ (σ' : Strategy (Fin 2) ℚ), IVariant 1 optStrategy σ' → g.value₀ ≤ outcome σ' g 0) ∧ ∀ (σ' : Strategy (Fin 2) ℚ), IVariant 0 optStrategy σ' → outcome σ' g 0 ≤ g.value₀

Zermelo's theorem (determinacy / saddle value). In a finite two-player zero-sum perfect-information game, optStrategy is a saddle point with value value₀ g:

• playing optStrategy, player 0 secures at least value₀ g against every opponent play (1-variant);
• playing optStrategy, player 1 holds player 0 to at most value₀ g against every opponent play (0-variant).

Hence the game is determined and value₀ g is its value, attained by the pure backward-induction strategy on both sides.