Bounded functional interpretation

DOI10.1016/j.apal.2004.11.001zbMath1095.03060OpenAlexW2097978997MaRDI QIDQ2488269

Paulo Oliva, Fernando Ferreira

Publication date: 25 August 2005

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

Full work available at URL: https://doi.org/10.1016/j.apal.2004.11.001

zbMATH Keywords

Functional interpretationProof miningIntuitionismProof TheoryMajorizability

Mathematics Subject Classification ID

First-order arithmetic and fragments (03F30) Functionals in proof theory (03F10) Second- and higher-order arithmetic and fragments (03F35) Relative consistency and interpretations (03F25)

Related Items (38)

A NEW COMPUTATION OF THE Σ-ORDINAL OF KPω ⋮ Bounded functional interpretation and feasible analysis ⋮ A parametrised functional interpretation of Heyting arithmetic ⋮ A herbrandized functional interpretation of classical first-order logic ⋮ Hardwiring truth in functional interpretations ⋮ A proof‐theoretic metatheorem for tracial von Neumann algebras ⋮ Interpreting weak Kőnig's lemma in theories of nonstandard arithmetic ⋮ Stateful Realizers for Nonstandard Analysis ⋮ The FAN principle and weak König's lemma in Herbrandized second-order arithmetic ⋮ On bounded functional interpretations ⋮ Logical metatheorems for abstract spaces axiomatized in positive bounded logic ⋮ The bounded functional interpretation of bar induction ⋮ Intuitionistic nonstandard bounded modified realisability and functional interpretation ⋮ A note on non-classical nonstandard arithmetic ⋮ The finitary content of sunny nonexpansive retractions ⋮ Unnamed Item ⋮ Proof-theoretic uniform boundedness and bounded collection principles and countable Heine-Borel compactness ⋮ The abstract type of the real numbers ⋮ Harrington's conservation theorem redone ⋮ The bounded functional interpretation of the double negation shift ⋮ A Logical Uniform Boundedness Principle for Abstract Metric and Hyperbolic Spaces ⋮ Functional interpretations of linear and intuitionistic logic ⋮ 2006 Annual Meeting of the Association for Symbolic Logic ⋮ A functional interpretation for nonstandard arithmetic ⋮ On Tao's “finitary” infinite pigeonhole principle ⋮ Proof interpretations with truth ⋮ Injecting uniformities into Peano arithmetic ⋮ Metastability of the proximal point algorithm with multi-parameters ⋮ Weak König's lemma in Herbrandized classical second-order arithmetic ⋮ On Some Semi-constructive Theories Related to Kripke–Platek Set Theory ⋮ Bounded modified realizability ⋮ BOUNDS FOR INDEXES OF NILPOTENCY IN COMMUTATIVE RING THEORY: A PROOF MINING APPROACH ⋮ A Rate of Metastability for the Halpern Type Proximal Point Algorithm ⋮ A note on the monotone functional interpretation ⋮ Functional interpretation and inductive definitions ⋮ On the removal of weak compactness arguments in proof mining ⋮ Light Dialectica Program Extraction from a Classical Fibonacci Proof ⋮ Nonstandardness and the bounded functional interpretation

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Effective moduli from ineffective uniqueness proofs. An unwinding of de La Vallée Poussin's proof for Chebycheff approximation
• Pointwise hereditary majorization and some applications
• Mathematically strong subsystems of analysis with low rate of growth of provably recursive functionals
• Proof mining in \(L_{1}\)-approximation
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Extensional Gödel functional interpretation. A consistency proof of classical analysis
• Intuitionistic analysis and Gödel's interpretation
• A QUANTITATIVE VERSION OF A THEOREM DUE TO BORWEIN-REICH-SHAFRIR
• Recursive Functionals and Quantifiers of Finite Types I
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
• Strongly majorizable functionals of finite type: A model for barrecursion containing discontinuous functionals
• Effective bounds from ineffective proofs in analysis: An application of functional interpretation and majorization
• Relative constructivity
• A feasible theory for analysis
• Some logical metatheorems with applications in functional analysis
• Existence and feasibility in arithmetic
• On n-quantifier induction
• Intuitionistische Untersuchungen der formalistischen Logik
• A note on Spector's quantifier-free rule of extensionality
• On uniform weak König's lemma

This page was built for publication: Bounded functional interpretation