Arithmetizing proofs in analysis
General methods of extracting numerical bounds from proofs in classical analysis (negative translation combined with functional interpretation) lead to the order of magnitude which is difficult to explain to a working mathematician. The author describes a supply of general tools which allow to extract much more reasonable bounds from proofs using notoriously non-constructive principles. These tools include the use of constructive \(\varepsilon\)-weakenings of classical principles. Many standard analytical principles (like sequential Borel Lemma, attainment of the maximum value of a continuous function etc.) are provable from WKL, the binary König's Lemma, which cannot even be expressed in ``polynomial systems, since this involves coding functionals for finite sequences. Such principles are treated using a certain schema \(F^-\) which is classically false. However, one can extract polynomial bounds from the proof using \(F^-\). On the other hand, the use of \(F^-\) can be replaced by its \(\varepsilon\)-weakening, and this \(\varepsilon\)-weakening is provable in a system for Kalmar-elementary functions. This shows that the bounds are classically true. A more complicated treatment (producing higher bounds) is needed for the theorems (like convergence of bounded monotone sequences of reals, the Arzela-Ascoli property, etc.) which are proved from instances of the arithmetical comprehension axiom. For the entire collection see [Zbl 0893.00029].
- Relative constructivity
- Mathematically strong subsystems of analysis with low rate of growth of provably recursive functionals
- Some axioms for constructive analysis
- scientific article; zbMATH DE number 2185652
- scientific article; zbMATH DE number 5269066
- scientific article; zbMATH DE number 2236625
- scientific article; zbMATH DE number 2152236
- A realizability interpretation for classical analysis
- scientific article; zbMATH DE number 895269
- scientific article; zbMATH DE number 2247255
- Realizability interpretation of proofs in constructive analysis
- On the arithmetical content of restricted forms of comprehension, choice and general uniform boundedness
- Some computational aspects of metric fixed-point theory
- Things that can and things that cannot be done in PRA
- Proof-theoretic uniform boundedness and bounded collection principles and countable Heine-Borel compactness
- A QUANTITATIVE VERSION OF A THEOREM DUE TO BORWEIN-REICH-SHAFRIR
- Writing Proofs in Analysis
- On the computational content of the Bolzano-Weierstraß Principle
- Proof interpretations and majorizability
- scientific article; zbMATH DE number 5862941 (Why is no real title available?)
- Light monotone Dialectica methods for proof mining
- scientific article; zbMATH DE number 3871342 (Why is no real title available?)
- scientific article; zbMATH DE number 3966052 (Why is no real title available?)
- scientific article; zbMATH DE number 956475 (Why is no real title available?)
- Effective bounds from ineffective proofs in analysis: An application of functional interpretation and majorization
- scientific article; zbMATH DE number 1231647 (Why is no real title available?)
- scientific article; zbMATH DE number 1874095 (Why is no real title available?)
- Some logical metatheorems with applications in functional analysis
- The finitary content of sunny nonexpansive retractions
- From Bolzano‐Weierstraß to Arzelà‐Ascoli
- General logical metatheorems for functional analysis
- On quantitative versions of theorems due to F. E. Browder and R. Wittmann
- Proof mining for the dual of a Banach space with extensions for uniformly Fréchet differentiable functions
- A proof-theoretic bound extraction theorem for monotone operators in Banach spaces
This page was built for publication: Arithmetizing proofs in analysis
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4218526)
