On Spector's bar recursion

DOI10.1002/MALQ.201100106MaRDI QIDQ2910991zbMATH OpenOpenAlexFDO

Authors Paulo Oliva, Thomas Powell

Publication date 12 September 2012

Published in Mathematical Logic Quarterly (MLQ) (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1002/malq.201100106

zbMATH Keywords

selection functionsSpector's bar recursionT-definability

Mathematics Subject Classification ID

Structure of proofs (03F07) Functionals in proof theory (03F10) Relative consistency and interpretations (03F25)

Recommendations

• Bar recursion and products of selection functions
• Logical Approaches to Computational Barriers
• Bar recursion over finite partial functions
• Bar recursion is not computable via iteration
• Equivalence of bar recursors in the theory of functionals of finite type

Cites work

• Applied Proof Theory: Proof Interpretations and Their Use in Mathematics
• Extensional Gödel functional interpretation. A consistency proof of classical analysis
• scientific article; zbMATH DE number 3231083 (Why is no real title available?)
• scientific article; zbMATH DE number 3259893 (Why is no real title available?)
• scientific article; zbMATH DE number 3335898 (Why is no real title available?)
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• On bar recursion of types 0 and 1
• On the No-Counterexample Interpretation
• Ordinal analysis of simple cases of bar recursion
• Selection functions, bar recursion and backward induction
• Sequential games and optimal strategies
• Strongly majorizable functionals of finite type: A model for barrecursion containing discontinuous functionals
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES

Cited in

(16)

• Equivalence of bar recursors in the theory of functionals of finite type
• A coalgebraic view of bar recursion and bar induction
• A short note on Spector's proof of consistency of analysis
• System T and the product of selection functions
• Selection functions, bar recursion and backward induction
• The equivalence of bar recursion and open recursion
• A direct proof of Schwichtenberg's bar recursion closure theorem
• The Herbrand functional interpretation of the double negation shift
• scientific article; zbMATH DE number 7269245 (Why is no real title available?)
• scientific article; zbMATH DE number 7297814 (Why is no real title available?)
• Bar recursion over finite partial functions
• Bar recursion is not computable via iteration
• Bar recursion and products of selection functions
• Modified bar recursion
• Logical Approaches to Computational Barriers
• Diller-Nahm bar recursion

This page was built for publication: On Spector's bar recursion

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2910991)