An independence result for \((\Pi^ 1_ 1-CA)+BI\)
This paper meets a combinatorial problem by modern means of proof theory, which can be clothed in the legend of Hercules and the Hydra: A hydr AB This paper meets a combinatorial problem by modern means of proof theory, which can be clothed in the legend of Hercules and the Hydra: A hydra is a finite tree, each node of which is labelled by some element of the set \(\{+\} \cup (\omega + 1)\). Cutting a head ( = leaf of the tree) of the hydra is defined in such a way that from stroke to stroke the beast seems to increase. But surprisingly, it can be proven.
scientific article; zbMATH DE number 4035824