Bounded functional interpretation and feasible analysis

In this article we study applications of the bounded functional interpretation to theories of feasible arithmetic and analysis. The main results show that the novel interpretation is sound for considerable generalizations of weak K¨onig’s lemma, even in the presence of very weak induction. Moreover, when combined with Cook and Urquhart’s variant of the functional interpretation, one obtains effective versions of conservation results regarding weak K¨onig’s lemma which have been so far only obtained non-constructively. Key words: Functional interpretation, majorizability, feasibility, proof theory. 1991 MSC: 03F03, 03F10, 03F30, 03F35, 03D15

• Type: Journal
• Year: 2007
• Where: APAL
• Authors: Fernando Ferreira, Paulo Oliva
• Keywords: APAL 2007, Functional Interpretation, K¨onig’s Lemma, Weak K¨onig Lemma