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 arithmeticconservationfinite type extensionPRAweak König's lemmaWKL

Mathematics Subject Classification ID

Functionals in proof theory (03F10) Second- and higher-order arithmetic and fragments (03F35) Metamathematics of constructive systems (03F50) Relative consistency and interpretations (03F25) Higher-type and set recursion theory (03D65)

Related Items (12)

Reverse mathematics and parameter-free transfer ⋮ Betwixt Turing and Kleene ⋮ Term extraction and Ramsey's theorem for pairs ⋮ Banach’s theorem in higher-order reverse mathematics ⋮ To be or not to be constructive, that is not the question ⋮ A note on non-classical nonstandard arithmetic ⋮ Bounded functional interpretation ⋮ COMPUTABILITY THEORY, NONSTANDARD ANALYSIS, AND THEIR CONNECTIONS ⋮ Effective Choice and Boundedness Principles in Computable Analysis ⋮ Bounded modified realizability ⋮ The strength of compactness in computability theory and nonstandard analysis ⋮ Classical provability of uniform versions and intuitionistic provability

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

This page was built for publication: On uniform weak König's lemma