- Abstract:
-
This note supplies the proof of a theorem stated in the forthcoming book by Longley and Normann: namely, that Spector s bar recursion functional is not representable by a left-well-founded sequential procedure, and hence is not definable in the language T+min (that is, G odel s System T augmented with the minimization operator), for instance within the Kleene Kreisel model of total continuous functionals.
- Copyright:
- 2015 by The University of Edinburgh. All Rights Reserved
- Links To Paper
- 1st Link
- Bibtex format
- @Misc{EDI-INF-RR-1420,
- author = {
and John Longley
},
- title = {Bar recursion is not T+min definable},
- year = 2015,
- month = {Feb},
- howpublished={Internet Publication},
- url = {http://homepages.inf.ed.ac.uk/jrl/Research/bar-rec-not-Tmin.pdf},
- }
|
