Abstract
The main result of this paper is the equivalence of several definition schemas of bar recursion occurring in the literature on functionals of finite type. We present the theory of functionals of finite type, in [T] denoted byqf-WE-HA ω, which is necessary for giving the equivalence proofs. Moreover we prove two results on this theory that cannot be found in the literature, namely the deduction theorem and a derivation of Spector's rule of extensionality from [S]: ifP→T 1=T 2 and Q[X∶≡T1], then P→Q[X∶≡ T2], from the at first sight weaker rule obtained by omitting “P→”.
Similar content being viewed by others
References
Barendregt, H.P.: The lambda calculus. Amsterdam: North-Holland 1984
Bezem, M.A.: Strongly majorizable functionals of finite type: a model for bar recursion containing discontinuous functionals. J. Symb. Logic50, 652–660 (1985)
Curry, H.B., Feys, R.: Combinatory logic. Amsterdam: North-Holland 1958
Howard, W.A.: Functional interpretation of bar induction by bar recursion. Compos. Math.20, 107–124 (1968)
Luckhardt, H.: Extensional Gödel functional interpretation. (Lect. Notes Math., vol. 306) Berlin Heidelberg New York: Springer 1973
Spector, C.: Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles formulated in current intuitionistic mathematics. In: Dekker, J.C.E. (ed.): Proceedings of symposia in pure mathematics V, pp. 1–27. Providence: AMS 1962
Tait, W.W.: Normal form theorem for bar recursive functions of finite type. In: Proceedings of the second scandinavian logic symposium, pp. 353–367. Amsterdam: North-Holland 1971
Troelstra, A.S. (ed.): Metamathematical investigation of intuitionistic arithmetic and analysis. (Lect. Notes Math., vol. 344) Berlin Heidelberg New York: Springer 1973
Vogel, H.: Ein starker Normalisationssatz für die barrekursiven Funktionale. Arch. Math. Logik Grundlagenforsch.18, 81–84 (1976)
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Bezem, M. Equivalence of bar recursors in the theory of functionals of finite type. Arch Math Logic 27, 149–160 (1988). https://doi.org/10.1007/BF01620763
Received:
Issue Date:
DOI: https://doi.org/10.1007/BF01620763