A constructive analysis of learning in Peano arithmetic (Q450942): Difference between revisions
From MaRDI portal
m rollbackEdits.php mass rollback Tag: Rollback |
Set OpenAlex properties. |
||
| Property / full work available at URL | |||
| Property / full work available at URL: https://doi.org/10.1016/j.apal.2011.12.004 / rank | |||
Normal rank | |||
| Property / OpenAlex ID | |||
| Property / OpenAlex ID: W2016104854 / rank | |||
Normal rank | |||
Revision as of 17:29, 19 March 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
