Bounded functional interpretation and feasible analysis
type: Item
instance of: scholarly article
title: Bounded functional interpretation and feasible analysis
zbMATH Open document ID: 1112.03052
author: Fernando Ferreira
author: Paulo Oliva
published in: Annals of Pure and Applied Logic
publication date: 2007-02-14T00:00:00Z
review text: Bounded functional interpretation developed earlier by the authors [Ann. Pure Appl. Logic 135, No. 1--3, 73--112 (2005; Zbl 1095.03060)] is proved here to apply to several theories of feasible first-order arithmetic that have weak induction and polynomially computable provably recursive functions. Combining it with the variants of functional interpretation due to Cook and Urquhart, the authors obtain effective version of a conservation result over weak König's lemma.
Mathematics Subject Classification ID: 03F10
Mathematics Subject Classification ID: 03F30
Mathematics Subject Classification ID: 03F35
zbMATH DE Number: 5126401
zbMATH Keywords: functional interpretation
zbMATH Keywords: König's lemma
zbMATH Keywords: majorizability
zbMATH Keywords: feasibility
reviewed by: G. E. Mints
MaRDI profile type: Publication
full work available at URL: j.apal.2006.07.002
OpenAlex ID: W2135734418
cites work: Q4215634
cites work: Strongly majorizable functionals of finite type: A model for barrecursion containing discontinuous functionals
cites work: Q3754620
cites work: Asymmetric Interpretations for Bounded Theories
cites work: Functional interpretations of feasibly constructive arithmetic
cites work: Q5711882
cites work: A feasible theory for analysis
cites work: Groundwork for weak analysis
cites work: Q5711883
cites work: Bounded functional interpretation
cites work: ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
cites work: Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
cites work: Effective bounds from ineffective proofs in analysis: An application of functional interpretation and majorization
cites work: Effective moduli from ineffective uniqueness proofs. An unwinding of de La Vallée Poussin's proof for Chebycheff approximation
cites work: Mathematically strong subsystems of analysis with low rate of growth of provably recursive functionals
cites work: Intuitionistische Untersuchungen der formalistischen Logik
cites work: Extensional Gödel functional interpretation. A consistency proof of classical analysis
cites work: Existence and feasibility in arithmetic
cites work: Q5711898
DOI: 10.1016/J.APAL.2006.07.002
description: scientific article; zbMATH DE number 5126401