A constructive analysis of learning in Peano arithmetic (Q450942)

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.