A constructive analysis of learning in Peano arithmetic (Q450942): Difference between revisions
From MaRDI portal
Added link to MaRDI item. |
Removed claim: reviewed by (P1447): Item:Q454365 |
||
| Property / reviewed by | |||
| Property / reviewed by: Grigori Mints / rank | |||
Revision as of 11:35, 15 February 2024
scientific article
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | A constructive analysis of learning in Peano arithmetic |
scientific article |
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
