A note on the monotone functional interpretation |
| |
Authors: | Ulrich Kohlenbach |
| |
Affiliation: | Department of Mathematics, Technische Universit?t Darmstadt, Schlossgartenstra?e 7, 64289 Darmstadt, Germany |
| |
Abstract: | We prove a result relating the author's monotone functional interpretation to the bounded functional interpretation due to Ferreira and Oliva. More precisely we show that (over model of majorizable functionals) largely a solution for the bounded interpretation also is a solution for the monotone functional interpretation although the latter uses the existence of an underlying precise witness. This makes it possible to focus on the extraction of bounds (as in the bounded interpretation) while using the conceptual benefit of having precise realizers at the same time without having to construct them. |
| |
Keywords: | Monotone functional interpretation bounded functional interpretation majorizability proof mining MSC (2010) 03F10 03F03 03F35 |
|
|