Program extraction for 2-random reals

DOI10.1007/s00153-013-0336-9zbMath1295.03039OpenAlexW2021119129MaRDI QIDQ365682

Alexander P. Kreuzer

Publication date: 9 September 2013

Published in: Archive for Mathematical Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00153-013-0336-9

zbMATH Keywords

program extractionconservationproof mining2-random realsweak weak König's lemma

Mathematics Subject Classification ID

Foundations of classical theories (including reverse mathematics) (03B30) Functionals in proof theory (03F10) Second- and higher-order arithmetic and fragments (03F35)

Cites Work

• Unnamed Item
• Primitive recursion and the chain antichain principle
• \(\varPi^1_1\)-conservation of combinatorial principles weaker than Ramsey's theorem for pairs
• Algorithmic randomness, reverse mathematics, and the dominated convergence theorem
• Elimination of Skolem functions for monotone formulas in analysis
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Measure theory and weak König's lemma
• Term extraction and Ramsey's theorem for pairs
• Algorithmic Randomness and Complexity
• Random reals, the rainbow Ramsey theorem, and arithmetic conservation
• Applied Proof Theory: Proof Interpretations and Their Use in Mathematics

This page was built for publication: Program extraction for 2-random reals