An independence result for \((\Pi^ 1_ 1-CA)+BI\) (Q1097882): Difference between revisions
From MaRDI portal
Set OpenAlex properties. |
ReferenceBot (talk | contribs) Changed an Item |
||
| Property / cites work | |||
| Property / cites work: Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies / rank | |||
Normal rank | |||
| Property / cites work | |||
| Property / cites work: A Short Proof of Two Recently Discovered Independence Results Using Recursion Theoretic Methods / rank | |||
Normal rank | |||
| Property / cites work | |||
| Property / cites work: Rapidly growing Ramsey functions / rank | |||
Normal rank | |||
| Property / cites work | |||
| Property / cites work: Accessible Independence Results for Peano Arithmetic / rank | |||
Normal rank | |||
| Property / cites work | |||
| Property / cites work: Built-up systems of fundamental sequences and hierarchies of number-theoretic functions / rank | |||
Normal rank | |||
| Property / cites work | |||
| Property / cites work: Q5605873 / rank | |||
Normal rank | |||
Latest revision as of 14:45, 18 June 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
0 references
0 references
0 references
