A functional interpretation for nonstandard arithmetic

DOI10.1016/j.apal.2012.07.003zbMath1270.03121arXiv1109.3103MaRDI 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 theory; functional interpretations; nonstandard arithmetic; rewriting algorithm; saturation principles; term extraction

Mathematics Subject Classification ID

03H15: Nonstandard models of arithmetic

03F10: Functionals in proof theory

03F50: Metamathematics of constructive systems

Related Items

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

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