Hostname: page-component-586b7cd67f-dlnhk Total loading time: 0 Render date: 2024-11-24T15:05:13.340Z Has data issue: false hasContentIssue false
  • English
  • Français

A DIRECT PROOF OF SCHWICHTENBERG’S BAR RECURSION CLOSURE THEOREM

Published online by Cambridge University Press:  12 February 2018

PAULO OLIVA  and
SILVIA STEILA
PAULO OLIVA
Affiliation:
SCHOOL OF ELECTRONIC ENGINEERING AND COMPUTER SCIENCE QUEEN MARY, UNIVERSITY OF LONDON PETER LANDING BUILDING, 10 GODWARD SQUARE LONDON E1 4FZ, UKE-mail:[email protected]
SILVIA STEILA
Affiliation:
INSITUTE OF COMPUTER SCIENCE UNIVERSITY OF BERN NEUBRÜCKSTRASSE 10 CH-3012 BERN, SWITZERLANDE-mail:[email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

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 $\alpha < {\varepsilon _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^{\mathbb{N},\sigma } $ for this particular Y are definable in the fragment ${T_{i + {\rm{max}}\left\{ {1,{\rm{level}}\left( \sigma \right)} \right\} + 2}}$.

Keywords

03F0703F10Spector’s bar recursionSchwichtenberg’s closure theoremlogical relationsgeneral bar recursionSystem T
Type
Articles
Information
The Journal of Symbolic Logic , Volume 83 , Issue 1 , March 2018 , pp. 70 - 83
Copyright
Copyright © The Association for Symbolic Logic 2018 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

Berardi, S., Oliva, P., and Steila, S., An analysis of the Podelski-Rybalchenko termination theorem via bar recursion. Journal of Logic and Computation, (2015), First published online: August 28, 2015. Available at https://doi.org/10.1093/logcom/exv058.Google Scholar
Diller, J., Zur Theorie rekursiver Funktionale höherer Typen, Habilitationsschrift, München, 1968.Google Scholar
Gödel, K., Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes. Dialectica, vol. 12 (1958), pp. 280–287.CrossRefGoogle Scholar
Howard, W. A., Functional interpretation of bar induction by bar recursion. Compositio Mathematica, vol. 20 (1968), pp. 107–124.Google Scholar
Howard, W. A., Ordinal analysis of bar recursion of type zero. Compositio Mathematica, vol. 42 (1980), no. 1, pp. 105–119.Google Scholar
Howard, W. A., Ordinal analysis of simple cases of bar recursion, this Journal, vol. 46 (1981), no. 1, pp. 17–30.Google Scholar
Kohlenbach, U., On the no-counterexample interpretation, this Journal, vol. 64 (1999), no. 4, pp. 1491–1511.Google Scholar
Kreuzer, A., Primitive recursion and the chain antichain principle. Notre Dame Journal of Formal Logic, vol. 53 (2012), no. 2, pp. 245–265.CrossRefGoogle Scholar
Podelski, A. and Rybalchenko, A., Transition invariants, Proceedings of the 19th IEEE Symposium on Logic in Computer Science (LICS 2004), IEEE Computer Society, 2004, pp. 32–41.Google Scholar
Ramsey, F. P., On a problem in formal logic. Proceedings of the London Mathematical Society, vol. 30 (1930), pp. 264–286.CrossRefGoogle Scholar
Schwichtenberg, H., Elimination of higher type levels in definitions of primitive recursive functionals by means of transfinite recursion, Proceedings of the Logic Colloquium’73 (Rose, H. E. and Shepherdson, J. C., editors), Studies in Logic and the Foundations of Mathematics, vol. 80, Elsevier, New York, 1975, pp. 279–303.Google Scholar
Schwichtenberg, H., On bar recursion of types 0 and 1, this Journal, vol. 44 (1979), no. 3, pp. 325–329.Google Scholar
Spector, C., Provably recursive functionals of analysis: A consistency proof of analysis by an extension of principles in current intuitionistic mathematics, Recursive Function Theory (Dekker, F. D. E., editor), Proceedings of Symposia in Pure Mathematics, vol. 5, American Mathematical Society, Providence, RI, 1962, pp. 1–27.CrossRefGoogle Scholar
Tait, W. W., Infinitely long terms of transfinite type, Formal Systems and Recursive Functions (Crossley, J. N. and Dummett, M. A. E., editors), Studies in Logic and the Foundations of Mathematics, vol. 40, Elsevier, Amsterdam, 1965, pp. 176–185.CrossRefGoogle Scholar