click a head to chop — Kirby-Paris Hydra Game
Step: 0 Heads: 5 Nodes: 13 λ: ω
Kirby-Paris Hydra Game — every finite hydra eventually dies. Hercules always wins.
Unprovable in Peano Arithmetic — requires ε₀ induction. The number of steps grows faster than any computable function.
Chop a head → the tree grows bigger before it shrinks. That's the point.
∎ The Proof

Assign each node an ordinal: leaves = 0, internal = sum of ω^child_ordinal in descending order.

Each chop STRICTLY reduces the root's ordinal. Ordinals are well-ordered — no infinite descending chain exists.

∴ Every hydra eventually dies. Hercules always wins.

But Peano Arithmetic can't prove this. The proof requires induction up to ε₀ — the first fixed point of α → ωα.

This is actual independence logic. Goodstein 1944, Kirby-Paris 1982.