Open AccessProof Theory and Computational Analysis
Author(s) -
Ulrich Kohlenbach
Publication year - 1997
Publication title -
brics report series
Language(s) - English
Resource type - Journals
eISSN - 1601-5355
pISSN - 0909-0878
DOI - 10.7146/brics.v4i30.18956
Subject(s) - mathematical proof , constructive , constructive proof , bounded function , range (aeronautics) , mathematics , focus (optics) , proof complexity , polynomial , convergence (economics) , expressive power , discrete mathematics , computer science , algebra over a field , theoretical computer science , pure mathematics , process (computing) , programming language , mathematical analysis , materials science , geometry , physics , optics , economics , composite material , economic growth
In this survey paper we start with a discussion how functionals of finite type can be used for the proof-theoretic extraction of numerical data (e.g. effective uniform bounds and rates of convergence) from non-constructive proofs in numerical analysis. We focus on the case where the extractability of polynomial bounds is guaranteed. This leads to the concept of hereditarily polynomial bounded analysis (PBA). We indicate the mathematical range of PBA which turns out to be surprisingly large. Finally we discuss the relationship between PBA and so-called feasible analysis FA. It turns out that both frameworks are incomparable. We argue in favor of the thesis that PBA offers the more useful approach for the purpose of extracting mathematically interesting bounds from proofs. In a sequel of appendices to this paper we indicate the expressive power of PBA.