A direct independence proof of Buchholz's Hydra Game on finite labeled trees (Q1128173)

We know that Heracles chops off all heads of any hideous Hydra; but this fact is very difficult, or even impossible, to prove. The authors show the impossibility with respect to Buchholz Hydras and ISN (= isolated number theory). Their strategy is as follows. To a proof of the contradiction in ISN is associated an ordinal diagram (by Takeuti), i.e. a tree, which the authors read as a Buchholz Hydra. The reduction of proofs corresponds to chopping off a head and the subsequent monstrous growth of the Hydra. And so, if ISN can prove Heracles' ultimate victory, it proves its own consistency. Their main task is to assign heights to new proofs. They introduce even more horrid Hydras, and, by a similar method, show that their deaths cannot be proved by the system with iterated inductive definitions. The story of ``Heracles and Hydra'' was retold by Kirby and Paris in 1982. Their Hydras are tame: heads grow in width but not in height. And, unprovability is in Peano Arithmetic, and the tool is indicators and model theory. Buchholz's Hydras grow in both directions, and their deaths cannot be proved even by \(\Pi^1_1\)-Comprension Axioms with Bar Induction (which is equivalent to ISN). But he showed it by using generalized Hardy hierarchy and an infinitary proof system.