A constructive analysis of learning in Peano arithmetic (Q450942): Difference between revisions

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

zbMATH Keywords

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

reviewed by

Grigori Mints

0 references

MaRDI profile type

MaRDI publication profile

0 references

full work available at URL

https://doi.org/10.1016/j.apal.2011.12.004

0 references

cites work

Interactive Learning-Based Realizability for Heyting Arithmetic with EM1

0 references

Q2776806

0 references

Classical logic as limit completion

0 references

New Computational Paradigms

0 references

Q3994895

0 references

Q4218534

0 references

Applied Proof Theory: Proof Interpretations and Their Use in Mathematics

0 references

Epsilon substitution method for elementary analysis

0 references

Q4360861

0 references

On bar recursion of types 0 and 1

0 references

Lectures on the Curry-Howard isomorphism

0 references

Q5635418

0 references

Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard

0 references

Identifiers

zbMATH Open document ID

1257.03083

0 references

Mathematics Subject Classification ID

0 references

0 references

0 references

0 references

0 references

10.1016/J.APAL.2011.12.004

0 references

Sitelinks

Mathematics(1 entry)

mardi Publication:450942

@@ Property / DOI @@
-.1016/j.apal.2011.12.004
@@ Property / DOI: 10.1016/j.apal.2011.12.004 / rank @@
-Normal rank
@@ Property / 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.
+Normal rank
@@ Property / Mathematics Subject Classification ID @@
+F03
@@ Property / Mathematics Subject Classification ID: 03F03 / rank @@
+Normal rank
@@ Property / Mathematics Subject Classification ID @@
+F30
@@ Property / Mathematics Subject Classification ID: 03F30 / rank @@
+Normal rank
@@ Property / Mathematics Subject Classification ID @@
+F55
@@ Property / Mathematics Subject Classification ID: 03F55 / rank @@
+Normal rank
@@ Property / zbMATH DE Number @@
+6086890
@@ Property / zbMATH DE Number: 6086890 / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+learning-based realizability
@@ Property / zbMATH Keywords: learning-based realizability / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+classical arithmetic
@@ Property / zbMATH Keywords: classical arithmetic / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+update procedures
@@ Property / zbMATH Keywords: update procedures / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+epsilon substitution method
@@ Property / zbMATH Keywords: epsilon substitution method / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+constructive termination proof
@@ Property / zbMATH Keywords: constructive termination proof / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+primitive recursive functionals
@@ Property / zbMATH Keywords: primitive recursive functionals / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+oracle
@@ Property / zbMATH Keywords: oracle / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+halting problem
@@ Property / zbMATH Keywords: halting problem / rank @@
+Normal rank
@@ Property / reviewed by @@
+Grigori Mints
@@ Property / reviewed by: Grigori Mints / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1016/j.apal.2011.12.004
+Normal rank
@@ Property / OpenAlex ID @@
+W2016104854
@@ Property / OpenAlex ID: W2016104854 / rank @@
+Normal rank
@@ Property / cites work @@
+Interactive Learning-Based Realizability for Heyting Arithmetic with EM1
+Normal rank
@@ Property / cites work @@
+Q2776806
@@ Property / cites work: Q2776806 / rank @@
+Normal rank
@@ Property / cites work @@
+Classical logic as limit completion
@@ Property / cites work: Classical logic as limit completion / rank @@
+Normal rank
@@ Property / cites work @@
+New Computational Paradigms
@@ Property / cites work: New Computational Paradigms / rank @@
+Normal rank
@@ Property / cites work @@
+Q3994895
@@ Property / cites work: Q3994895 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4218534
@@ Property / cites work: Q4218534 / rank @@
+Normal rank
@@ Property / cites work @@
+Applied Proof Theory: Proof Interpretations and Their Use in Mathematics
+Normal rank
@@ Property / cites work @@
+Epsilon substitution method for elementary analysis
+Normal rank
@@ Property / cites work @@
+Q4360861
@@ Property / cites work: Q4360861 / rank @@
+Normal rank
@@ Property / cites work @@
+On bar recursion of types 0 and 1
@@ Property / cites work: On bar recursion of types 0 and 1 / rank @@
+Normal rank
@@ Property / cites work @@
+Lectures on the Curry-Howard isomorphism
@@ Property / cites work: Lectures on the Curry-Howard isomorphism / rank @@
+Normal rank
@@ Property / cites work @@
+Q5635418
@@ Property / cites work: Q5635418 / rank @@
+Normal rank
@@ Property / cites work @@
+Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
+Normal rank
@@ Property / DOI @@
+.1016/J.APAL.2011.12.004
@@ Property / DOI: 10.1016/J.APAL.2011.12.004 / rank @@
+Normal rank
@@ links / mardi / name / links / mardi / name @@
+Publication:450942