A Direct Proof of Schwichtenberg's Bar Recursion Closure Theorem

Oliva, Paulo; Steila, Silvia (2018). A Direct Proof of Schwichtenberg's Bar Recursion Closure Theorem. The journal of symbolic logic, 83(1), pp. 70-83. Cambridge University Press 10.1017/jsl.2017.33

Preview

Text os17.pdf - Accepted Version Available under License Publisher holds Copyright. Download (405kB) | Preview

In [12], 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 α<ɛa 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 T i then terms built from BRNa for this particular Y are definable in the fragment Ti+max {1,level(ơ)}+2'.

Interest & Impact

Downloads

212 since deposited on 02 May 2018
38 in the past 12 months

Citations

5 Citations in Web of Science ®
6 Citations in Scopus

Search

in Google Scholar™

Services

Actions (login required)

Edit item

Actions (login required)

Edit item