Equivalence of bar recursors in the theory of functionals of finite type
type: Item
instance of: scholarly article
title: Equivalence of bar recursors in the theory of functionals of finite type
zbMATH Open document ID: 0665.03042
DOI: 10.1007/BF01620763
author: Marc Bezem
published in: Archive for Mathematical Logic
publication date: 1988-01-01T00:00:00Z
review text: The main result is that the various formulations of bar recursion given by Spector (1962), Howard (1968), Tait (1971), Vogel (1976) and the author (1985) are all equivalent, on the basis of an equational theory of (Gödel) primitive recursion of finite types including a (weak) extensionality rule (i.e., in \(qf-WE-HA^{\omega}\) in Troelstra's terminology). It is also proved that the deduction theorem holds for this theory (this corrects a small oversight of \textit{A. Troelstra} [Metamathematical investigations of intuitionistic arithmetic and analysis, Lect. Notes Math. 344 (1973; Zbl 0275.02025), p. 45], and that a seemingly more general version of the extensionality rule (i.e., from \(P\to T_ 1=T_ 2\) and \(Q[X:\equiv T_ 1]\) conclude \(P\to Q[X:\equiv T_ 2])\) is derivable from the ordinary extensionality rule (without ``P\(\to '')\) (this clears up a point left open by Troelstra [loc. cit., p. 44]). - The paper is carefully written and easy to read.
Mathematics Subject Classification ID: 03F50
Mathematics Subject Classification ID: 03F10
Mathematics Subject Classification ID: 03F15
zbMATH DE Number: 4087660
zbMATH Keywords: bar recursion
zbMATH Keywords: deduction theorem
zbMATH Keywords: extensionality rule
reviewed by: Helmut Schwichtenberg
MaRDI profile type: Publication
cites work: The lambda calculus. Its syntax and semantics. Rev. ed.
cites work: Strongly majorizable functionals of finite type: A model for barrecursion containing discontinuous functionals
cites work: Combinatory logic. With two sections by William Craig.
cites work: Q5545953
cites work: Extensional Gödel functional interpretation. A consistency proof of classical analysis
cites work: Q5519134
cites work: Q4767297
cites work: Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
cites work: Ein starker Normalisationssatz für die bar-rekursiven Funktionale
description: scientific article; zbMATH DE number 4087660