Bounded functional interpretation and feasible analysis

DOI10.1016/J.APAL.2006.07.002MaRDI QIDQ866559zbMATH OpenOpenAlexFDO

Authors Fernando Ferreira, Paulo Oliva

Publication date 14 February 2007

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.2006.07.002

zbMATH Keywords

feasibilityfunctional interpretationKönig's lemmamajorizability

Mathematics Subject Classification ID

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

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.

Recommendations

• Bounded functional interpretation
• On bounded functional interpretations
• Interpreting weak Kőnig's lemma in theories of nonstandard arithmetic
• Nonstandardness and the bounded functional interpretation
• Functional interpretations of feasibly constructive arithmetic

Cites work

• A feasible theory for analysis
• Asymmetric Interpretations for Bounded Theories
• Bounded functional interpretation
• Effective bounds from ineffective proofs in analysis: An application of functional interpretation and majorization
• Effective moduli from ineffective uniqueness proofs. An unwinding of de La Vallée Poussin's proof for Chebycheff approximation
• Existence and feasibility in arithmetic
• Extensional Gödel functional interpretation. A consistency proof of classical analysis
• Functional interpretations of feasibly constructive arithmetic
• Groundwork for weak analysis
• scientific article; zbMATH DE number 4002093 (Why is no real title available?)
• scientific article; zbMATH DE number 1215497 (Why is no real title available?)
• scientific article; zbMATH DE number 2236631 (Why is no real title available?)
• scientific article; zbMATH DE number 2236632 (Why is no real title available?)
• scientific article; zbMATH DE number 2236647 (Why is no real title available?)
• Intuitionistische Untersuchungen der formalistischen Logik
• Mathematically strong subsystems of analysis with low rate of growth of provably recursive functionals
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Strongly majorizable functionals of finite type: A model for barrecursion containing discontinuous functionals
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES

Cited in

(20)

• Factorization of the Shoenfield-like bounded functional interpretation
• 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
• Nonstandardness and the bounded functional interpretation
• Bounded functional interpretation
• A note on the monotone functional interpretation
• Confined modified realizability
• The bounded functional interpretation of the double negation shift
• Effective bounds from ineffective proofs in analysis: An application of functional interpretation and majorization
• scientific article; zbMATH DE number 176201 (Why is no real title available?)
• On bounded functional interpretations
• A feasible theory for analysis
• The bounded functional interpretation of bar induction
• Asymmetric Interpretations for Bounded Theories
• Interpreting weak Kőnig's lemma in theories of nonstandard arithmetic
• scientific article; zbMATH DE number 2236632 (Why is no real title available?)
• Functional interpretations of feasibly constructive arithmetic
• Uniform functional interpretations
• Reasonable extreme-bounds analysis
• Functional interpretations of linear and intuitionistic logic

This page was built for publication: Bounded functional interpretation and feasible analysis

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q866559)