An independence result for \((\Pi^ 1_ 1-CA)+BI\) (Q1097882)
From MaRDI portal
scientific article
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | An independence result for \((\Pi^ 1_ 1-CA)+BI\) |
scientific article |
Statements
An independence result for \((\Pi^ 1_ 1-CA)+BI\) (English)
0 references
1987
0 references
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.
0 references
proof theory
0 references
Hercules
0 references
Hydra
0 references
finite tree
0 references
wellfounded trees
0 references
0 references
0 references
0 references
