Informatics Report Series



Related Pages

Report (by Number) Index
Report (by Date) Index
Author Index
Institute Index

Title:Bar recursion is not T+min definable
Authors: ; John Longley
Date:Feb 2015
Publication Type:Internet Publication Publication Status:Pre-print
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.
2015 by The University of Edinburgh. All Rights Reserved
Links To Paper
1st Link
Bibtex format
author = { and John Longley },
title = {Bar recursion is not T+min definable},
year = 2015,
month = {Feb},
howpublished={Internet Publication},
url = {},

Home : Publications : Report 

Please mail <> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh