Book contents
- Frontmatter
- Preface
- Contents
- TUTORIALS
- ARTICLES
- Modified bar recursion and classical dependent choice
- Choice and uniformity in weak applicative theories
- Compactness and incompactness phenomena in set theory
- Selection for Borel relations
- Interpolation in goal-directed proof systems 1
- Sequences of degrees associated with models of arithmetic
- The limit theory of generic polynomials
- Moschovakis's notion of meaning as applied to linguistics
- Tameness in expansions of the real field
- The model theory of compact complex spaces
- “Natural” representations and extensions of Gödel's second theorem 350
- Effective Hausdorff dimension
- Mutual stationarity in the coremodel
- The pair (Nn, N0) may fail N0-compactness
- Incompleteness theoremand its frontier
- Groups in Simple Theories
- References
Modified bar recursion and classical dependent choice
from ARTICLES
Published online by Cambridge University Press: 31 March 2017
Book contents
- Frontmatter
- Preface
- Contents
- TUTORIALS
- ARTICLES
- Modified bar recursion and classical dependent choice
- Choice and uniformity in weak applicative theories
- Compactness and incompactness phenomena in set theory
- Selection for Borel relations
- Interpolation in goal-directed proof systems 1
- Sequences of degrees associated with models of arithmetic
- The limit theory of generic polynomials
- Moschovakis's notion of meaning as applied to linguistics
- Tameness in expansions of the real field
- The model theory of compact complex spaces
- “Natural” representations and extensions of Gödel's second theorem 350
- Effective Hausdorff dimension
- Mutual stationarity in the coremodel
- The pair (Nn, N0) may fail N0-compactness
- Incompleteness theoremand its frontier
- Groups in Simple Theories
- References
- Type
- Chapter
- Information
- Logic Colloquium '01 , pp. 89 - 107Publisher: Cambridge University PressPrint publication year: 2005
References
[1] and , Gödel's functional (“Dialectica”) interpretation, Handbook of proof theory (, editor), Studies in Logic and the Foundations of Mathematics, vol. 137, North-Holland, 1998, pp. 337–405.
[2] , , and , On the computational content of the axiom of choice, The Journal of Symbolic Logic, vol. 63 (1998), no. 2, pp. 600–622.Google Scholar
[3] , Totale Objekte und Mengen in der Bereichstheorie, Ph.D. thesis, Mathematisches Institut der Universitätünchen, 1990.
[4] , , and , Refined program extraction from classical proofs, Annals of Pure and Applied Logic, vol. 114 (2002), pp. 3–25.Google Scholar
[5] and , Modified bar recursion, BRICS Report Series RS-02-14, BRICS, 2002, 23 pages, http://www.brics.dk/RS/02/14/BRICS-RS-02-14.ps.gz.
[6] and , Program extraction from classical proofs, Logic and Computational Complexity workshop (LCC–94) (, editor), Lecture Notes in Computer Science, vol. 960, Springer, 1995, pp. 77–97.
[7] , Strongly majorizable functionals of finite type: A model for bar recursion containing discontinuous functionals, The Journal of Symbolic Logic, vol. 50 (1985), pp. 652–660.Google Scholar
[8] , Equivalence of bar recursors in the theory of functionals of finite type, Archive for Mathematical Logic, vol. 27 (1988), pp. 149–160.Google Scholar
[9] , Model C of partial continuous functionals, Logic colloquium 1976 ( and , editors), North-Holland, 1977, pp. 455–467.
[10] , ü ber eine bisher noch nicht benützte Erweiterung des finiten Standpunktes, Dialectica, vol. 12 (1958), pp. 280–287.Google Scholar
[11] , Hereditarily majorizable functionals of finite type, Metamathematical investigation of intuitionistic Arithmetic and Analysis (, editor), Lecture Notes in Mathematics, vol. 344, Springer, 1973, pp. 454–461.
[12] and , Transfinite induction and bar induction of types zero and one, and the role of continuity in intuitionistic analysis, The Journal of Symbolic Logic, vol. 31 (1966), no. 3, pp. 325–358.Google Scholar
[13] , Countable functionals, Constructivity in mathematics (, editor), North–Holland, 1959, pp. 81–100.
[14] , Theorie der majorisierbaren und stetigen Funktionale und ihre Anwendung bei der Extraktion von Schranken aus inkonstruktiven Beweisen: Effektive Eindeutigkeitsmodule bei besten Approximationen aus ineffektiven Eindeutigkeitsbeweisen, Ph.D. thesis, Frankfurt, 1990.
[15] , Interpretation of analysis by means of constructive functionals of finite types, Constructivity in mathematics (, editor), North–Holland, 1959, pp. 101–128.
[16] , Extensional Gödel functional interpretation—a consistency proof of classical analysis, Lecture Notes inMathematics, vol. 306, Springer, 1973.
[17] , The continuous functionals, Handbook of computability theory (, editor), North-Holland, 1999, pp. 251–275.
[18] , LCF considered as a programming language, TheoreticalComputer Science, vol. 5 (1977), pp. 223–255.Google Scholar
[19] , On bar recursion of types 0 and 1, The Journal of Symbolic Logic, vol. 44 (1979), pp. 325–329.Google Scholar
[20] , Outline of a mathematical theory of computation, 4th annual Princeton conference on Information Sciences and Systems, 1970, pp. 169–176.Google Scholar
[21] , Lazy functional algorithms for exact real functionals, Mathematical foundations of computer science (, , and , editors), Lecture Notes in Computer Science, vol. 1450, Springer, 1998, pp. 456–464.
[22] , Provably recursive functionals of analysis: Aconsistency proof of analysis by an extension of principles in current intuitionistic mathmatics, Recursive function theory: Proceedings of symposia in pure mathematics (, editor), vol. 5, AmericanMathematical Society, Providence, Rhode Island, 1962, pp. 1–27.
[23] , Metamathematical investigation of intuitionistic Arithmetic and Analysis, Lecture Notes inMathematics, vol. 344, Springer, 1973.
[24] , Realizability, Handbook of proof theory (, editor), vol. 137, North- Holland, 1998, pp. 408–473.
[25] and , Constructivism in mathematics. An introduction, Studies in Logic and the Foundations of Mathematics, vol. 121, North-Holland, 1988.
- 1
- Cited by