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

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 rulelike 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 Tdefinable, then the corresponding bar recursion of type levels 0 and 1 is already Tdefinable. 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 Tdefinitions 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'.
Item Type: 
Journal Article (Original Article) 

Division/Institute: 
08 Faculty of Science > Institute of Computer Science (INF) > Logic and Theory Group (LTG) 08 Faculty of Science > Institute of Computer Science (INF) 
UniBE Contributor: 
Steila, Silvia 
Subjects: 
000 Computer science, knowledge & systems 500 Science > 510 Mathematics 
ISSN: 
00224812 
Publisher: 
Cambridge University Press 
Language: 
English 
Submitter: 
Lukas Jaun 
Date Deposited: 
02 May 2018 12:33 
Last Modified: 
02 May 2018 12:33 
Publisher DOI: 
10.1017/jsl.2017.33 
BORIS DOI: 
10.7892/boris.112774 
URI: 
https://boris.unibe.ch/id/eprint/112774 