On uniform weak König's lemma

DOI10.1016/S0168-0072(01)00077-XzbMath1001.03052WikidataQ124916860 ScholiaQ124916860MaRDI QIDQ5957854

Ulrich Kohlenbach

Publication date: 2 June 2002

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

zbMATH Keywords

primitive recursive arithmetic; conservation; finite type extension; PRA; weak König's lemma; WKL

Mathematics Subject Classification ID

03F10: Functionals in proof theory

03F35: Second- and higher-order arithmetic and fragments

03F50: Metamathematics of constructive systems

03F25: Relative consistency and interpretations

03D65: Higher-type and set recursion theory

Related Items

Classical provability of uniform versions and intuitionistic provability, Bounded modified realizability, Bounded functional interpretation, Term extraction and Ramsey's theorem for pairs, Effective Choice and Boundedness Principles in Computable Analysis

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Fragments of arithmetic
• Recursion on the countable functionals
• Handbook of proof theory
• Mathematically strong subsystems of analysis with low rate of growth of provably recursive functionals
• Remarks on Herbrand normal forms and Herbrand realizations
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Extensional Gödel functional interpretation. A consistency proof of classical analysis
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
• Hilbert's program relativized; Proof-theoretical and foundational reductions
• Effective bounds from ineffective proofs in analysis: An application of functional interpretation and majorization
• Note on the fan theorem
• Some models for intuitionistic finite type arithmetic with fan functional
• Relative constructivity
• On effectively discontinuous type-2 objects
• A note on Spector's quantifier-free rule of extensionality