Functional interpretation of bar induction by bar recursion

W. A. Howard

Compositio Mathematica (1968)

  • Volume: 20, page 107-124
  • ISSN: 0010-437X

How to cite


Howard, W. A.. "Functional interpretation of bar induction by bar recursion." Compositio Mathematica 20 (1968): 107-124. <>.

author = {Howard, W. A.},
journal = {Compositio Mathematica},
keywords = {recursion theory, constructive mathematics},
language = {eng},
pages = {107-124},
publisher = {Wolters-Noordhoff Publishing},
title = {Functional interpretation of bar induction by bar recursion},
url = {},
volume = {20},
year = {1968},

AU - Howard, W. A.
TI - Functional interpretation of bar induction by bar recursion
JO - Compositio Mathematica
PY - 1968
PB - Wolters-Noordhoff Publishing
VL - 20
SP - 107
EP - 124
LA - eng
KW - recursion theory, constructive mathematics
UR -
ER -


  1. K. Gödel [1] Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes, Dialectica, 12 (1958), 280-287. Zbl0090.01003MR102482
  2. W.A. Howard and G. Kreisel [2] Transfinite induction and bar induction of types zero and one, and the role of continuity in intuitionistic analysis, Journal of Symbolic Logic31 (1966), 325 — 358. Zbl0156.00804
  3. S.C. Kleene and R.E. Vesley [3] Foundations of Intuitionistic Mathematics, North-Holland Publishing Co., Amsterdam, 1965. Zbl0133.24601MR176922
  4. G. Kreisel [4] Interpretation of analysis by means of constructive functionals of finite types, Constructivity in Mathematics, North-Holland Publishing Co., Amsterdam, 1959, 101-128. Zbl0134.01001MR106838
  5. G. Kreisel [5] Proof by transfinite induction and definition by transfinite recursion, Journal of Symbolic Logic, 24 (1959), 322-323. 
  6. G. Kreisel [6] A survey of proof theory, Journal of Symbolic Logic, to appear. Zbl0177.01002MR281580
  7. C. Spector [7] Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles formulated in current intuitionistic mathematics, Proceedings of the Symposia in Pure Mathematics, vol. 5, American Mathematical Society, Providence, 1962, 1- 27. Zbl0143.25502MR154801

NotesEmbed ?


You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.


Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.