2016/07/18 by Paulo Oliva, Oliva, Paulo, Silvia Steila +1
Mathematics · #03F07 #03F10 #FOS: Mathematics #Logic (math.LO) #math.LO #msc:03F07 #msc:03F10
paper · pdf · doi:10.48550/arxiv.1607.05237
12 pages
arxiv created 2017/08/15 · arxiv updated 2017/08/16
In 1979 Schwichtenberg showed that the System T definable functionals are closed under a rule-like version Spector's bar recursion of lowest type levels 0 and 1. More precisely, if the functional Y which controls the stopping condition of Spector's bar recursor is T-definable, then the corresponding bar recursion of type levels 0 and 1 is already T-definable. Schwichtenberg's original proof, however, relies on a detour through Tait's infinitary terms and the correspondence between ordinal recursion for α< ε0 and primitive recursion over finite types. This detour makes it hard to calculate on given concrete system T input, what the corresponding system T output would look like. In this paper we present an alternative (more direct) proof based on an explicit construction which we prove correct via a suitably defined logical relation. We show through an example how this gives a straightforward mechanism for converting bar recursive definitions into T-definitions under the conditions of Schwichtenberg's theorem. Finally, with the explicit construction we can also easily state a sharper result: if Y is in the fragment Ti then terms built from BRℕ, σ for this particular Y are definable in the fragment T_i + max \ 1, levelσ \ + 2.