A functional interpretation for nonstandard arithmetic

DOI10.1016/J.APAL.2012.07.003MaRDI QIDQ714729zbMATH OpenOpenAlexFDO

Authors Benno van den Berg, Eyvind Martol Briseid, Pavol Safarik

Publication date 11 October 2012

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

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

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)

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.

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

Cites work

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

Cited in

(37)

• Stateful Realizers for Nonstandard Analysis
• Reverse mathematics and parameter-free transfer
• A herbrandized functional interpretation of classical first-order logic
• The strength of compactness in computability theory and nonstandard analysis
• Hardwiring truth in functional interpretations
• Computability theory, nonstandard analysis, and their connections
• On the Herbrand functional interpretation
• Formalizing non-standard arguments in second-order arithmetic
• Infinitesimal analysis without the axiom of choice
• The strength of countable saturation
• Proof mining and effective bounds in differential polynomial rings
• Reverse formalism 16
• Transfer principles in nonstandard intuitionistic arithmetic
• Saturation and Σ₂-transfer for ERNA
• Erratum to ``Spacelike hypersurfaces of constant higher order mean curvature in generalized Robertson-Walker spacetimes.
• To be or not to be constructive, that is not the question
• Nonstandardness and the bounded functional interpretation
• Weyl and Intuitionistic Infinitesimals
• Refining the taming of the reverse mathematics zoo
• Herbrandized modified realizability
• A parametrised functional interpretation of Heyting arithmetic
• A note on equality in finite‐type arithmetic
• A note on non-classical nonstandard arithmetic
• Injecting uniformities into Peano arithmetic
• Interpreting weak Kőnig's lemma in theories of nonstandard arithmetic
• Multi-level nonstandard analysis and the axiom of choice
• From nonstandard analysis to various flavours of computability theory
• Nonstandard functional interpretations and categorical models
• The Herbrand functional interpretation of the double negation shift
• The computational content of nonstandard analysis
• THE CHARACTERIZATION OF WEIHRAUCH REDUCIBILITY IN SYSTEMS CONTAINING
• The Herbrand topos
• scientific article; zbMATH DE number 2236625 (Why is no real title available?)
• 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
• Intuitionistic nonstandard bounded modified realisability and functional interpretation
• σ-algebras for quasirandom hypergraphs

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)