A constructive analysis of learning in Peano arithmetic
From MaRDI portal
Publication:450942
DOI10.1016/j.apal.2011.12.004zbMath1257.03083MaRDI QIDQ450942
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
halting problem; oracle; primitive recursive functionals; classical arithmetic; constructive termination proof; epsilon substitution method; learning-based realizability; update procedures
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