A constructive analysis of learning in Peano arithmetic (Q450942)
From MaRDI portal
 | This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use this page instead for the normal view: A constructive analysis of learning in Peano arithmetic |
scientific article; zbMATH DE number 6086890
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | A constructive analysis of learning in Peano arithmetic |
scientific article; zbMATH DE number 6086890 |
Statements
A constructive analysis of learning in Peano arithmetic (English)
0 references
26 September 2012
0 references
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.
0 references
learning-based realizability
0 references
classical arithmetic
0 references
update procedures
0 references
epsilon substitution method
0 references
constructive termination proof
0 references
primitive recursive functionals
0 references
oracle
0 references
halting problem
0 references
