Hostname: page-component-cd9895bd7-q99xh Total loading time: 0 Render date: 2024-12-22T17:41:54.942Z Has data issue: false hasContentIssue false
  • English
  • Français

BAR RECURSION AND PRODUCTS OF SELECTION FUNCTIONS

Published online by Cambridge University Press:  13 March 2015

MARTÍN ESCARDÓ  and
PAULO OLIVA
MARTÍN ESCARDÓ
Affiliation:
UNIVERSITY OF BIRMINGHAM, SCHOOL OF COMPUTER SCIENCE, BIRMINGHAM B15 2TT, UK
PAULO OLIVA
Affiliation:
QUEEN MARY UNIVERSITY OF LONDON, SCHOOL OF ELECTRONIC ENGINEERING AND COMPUTER SCIENCE, LONDON E1 4NS, UK
Get access Rights & Permissions [Opens in a new window]

Abstract

We show how two iterated products of selection functions can both be used in conjunction with system T to interpret, via the dialectica interpretation and modified realizability, full classical analysis. We also show that one iterated product is equivalent over system T to Spector’s bar recursion, whereas the other is T-equivalent to modified bar recursion. Modified bar recursion itself is shown to arise directly from the iteration of a different binary product of ‘skewed’ selection functions. Iterations of the dependent binary products are also considered but in all cases are shown to be T-equivalent to the iteration of the simple products.

Keywords

Spector bar recursionmodified bar recursionselection functiongeneralised quantifierT-definability
Type
Articles
Information
The Journal of Symbolic Logic , Volume 80 , Issue 1 , March 2015 , pp. 1 - 28
Copyright
Copyright © The Association for Symbolic Logic 2015 

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

Avigad, J. and Feferman, S., Gödel’s functional (“Dialectica”) interpretation, Handbook of proof theory (Buss, S. R., editor), Studies in Logic and the Foundations of Mathematics, vol. 137, North Holland, Amsterdam, 1998, pp. 337–405.Google Scholar
Berardi, S., Bezem, M., and Coquand, T., On the computational content of the axiom of choice, this Journal, vol. 63 (1998), no. 2, pp. 600–622.Google Scholar
Berger, U., A computational interpretation of open induction, Proceedings of the 19th annual IEEE symposium on logic in computer science (Titsworth, F., editor), IEEE Computer Society, 2004, pp. 326–334.Google Scholar
Berger, U. and Oliva, P., Modified bar recursion and classical dependent choice, Lecture Notes in Logic, vol. 20(2005), pp. 89–107.Google Scholar
Berger, U. and Oliva, P., Modified bar recursion, Mathematical Structures in Computer Science, vol. 16 (2006), pp. 163–183.Google Scholar
Berger, U. and Schwichtenberg, H., Program extraction from classical proofs, Logic and computational complexity workshop (LCC’94) (Leivant, D., editor), Lecture Notes in Computer Science, vol. 960, Springer, Berlin, 1995, pp. 77–97.CrossRefGoogle Scholar
Bezem, M., Strongly majorizable functionals of finite type: a model for bar recursion containing discontinuous functionals, this Journal, vol. 50 (1985), pp. 652–660.Google Scholar
Escardó, M. H., Exhaustible sets in higher-type computation, Logical Methods in Computer Science, vol. 4 (2008), no. 3, p. 4.Google Scholar
Escardó, M. H. and Oliva, P., Computational interpretations of analysis via products of selection functions, Programs, Proofs, Processes - CiE 2010, LNCS, vol. 6158 (Ferreira, F., Löwe, B., Mayordomo, E., and Gomes, L. M., editors), Springer, 2010, pp. 141–150.Google Scholar
Escardó, M. H. and Oliva, P., The Peirce translation and the double negation shift, Programs, Proofs, Processes - CiE 2010, LNCS, vol. 6158 (Ferreira, F., Löwe, B., Mayordomo, E., and Gomes, L. M., editors), Springer, 2010, pp. 151–161.Google Scholar
Escardó, M. H. and Oliva, P., Selection functions, bar recursion, and backward induction, Mathematical Structures in Computer Science, vol. 20 (2010), no. 2, pp. 127–168.CrossRefGoogle Scholar
Escardó, M. H. and Oliva, P., Sequential games and optimal strategies, Royal Society Proceedings A, vol. 467 (2011), pp. 1519–1545.Google Scholar
Gödel, K., Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes. Dialectica, vol. 12 (1958), pp. 280–287.Google Scholar
Howard, W. A., Functional interpretation of bar induction by bar recursion. Compositio Mathematica, vol. 20 (1968), pp. 107–124.Google Scholar
Kohlenbach, U., Applied proof theory: Proof interpretations and their use in mathematics, Monographs in Mathematics, Springer, 2008.Google Scholar
Oliva, P. and Powell, T., On Spector’s bar recursion. Mathematical Logic Quarterly, vol. 58 (2012), no. 4–5, pp. 356–365.Google Scholar
Powell, T., The equivalence of bar recursion and open recursion. Annals of Pure and Applied Logic, vol. 165 (2014), pp. 1727–1754.CrossRefGoogle 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: Proc. symposia in pure mathematics (Dekker, F. D. E., editor), vol. 5, American Mathematical Society, Providence, Rhode Island, 1962, pp. 1–27.Google Scholar
Tait, W. W., Infinitely long terms of transfinite type, Formal Systems and Recursive Functions (Proc. Eighth Logic Colloq., Oxford), North-Holland, Amsterdam, 1965, pp. 176–185.Google Scholar
Troelstra, A. S., Metamathematical investigation of intuitionistic arithmetic and analysis, Lecture Notes in Mathematics, vol. 344, Springer, Berlin, 1973.Google Scholar