An independence result for \((\Pi^ 1_ 1-CA)+BI\) (Q1097882): Difference between revisions
From MaRDI portal
Set profile property. |
Set OpenAlex properties. |
||
| Property / OpenAlex ID | |||
| Property / OpenAlex ID: W2084179139 / rank | |||
Normal rank | |||
Revision as of 22:17, 19 March 2024
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
