A constructive analysis of learning in Peano arithmetic
type: Item
instance of: scholarly article
title: A constructive analysis of learning in Peano arithmetic
zbMATH Open document ID: 1257.03083
author: Federico Aschieri
published in: Annals of Pure and Applied Logic
publication date: 2012-09-26T00:00:00Z
review text: The paper analyses Gödel primitive recursive functionals over an oracle for the halting problem. The goal is to treat intuitionistic arithmetic HA plus the law of excluded middle for existential formulas \(\mathrm{HA}+\mathrm{EM}_1\). A combination of the no-counterexample interpretation with continuity of Gödel primitive recursive functionals is used. This is rather intuitive for Kleene primitive recursive functionals but becomes more complicated in general. A termination proof for the epsilon-substitution method following \textit{J. Avigad} [Math. Log. Q. 48, No. 1, 3--13 (2002; Zbl 0988.03087)] is presented.
Mathematics Subject Classification ID: 03F03
Mathematics Subject Classification ID: 03F30
Mathematics Subject Classification ID: 03F55
zbMATH DE Number: 6086890
zbMATH Keywords: learning-based realizability
zbMATH Keywords: classical arithmetic
zbMATH Keywords: update procedures
zbMATH Keywords: epsilon substitution method
zbMATH Keywords: constructive termination proof
zbMATH Keywords: primitive recursive functionals
zbMATH Keywords: oracle
zbMATH Keywords: halting problem
reviewed by: G. E. Mints
MaRDI profile type: Publication
full work available at URL: j.apal.2011.12.004
OpenAlex ID: W2016104854
cites work: Interactive learning-based realizability for Heyting arithmetic with \(\mathrm{EM}_1\)
cites work: Update procedures and the 1-consistency of arithmetic
cites work: Classical logic as limit completion
cites work: New Computational Paradigms
cites work: Q3994895
cites work: Q4218534
cites work: Applied Proof Theory: Proof Interpretations and Their Use in Mathematics
cites work: Epsilon substitution method for elementary analysis
cites work: Q4360861
cites work: On bar recursion of types 0 and 1
cites work: Lectures on the Curry-Howard isomorphism
cites work: Q5635418
cites work: Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
DOI: 10.1016/J.APAL.2011.12.004
description: scientific article; zbMATH DE number 6086890