A functional interpretation for nonstandard arithmetic

DOI10.1016/J.APAL.2012.07.003zbMATH Open1270.03121arXiv1109.3103OpenAlexW2593449741MaRDI QIDQ714729FDOQ714729

Benno van den Berg, Pavol Safarik, Eyvind Martol Briseid

Publication date: 11 October 2012

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Abstract: We introduce constructive and classical systems for nonstandard arithmetic and show how variants of the functional interpretations due to Goedel and Shoenfield can be used to rewrite proofs performed in these systems into standard ones. These functional interpretations show in particular that our nonstandard systems are conservative extensions of extensional Heyting and Peano arithmetic in all finite types, strengthening earlier results by Moerdijk, Palmgren, Avigad and Helzner. We will also indicate how our rewriting algorithm can be used for term extraction purposes. To conclude the paper, we will point out some open problems and directions for future research and mention some initial results on saturation principles.

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

Recommendations

• Nonstandardness and the bounded functional interpretation
• Nonstandard functional interpretations and categorical models
• Formalizing non-standard arguments in second-order arithmetic
• Intuitionistic nonstandard bounded modified realisability and functional interpretation
• Interpreting weak Kőnig's lemma in theories of nonstandard arithmetic

zbMATH Keywords

proof theoryfunctional interpretationsnonstandard arithmeticrewriting algorithmsaturation principlesterm extraction

Mathematics Subject Classification ID

Metamathematics of constructive systems (03F50) Nonstandard models of arithmetic (03H15) Functionals in proof theory (03F10)

Cites Work

• A quantitative mean ergodic theorem for uniformly convex Banach spaces
• Title not available (Why is that?)
• Fixed points of asymptotic contractions
• Some logical metatheorems with applications in functional analysis
• A quadratic rate of asymptotic regularity for CAT(0)-spaces
• Nonstandard methods in fixed point theory
• Asymptotically nonexpansive mappings in uniformly convex hyperbolic spaces
• Local stability of ergodic averages
• Title not available (Why is that?)
• Factorization of the Shoenfield-like bounded functional interpretation
• Metamathematical problems
• General logical metatheorems for functional analysis
• Applied Proof Theory: Proof Interpretations and Their Use in Mathematics
• Constructivism in mathematics. An introduction. Volume II
• Internal set theory: A new approach to nonstandard analysis
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Shoenfield is Gödel after Krivine
• Classical logic, continuation semantics and abstract machines
• Intuitionistische Untersuchungen der formalistischen Logik
• Opérateurs de mise en mémoire et traduction de Gödel. (Storage operators and Gödel translation)
• The syntax of nonstandard analysis
• A model for intuitionistic non-standard arithmetic
• Minimal models of Heyting arithmetic
• On quantitative versions of theorems due to F. E. Browder and R. Wittmann
• Mann iterates of directionally nonexpansive mappings in hyperbolic spaces
• A quantitative nonlinear strong ergodic theorem for Hilbert spaces
• Some computational aspects of metric fixed-point theory
• Bounded functional interpretation
• Eine Variante zur Dialectica-Interpretation der Heyting-Arithmetik endlicher Typen
• Bounded modified realizability
• A simple proof of the ergodic theorem using nonstandard analysis
• On the strength of nonstandard analysis
• Developments in Constructive Nonstandard Analysis
• Uniform Heyting arithmetic
• Theory of models with generalized atomic formulas
• Computer Science Logic
• Title not available (Why is that?)
• The metamathematics of ergodic theory
• Injecting uniformities into Peano arithmetic
• Proof mining in topological dynamics
• Transfer principles in nonstandard intuitionistic arithmetic
• Title not available (Why is that?)
• Logical aspects of rates of convergence in metric spaces
• Title not available (Why is that?)
• An Effective Conservation Result for Nonstandard Arithmetic
• Title not available (Why is that?)
• The Herbrand topos
• A quantitative version of Kirk's fixed point theorem for asymptotic contractions

Cited In (35)

• Nonstandardness and the bounded functional interpretation
• A note on equality in finite‐type arithmetic
• THE CHARACTERIZATION OF WEIHRAUCH REDUCIBILITY IN SYSTEMS CONTAINING
• From Nonstandard Analysis to Various Flavours of Computability Theory
• Herbrandized modified realizability
• A herbrandized functional interpretation of classical first-order logic
• Refining the taming of the reverse mathematics zoo
• The strength of compactness in computability theory and nonstandard analysis
• Weyl and Intuitionistic Infinitesimals
• The Herbrand topos
• Saturation and Σ₂-transfer for ERNA
• Multi-level nonstandard analysis and the axiom of choice
• Reverse mathematics and parameter-free transfer
• On the Herbrand functional interpretation
• To be or not to be constructive, that is not the question
• Weak König's lemma in Herbrandized classical second-order arithmetic
• The FAN principle and weak König's lemma in Herbrandized second-order arithmetic
• THE HERBRAND FUNCTIONAL INTERPRETATION OF THE DOUBLE NEGATION SHIFT
• Transfer principles in nonstandard intuitionistic arithmetic
• Reverse formalism 16
• σ-algebras for quasirandom hypergraphs
• A parametrised functional interpretation of Heyting arithmetic
• Title not available (Why is that?)
• Erratum to ``Spacelike hypersurfaces of constant higher order mean curvature in generalized Robertson-Walker spacetimes.
• Interpreting weak Kőnig's lemma in theories of nonstandard arithmetic
• Formalizing non-standard arguments in second-order arithmetic
• Title not available (Why is that?)
• Hardwiring truth in functional interpretations
• COMPUTABILITY THEORY, NONSTANDARD ANALYSIS, AND THEIR CONNECTIONS
• Infinitesimal analysis without the axiom of choice
• Stateful Realizers for Nonstandard Analysis
• Intuitionistic nonstandard bounded modified realisability and functional interpretation
• The strength of countable saturation
• Proof mining and effective bounds in differential polynomial rings
• A note on non-classical nonstandard arithmetic

This page was built for publication: A functional interpretation for nonstandard arithmetic

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