Document Open Access Logo

Diller-Nahm Bar Recursion

Author Valentin Blot

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2023.32.pdf
  • Filesize: 0.59 MB
  • 16 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof theory
Keywords
  • Dialectica
  • Bar recursion

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

We present a generalization of Spector’s bar recursion to the Diller-Nahm variant of Gödel’s Dialectica interpretation. This generalized bar recursion collects witnesses of universal formulas in sets of approximation sequences to provide an interpretation to the double-negation shift principle. The interpretation is presented in a fully computational way, implementing sets via lists. We also present a demand-driven version of this extended bar recursion manipulating partial sequences rather than initial segments. We explain why in a Diller-Nahm context there seems to be several versions of this demand-driven bar recursion, but no canonical one.

Cite As Get BibTex

Valentin Blot. Diller-Nahm Bar Recursion. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 32:1-32:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.FSCD.2023.32

Author Details

Valentin Blot
  • Inria, Laboratoire Méthodes Formelles, Université Paris-Saclay, France

References

  1. Stefano Berardi, Marc Bezem, and Thierry Coquand. On the Computational Content of the Axiom of Choice. Journal of Symbolic Logic, 63(2):600-622, 1998. Google Scholar
  2. Justus Diller and Werner Nahm. Eine Variante zur Dialectica-Interpretation der Heyting-Arithmetik endlicher Typen. Archiv für mathematische Logik und Grundlagenforschung, 16:49-66, 1974. Google Scholar
  3. Martín Escardó and Paulo Oliva. The herbrand functional interpretation of the double negation shift. Journal of Symbolic Logic, 82(2):590-607, 2017. Google Scholar
  4. Harvey Friedman. Classically and intuitionistically provably recursive functions. In Gert Müller and Dana Scott, editors, Higher Set Theory, volume 669 of Lecture Notes in Mathematics, pages 21-27. Springer, 1978. Google Scholar
  5. Kurt Gödel. Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes. Dialectica, 12(3-4):280-287, 1958. Google Scholar
  6. Stephen Cole Kleene. On the Interpretation of Intuitionistic Number Theory. Journal of Symbolic Logic, 10(4):109-124, 1945. Google Scholar
  7. Georg Kreisel. Interpretation of analysis by means of constructive functionals of finite types. In Constructivity in mathematics: Proceedings of the colloquium held at Amsterdam, 1957, Studies in Logic and the Foundations of Mathematics, pages 101-128. North-Holland Publishing Company, 1959. Google Scholar
  8. Paulo Oliva and Thomas Powell. Bar recursion over finite partial functions. Annals of Pure and Applied Logic, 168(5):887-921, 2017. Google Scholar
  9. Pierre-Marie Pédrot. A functional functional interpretation. In Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014, pages 77:1-77:10. ACM, 2014. Google Scholar
  10. Pierre-Marie Pédrot. A Materialist Dialectica. (Une Dialectica matérialiste). PhD thesis, Paris Diderot University, France, 2015. Google Scholar
  11. Clifford Spector. Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles in current intuitionistic mathematics. In Recursive Function Theory: Proceedings of Symposia in Pure Mathematics, volume 5, pages 1-27. American Mathematical Society, 1962. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact