×

zbMATH — the first resource for mathematics

Functional interpretation of bar induction by bar recursion. (English) Zbl 0162.31503

PDF BibTeX XML Cite
Full Text: Numdam EuDML
References:
[1] K. Gödel [1] Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes , Dialectica, 12 (1958), 280-287. · Zbl 0090.01003 · doi:10.1111/j.1746-8361.1958.tb01464.x
[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 Logic 31 (1966), 325 - 358. · Zbl 0156.00804 · doi:10.2307/2270450
[3] S.C. Kleene and R.E. Vesley [3] Foundations of Intuitionistic Mathematics , North-Holland Publishing Co., Amsterdam, 1965. · Zbl 0133.24601
[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. · Zbl 0134.01001
[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. · Zbl 0177.01002 · doi:10.2307/2270324
[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. · Zbl 0143.25502
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.