Nonstandard functional interpretations and categorical models

DOI10.1215/00294527-3870348zbMATH Open1431.03081arXiv1402.0784OpenAlexW3104000888MaRDI QIDQ2013393FDOQ2013393

Authors: Amar Hadzihasanovic, Benno van den Berg 

Publication date: 17 August 2017

Published in: Notre Dame Journal of Formal Logic (Search for Journal in Brave)

Abstract: Recently, the second author, Briseid and Safarik introduced nonstandard Dialectica, a functional interpretation that is capable of eliminating instances of familiar principles of nonstandard arithmetic - including overspill, underspill, and generalisations to higher types - from proofs. We show that, under few metatheoretical assumptions, the properties of this interpretation are mirrored by first order logic in a constructive sheaf model of nonstandard arithmetic due to Moerdijk, later developed by Palmgren. In doing so, we also draw some new connections between nonstandard principles, and principles that are rejected by strict constructivism. Furthermore, we introduce a variant of the Diller-Nahm interpretion with two different kinds of quantifiers (with and without computational meaning), similar to Hernest's light Dialectica interpretation, and show that one can obtain nonstandard Dialectica from this by weakening the computational content of the existential quantifiers -- a process we call herbrandisation. We also define a constructive sheaf model mirroring this new functional interpretation and show that the process of herbrandisation has a clear meaning in terms of these sheaf models.

Full work available at URL: https://arxiv.org/abs/1402.0784

Recommendations

• A functional interpretation for nonstandard arithmetic
• Nonstandardness and the bounded functional interpretation
• Intuitionistic nonstandard bounded modified realisability and functional interpretation
• Transfer principles in nonstandard intuitionistic arithmetic
• Functional interpretations. From the Dialectica interpretation to interpretations of classical and constructive set theory

zbMATH Keywords

categorical logicconstructive mathematicsproof miningDialectica interpretationfunctional interpretationsnonstandard arithmetic

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Relative consistency and interpretations (03F25) Nonstandard models of arithmetic (03H15)

Cited In (5)

• A model for intuitionistic non-standard arithmetic
• To be or not to be constructive, that is not the question
• COMPUTABILITY THEORY, NONSTANDARD ANALYSIS, AND THEIR CONNECTIONS
• Stateful Realizers for Nonstandard Analysis
• A note on non-classical nonstandard arithmetic

This page was built for publication: Nonstandard functional interpretations and categorical models

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2013393)