An independence result for \((\Pi^ 1_ 1-CA)+BI\)

DOI10.1016/0168-0072(87)90078-9zbMath0636.03052OpenAlexW2084179139MaRDI QIDQ1097882

Wilfried Buchholz

Publication date: 1987

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://epub.ub.uni-muenchen.de/3842/1/buchholz_wilfried_3842.pdf

zbMATH Keywords

proof theoryfinite treeHerculesHydrawellfounded trees

Mathematics Subject Classification ID

Trees (05C05) Cut-elimination and normal-form theorems (03F05) Second- and higher-order arithmetic and fragments (03F35) Complexity of proofs (03F20)

Related Items

Equational derivation vs. computation ⋮ Note on a proof of the extended Kirby-Paris theorem on labelled finite trees ⋮ Ordinal notation systems corresponding to Friedman's linearized well-partial-orders with gap-condition ⋮ Generalizations of the Kruskal-Friedman theorems ⋮ A new proof-theoretic proof of the independence of Kirby-Paris' hydra theorem. ⋮ Natural well-orderings ⋮ Functorial Fast-Growing Hierarchies ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Beyond polynomials and Peano arithmetic -- automation of elementary and ordinal interpretations ⋮ A slow growing analogue to Buchholz' proof ⋮ Pointwise Transfinite Induction and a Miniaturized Predicativity ⋮ Die another day ⋮ Systems of iterated projective ordinal notations and combinatorial statements about binary labeled trees ⋮ Unnamed Item ⋮ Tiered Arithmetics ⋮ Inductive definitions over a predicative arithmetic ⋮ Variations on a theme by Weiermann

Cites Work

• Unnamed Item
• Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies
• Rapidly growing Ramsey functions
• Accessible Independence Results for Peano Arithmetic
• Built-up systems of fundamental sequences and hierarchies of number-theoretic functions
• A Short Proof of Two Recently Discovered Independence Results Using Recursion Theoretic Methods