A functional interpretation for nonstandard arithmetic

DOI10.1016/j.apal.2012.07.003zbMath1270.03121arXiv1109.3103OpenAlexW2593449741MaRDI QIDQ714729

Benno van den Berg, Pavol Safarik, Eyvind Briseid

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

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

Related Items

Refining the taming of the reverse mathematics zoo, Reverse mathematics and parameter-free transfer, A parametrised functional interpretation of Heyting arithmetic, A herbrandized functional interpretation of classical first-order logic, The strength of countable saturation, Infinitesimal analysis without the axiom of choice, Hardwiring truth in functional interpretations, σ-algebras for quasirandom hypergraphs, To be or not to be constructive, that is not the question, Interpreting weak Kőnig's lemma in theories of nonstandard arithmetic, A note on equality in finite‐type arithmetic, Stateful Realizers for Nonstandard Analysis, The FAN principle and weak König's lemma in Herbrandized second-order arithmetic, On the Herbrand functional interpretation, Intuitionistic nonstandard bounded modified realisability and functional interpretation, Unnamed Item, Proof mining and effective bounds in differential polynomial rings, A note on non-classical nonstandard arithmetic, From Nonstandard Analysis to Various Flavours of Computability Theory, Weyl and Intuitionistic Infinitesimals, The Herbrand topos, The Herbrand topos, COMPUTABILITY THEORY, NONSTANDARD ANALYSIS, AND THEIR CONNECTIONS, Weak König's lemma in Herbrandized classical second-order arithmetic, Reverse formalism 16, THE HERBRAND FUNCTIONAL INTERPRETATION OF THE DOUBLE NEGATION SHIFT, The strength of compactness in computability theory and nonstandard analysis, THE CHARACTERIZATION OF WEIHRAUCH REDUCIBILITY IN SYSTEMS CONTAINING, Nonstandardness and the bounded functional interpretation

Cites Work

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