Equivalence of bar recursors in the theory of functionals of finite type (Q1115867): Difference between revisions

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.