A constructive analysis of learning in Peano arithmetic

DOI10.1016/j.apal.2011.12.004zbMath1257.03083MaRDI QIDQ450942

Federico Aschieri

Publication date: 26 September 2012

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

Full work available at URL: https://doi.org/10.1016/j.apal.2011.12.004

zbMATH Keywords

halting problem; oracle; primitive recursive functionals; classical arithmetic; constructive termination proof; epsilon substitution method; learning-based realizability; update procedures

Mathematics Subject Classification ID

03F30: First-order arithmetic and fragments

03F03: Proof theory in general (including proof-theoretic semantics)

03F55: Intuitionistic mathematics

Related Items

Constructive forcing, CPS translations and witness extraction in Interactive realizability, Interactive Realizability for second-order Heyting arithmetic with EM1 and SK1, Fluctuations, effective learnability and metastability in analysis

Cites Work

• Lectures on the Curry-Howard isomorphism
• Epsilon substitution method for elementary analysis
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Interactive Learning-Based Realizability for Heyting Arithmetic with EM1
• On bar recursion of types 0 and 1
• Classical logic as limit completion
• Applied Proof Theory: Proof Interpretations and Their Use in Mathematics
• New Computational Paradigms
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item