Functional interpretation of bar induction by bar recursion
Howard, W. A.
Compositio Mathematica, Tome 20 (1968), p. 107-124 / Harvested from Numdam
Access to full text
Full (PDF)
Full (DJVU) 
@article{CM_1968__20__107_0,
     author = {Howard, W. A.},
     title = {Functional interpretation of bar induction by bar recursion},
     journal = {Compositio Mathematica},
     volume = {20},
     year = {1968},
     pages = {107-124},
     mrnumber = {230619},
     zbl = {0162.31503},
     language = {en},
     url = {http://dml.mathdoc.fr/item/CM_1968__20__107_0}
}

Howard, W. A. Functional interpretation of bar induction by bar recursion. Compositio Mathematica, Tome 20 (1968) pp. 107-124. http://gdmltest.u-ga.fr/item/CM_1968__20__107_0/

K. Gödel [1] Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes, Dialectica, 12 (1958), 280-287. | MR 102482 | Zbl 0090.01003

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 Logic 31 (1966), 325 - 358. | Zbl 0156.00804

S.C. Kleene and R.E. Vesley [3] Foundations of Intuitionistic Mathematics, North-Holland Publishing Co., Amsterdam, 1965. | MR 176922 | Zbl 0133.24601

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. | MR 106838 | Zbl 0134.01001

G. Kreisel [5] Proof by transfinite induction and definition by transfinite recursion, Journal of Symbolic Logic, 24 (1959), 322-323.

G. Kreisel [6] A survey of proof theory, Journal of Symbolic Logic, to appear. | MR 281580 | Zbl 0177.01002

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. | MR 154801 | Zbl 0143.25502