Skip to main content
Log in

Analysing choice sequences

  • Published:
Journal of Philosophical Logic Aims and scope Submit manuscript

This is a preview of subscription content, log in via an institution to check access.

Access this article

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

References

  • Aczel, P.: 1978, ‘The type theoretic interpretation of constructive set theory’, in: A. Macintyre, L. Pacholski, and J. Paris (eds.), Logic Colloquium 77, North-Holland, Amsterdam, pp. 55–66.

    Google Scholar 

  • Ashvinikumar: 1979, ‘Microscopic completeness of full indications and intuitionist contradictory proofs’, Indag. Math. 41, 95–103.

    Google Scholar 

  • Bernays, P., 1970, ‘Die schematische Korrespondenz und die idealisierten Strukturen’, Dialectica 24, 53–66.

    Google Scholar 

  • Bernini, S.: 1976, ‘A very strong intuitionistic theory’, Studia Logica 35, 377–385.

    Google Scholar 

  • Bernini, S.: 1978, ‘A note on my paper “A very strong intuitionistic theory”’, Studia Logica 37, 349–350.

    Google Scholar 

  • Borel, E.: 1908, ‘Les “Paradoxes” de la théorie des ensembles’, Annales de l'Ecole Normale (3) 25, 443–448. Reprinted in Borel (1914), pp. 162–166, and Œ 3, 1271–1276.

  • Borel, E.: 1909, ‘Sur les principes de la théorie des ensembles’, in: Atti del IV Congresso Internazionale dei Matematici, Roma, 6–11 Aprile 1908, Academia dei Lincei, Rome; reprinted in Borel (1914), pp. 160–162, and Œ 3, 1267–1269.

    Google Scholar 

  • Borel, E.: 1912, ‘La philosophie mathématique et l'infini, Revue du Mois 14, 218–227, reprinted in Borel (1914), pp. 116–174, and Œ 4, 2127–2136.

    Google Scholar 

  • Borel, E.: 1914, Leçons sur la théorie des fonctions, 2nd edn., Gauthier-Villars, Paris. 3rd edn., 1928. Contains the text of the second edition, with the same pagination. Note VII has been added. 4th edition, 1950. Addition of Note VIII.

    Google Scholar 

  • Borel, E.: 1972, Oeuvres, Editions du Centre National de la Recherche Scientifique, Paris, 4 volumes (abbreviation Œ).

    Google Scholar 

  • Brouwer, L. E. J.: 1907, Over de grondslagen der wiskunde, PhD thesis, Amsterdam, Maas en van Suchtelen, Amsterdam. Reprinted with additional material, and D. van Dalen as editor, in the series MC Varia 1, Mathematisch Centrum, Amsterdam, 1981. (English translation in CW.)

  • Brouwer, L. E. J.: 1909, ‘Die möglichen Mächtigkeiten’, Atti del IV Congresso Internazionale dei Matematici, Roma, 6–11 Aprile 1908, Academia dei Lincei, Roma, pp. 569–571.

    Google Scholar 

  • Brouwer, L. E. J.: 1912, ‘Intuitionisme en formalisme’. Inaugural address, University of Amsterdam. English translation: ‘Intuitionism and formalism’, Bull. A.M.S. 20 (1913), 81–96; also in CW.

  • Brouwer, L. E. J.: 1914, Review of: ‘A. Schoenflies und H. Hahn, Die Entwicklung der Mengenlehre und ihrer Anwendungen’, Jahresber. Deutsch. Math.-Verein. 23, 78–83 (kursiv).

    MATH  Google Scholar 

  • Brouwer, L. E. J.: 1917, ‘Addenda en corrigenda over de grondslagen der wiskunde’, Verslagen der Koninklijke Nederlandse Akademie van Wetenschappen 25, 1418–1423.

    Google Scholar 

  • Brouwer, L. E. J.: 1918, ‘Begründung der Mengenlehre unabhängig vom logischen Satz vom ausgeschlossenen Dritten. Erster Teil, Allgemeine Mengenlehre’, Verhandelingen der Koninklijke Nederlandse Akademie van Wetenschappen, 1ste sectie 12, no. 5.

  • Brouwer, L;E. J.: 1919, ‘Begründung der Mengenlehre unabhängig vom logischen Satz vom ausgeschlossenen Dritten. Zweiter Teil, Theorie der Punktmengen’, Verhandelingen der Koninklijke Nederlandse Akademie van Wetenschappen, 1ste sectie 12, no. 7.

  • Brouwer, L. E. J.: 1923, ‘Begründung der Funktionenlehre unabhängig vom logischen Satz vom ausgeschlossenen Dritten. Erster Teil, Stetigkeit, Messbarkeit, Derivierbarkeit’, Verhandelingen der Koninklijke Nederlandse Akademie van Wetenschappen, 1 ste sectie 13, no. 2.

  • Brouwer, L. E. J.: 1924, ‘Beweis, dass jede volle funktion gleichmässig stetig ist’, Proc. Kon. Ned. Akad. Wet. Amsterdam 27, 189–193.

    Google Scholar 

  • Brouwer, L. E. J.: 1924a, ‘Bemerkungen zum Beweise der gleichmässigen Stetigkeit voller Funktionen’, Proc. Kon. Ned. Akad. Wet. Amsterdam, 27, 644–646.

    Google Scholar 

  • Brouwer, L. E. J.: 1925, ‘Zur Begründung der intuitionistischen Mathematik, Erster Teil’, Math. Ann. 93, 244–257.

    Google Scholar 

  • Brouwer, L. E. J.: 1927, ‘Über Definitionsbereiche von Funktionen’, Math. Ann. 97, 60–75.

    Google Scholar 

  • Brouwer, L. E. J.: 1942, ‘Zum freien Werden von Mengen und Funktionen’, Indag. Math. 4, 107–108.

    Google Scholar 

  • Brouwer, L. E. J.: 1949, ‘De non-aequivalentie van de constructieve en de negatieve orderelatie in het continuum’, Indag. Math. 11, 37–39. (English translation in CW.)

    Google Scholar 

  • Brouwer, L. E. J.: 1952, ‘Historical background, principles and methods of intuitionism’, South African J. Science 49, 139–147.

    Google Scholar 

  • Brouwer, L. E. J.: 1975, Collected Works, Vol. I: Philosophy and Foundations of Mathematics, edited by A. Heyting, North-Holland, Amsterdam (abbreviation CW).

    Google Scholar 

  • Dragalin, A. G.: 1974, ‘A constructive model of intuitionistic analysis’ (Russian), in D. V. Tavanec and V. A. Smirnov (eds.), Philosophy and Logic (Russian), Izdat ‘Nauka’, Moscow, pp. 55–78.

    Google Scholar 

  • Dragalin, A. G.: 1974a, ‘Constructive models of theories of intuitionistic choice sequences’ (Russian), in D. A. Bočvar (ed.), Studies in Formalized Languages and Non-classical Logic (Russian), Izdat. ‘Nauka’, Moscow, pp. 214–252.

    Google Scholar 

  • Dummett, M. A. E.: 1977, Elements of Intuitionism, Clarendon Press, Oxford.

    Google Scholar 

  • Feferman, S.: 1980, ‘Constructive theories of functions and classes’, in M. Boffa, D. Van Dalen and K. McAloon (eds.), Logic Colloquium 78, North-Holland, Amsterdam, pp. 159–224.

    Google Scholar 

  • Fourman, M. P.: 1983, ‘Notions of choice sequences’, in Troelstra and Van Dalen (1983).

  • Fourman, M. P. and Hyland, J. M. E.: 1979, ‘Sheaf models for analysis’, in Fourman et al. (1979) 280–301.

  • Fourman, M. P., Mulvey, C., and Scott, D. S. (eds.): 1979, Applications of Sheaves, Springer-Verlag, Berlin.

    Google Scholar 

  • Fourman, M. P. and Scott, D. S.: 1979, ‘Sheaves and Logic’, in: Fourman et al. 302–401.

  • Gandy, R. O.: 1980, ‘Church's thesis and principles for mechanics’, in: J. Barwise, H. J. Keisler, and K. Kunen (eds.), The Kleene Symposium, North-Holland, Amsterdam, pp. 123–148.

    Google Scholar 

  • Gielen, W., de Swart, H., and Veldman, W.: 1981, ‘The continuum hypothesis in intuitionism’, J. Symbolic Logic 46, 121–136. Preprint: Report 7908, Mathematisch Instituut, Katholieke Universiteit Nijmegen, 1979.

    Google Scholar 

  • Gödel, K.: 1947, ‘What is Cantor's continuum problem’, American Math. Monthly 54, 515–525. Revised and expanded in P. Benacerraf and H. Putnam (eds.), Philosophy of Mathematics: Selected Readings, Prentice-Hall, Englewood Cliffs, NJ, 1964, pp. 258–273.

    Google Scholar 

  • Goodman, N. D.: 1979, ‘Review of Dummett 1977’, J. Symbolic Logic 44, 276–277.

    Google Scholar 

  • Grayson, R. J.: 1981, ‘Concepts of general topology in constructive mathematics and sheaves’, Ann. Math. Logic 20, 1–41. Preprint Report 78–12, Dept. of Mathematics, University of Amsterdam, 1978.

    Google Scholar 

  • Greenleaf, N.: 1981, ‘Liberal constructive set theory’, in Richman (1981), 213–240.

  • Heyting, A.: 1930, ‘Die formalen Regeln der intuitionistischen Mathematik III’, Sitzungsberichte der preussischen Akademie von Wissenschaften, physikalishcmathematische Klasse, 42–56.

  • Heyting, A.: 1981, ‘Continuum en keuzenrij bij Brouwer’, Nieuw Arch. Wisk (3) 29, 125–139.

    Google Scholar 

  • Howard, W. A. and Kreisel, G.: 1966, ‘Transfinite induction and bar induction of types zero and one, and the role of continuity in intuitionistic analysis’, J. Symbolic Logic 31, 321–358.

    Google Scholar 

  • Isles, D.: 1981, ‘Remarks on the notion of standard non-isomorphic natural number series’, in Richman (1981), 111–134.

  • Jervell, H. R.: 1978, ‘From the axiom of choice to choice sequences — a historical note’, manuscript.

  • Kino, A., Myhill, J., and Vesley, R. E. (eds.): 1970, Intuitionism and Proof Theory, North-Holland, Amsterdam.

    Google Scholar 

  • Kleene, S. C. and Vesley, R. E.: 1965, The Foundations of Intuitionistic Mathematics, Especially in Relation to Recursive Functions, North-Holland, Amsterdam.

    Google Scholar 

  • Kreisel, G.: 1958, ‘A remark on free choice sequences and the topological completeness proofs’, J. Symbolic Logic 23, 369–388.

    Google Scholar 

  • Kreisel, G.: 1963, Section IV in ‘Stanford report on the foundations of analysis’, Stanford University, mimeographed.

  • Kreisel, G.: 1965, ‘Mathematical logic’, in T. L. Saaty (ed.), Lectures on Modern Mathematics Vol. III, John Wiley and Sons, New York, pp. 95–195.

    Google Scholar 

  • Kreisel, G.: 1967, ‘Informal rigour and completeness proofs’, in I. Lakatos (ed.), Problems in the Philosophy of Mathematics, North-Holland, Amsterdam, pp. 138–186.

    Google Scholar 

  • Kreisel, G.: 1968, ‘Lawless sequences of natural numbers’, Compositio Math. 20, 222‐248.

  • Kreisel, G.: 1970, ‘Church's thesis: a kind of reducibility axiom for constructive mathematics’, in Kino et al. (1970), pp. 121–150.

  • Kreisel, G.: 1971, ‘A survey of proof theory II’, in J. E. Fenstad (ed.), Proceedings of the Second Scandinavian Logic Symposium, North-Holland, Amsterdam, pp. 109–170.

    Google Scholar 

  • Kreisel, G. and Troelstra, A. S.: 1970, ‘Formal systems for some branches of intuitionistic analysis’, Ann. Math. Logic 1, 229–387.

    Google Scholar 

  • Krol', M. D.: 1976, ‘The topological models of intuitionistic analysis. One counterexample’, Mathematical Notes 19, 503–504, translation from Mat. Zametki 19, 859–862 (Russian).

    Google Scholar 

  • Krol', M. D.: 1977, ‘Disjunctive and existential properties of intuitionistic analysis with Kripke's scheme’ (Russian), Doklady Akad. Nauk SSSR 234, 750–753. (English translation: Soviet Math. Doklady 18, 755–758.)

    Google Scholar 

  • Krol', M. D.: 1978, ‘Distinct variants of Kripke's schema in intuitionistic analysis’ (Russian), Doklady Akad. Nauk SSSR 239, 1048–1051. (English translation: Soviet Math. Doklady 19, 474–477.)

    Google Scholar 

  • Krol', M. D.: 1978a, ‘A topological model for intuitionistic analysis with Kripke's scheme’, Z. Math. Logik Grundlag. Math. 24, 427–436.

    Google Scholar 

  • Lakatos, I.: 1976, Proofs and Refutations, Cambridge University Press, Cambridge.

    Google Scholar 

  • Lodder, J. S. and Van Dalen, D.: 1983, ‘Lawlessness and independence’, to appear in Troelstra and Van Dalen (1983). Preprint 189, Department of Mathematics, Utrecht University, 1981.

  • Martino, E. and Giaretta, F.: 1981, ‘Brouwer, Dummett and the bar theorem’, in S. Bernini (ed.), Atti del Congresso Nazionale di Logica Montecatini Terme 1–5 Ottobre 1979, Bibliopolis, Napoli, pp. 541–558.

    Google Scholar 

  • Moerdijk, I. and Van der Hoeven, G. F.: 1982, ‘Sheaf models for choice sequences’, Report 82-01, Department of Mathemtics, University of Amsterdam.

  • Moschovakis, J. R.: 1973, ‘A topological interpretation of second-order intuitionistic arithmetic’, Compositio Math. 26, 261–276.

    Google Scholar 

  • Myhill, J.: 1967, ‘Notes towards an axiomatization of intuitionistic analysis’, Logique et analyse (N.S.) 9, 280–297.

    Google Scholar 

  • Parikh, R.: 1971, ‘Existence and feasibility in arithmetic’, J. Symbolic Logic 36, 494–508.

    Google Scholar 

  • Posy, C.: 1974, ‘Brouwer's constructivism’, Synthese 27, 125–129.

    Google Scholar 

  • Posy, C.: 1976, ‘Varieties of indeterminacy in the theory of general choice sequences’, J. Philos. Logic 5, 91–132.

    Google Scholar 

  • Posy, C.: 1977, ‘The theory of empirical sequences’, J. Philos. Logic 6, 47–48.

    Google Scholar 

  • Posy, C.: 1980, ‘On Brouwer's definition of unextendable order’, History and Philosophy of Logic 1, 139–149.

    Google Scholar 

  • Richman, F. (ed.): 1981, Constructive Mathematics, Proceedings, New Mexico 1980, Springer-Verlag, Berlin.

    Google Scholar 

  • Schultz, K.: 1970, ‘Modelle modaler Mengenlehre’, Z. Math. Logik Grundlag. Math. 16, 327–339.

    Google Scholar 

  • Schultz, K.: 1980, ‘A topological model for Troelstra's system CS of intuitionistic analysis’, Z. Math. Logik Grundlag. Math. 26, 349–354.

    Google Scholar 

  • Scott, D. S.: 1970, ‘Extending the topological interpretation to intuitionistic analysis II’, in Kino et al. (1970), 235–255.

  • Troelstra, A. S.: 1968, ‘The theory of choice sequences’, in B. van Rootselaar and J. F. Staal (eds.), Logic, Methodology and Philosophy of Science III, North-Holland, Amsterdam, pp. 201–223.

    Google Scholar 

  • Troelstra, A. S.: 1969, ‘Informal theory of choice sequences’, Studia Logica 25, 31–52.

    Google Scholar 

  • Troelstra, A. S.: 1969a, Principles of Intuitionism, Springer-Verlag, Berlin.

    Google Scholar 

  • Troelstra, A. S.: 1969b, ‘Notes on the intuitionistic theory of sequences I’, Indag. Math. 31, 430–440.

    Google Scholar 

  • Troelstra, A. S.: 1960, ‘Notes on the intuitionistic theory of sequences II’, Indag. Math. 32, 99–109.

    Google Scholar 

  • Troelstra, A. S.: 1970a, ‘Notes on the intuitionistic theory of sequences III’, Indag. Math. 32, 245–252.

    Google Scholar 

  • Troelstra, A. S. (ed.): 1973, Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, Springer-Verlag, Berlin.

    Google Scholar 

  • Troelstra, A. S.: 1973a, ‘Notes on intuitionistic second order arithmetic’, in A. R. D. Mathias and H. Rogers (eds.), Cambridge Summer School in Mathematical Logic, Springer-Verlag, Berlin, pp. 171–205.

    Google Scholar 

  • Troelstra, A. S.: 1977, Choice Sequences, Clarendon Press, Oxford.

    Google Scholar 

  • Troelstra, A. S.: 1977a, ‘Aspects of constructive mathematics’, in J. Barwise (ed.), Handbook of Mathematical Logic, North-Holland, Amsterdam, pp. 973–1052.

    Google Scholar 

  • Troelstra, A. S.: 1977b, ‘Completeness and validity for intuitionistic predicate logic’, in Colloque international de logique Clermont-Ferrand 18–25 juillet 1975, CNRS, Paris, pp. 39–58.

    Google Scholar 

  • Troelstra, A. S.: 1977c, ‘Special instances of generalized continuity which are conservative over intuitionistic arithmetic’, Indag. Math. 39, 55–65.

    Google Scholar 

  • Troelstra, A. S.: 1977d, ‘A note on non-extensional operations in connection with continuity and recursiveness’, Indag. Math. 39, 455–462.

    Google Scholar 

  • Troelstra, A. S.: 1979, ‘On Ashvinikumar's principle of microscopic completeness’, Indag. Math. 41, 77–81.

    Google Scholar 

  • Troelstra, A. S.: 1980, ‘The interplay between logic and mathematics: intuitionism’, in E. Agazzi (ed.), Modern Logic — A Survey, D. Reidel, Dordrecht, pp. 197–221.

    Google Scholar 

  • Troelstra, A. S.: 1980a, ‘Extended bar induction of type 0’, in J. Barwise, H. J. Keisler, and K. Kunen (eds.), The Kleene Symposium, North-Holland, Amsterdam, pp. 277–316.

    Google Scholar 

  • Troelstra, A. S.: 1981, ‘Choice sequences and informal rigour’, Report 81-14. Department of Mathematics, University of Amsterdam.

  • Troelstra, A. S.: 1981a, ‘Lawless sequences and their uses’, in S. Bernini (ed.), Atti del Congresso Nazionale di Logica Montecatini Terme 1–5 Ottobre 1979, Bibliopolis, Napoli, pp. 165–173.

    Google Scholar 

  • Troelstra, A. S.: 1981b, ‘On a second order propositional operator in intuitionistic logic’, Studia Logica 40, 113–139. (Preprint Report 79–14, Department of Mathematics, University of Amsterdam, 1979.)

    Google Scholar 

  • Troelstra, A. S.: 1983, ‘On the origin and development of Brouwer's concept of choice sequence’, to appear in Troelstra and Van Dalen (1983).

  • Troelstra, A. S. and Van Dalen, D. (eds.): 1983, Proceedings of the Brouwer Centenary Conference, North-Holland, Amsterdam, to appear.

    Google Scholar 

  • Turing, A. M.: 1936, ‘On computable numbers, with an application to the Entscheidungs-problem’, Proc. London Math. Soc. 42 (1936–1937), 230–265; corrections, Proc. London Math. Soc. 43 (1937), 544–546.

    Google Scholar 

  • Van Dalen, D.: 1978, ‘An interpretation of intuitionistic analysis’, with an appendix by A. S. Troelstra, Ann. Math. Logic 13, 1–43.

    Google Scholar 

  • Van Dalen, D. and Troelstra, A. S.: 1970, ‘Projections of lawless sequences’, in: Kino et al. (1970) pp. 163–186.

  • Van der Hoeven, G. F.: 1978, ‘Models for LS projected from a single lawless sequence and Dragalin's elimination translation’, Report 78-10, Department of Mathematics, University of Amsterdam. Part of the material in revised form in Indag. Math. 85, (1982).

  • Van der Hoeven, G. F.: 1982, ‘Projections of lawless sequences’, Ph.D. thesis, University of Amsterdam. Also in the series Mathematical Centre Tracts, Mathematisch Centrum, Amsterdam.

  • Van der Hoeven, G. F.: 1983, ‘An application of projections of lawless sequences’, to appear in Troelstra and Van Dalen (1983).

  • Van der Hoeven, G. F. and Troelstra, A. S.: 1980, ‘Projections of lawless sequences II’, in M. Boffa, D. van Dalen, and M. McAloon (eds.), Logic Colloquium 8, North-Holland, Amsterdam, pp. 265–298.

    Google Scholar 

  • Veldman, W. H. M.: 1976, ‘An intuitionistic completeness theorem for intuitionistic predicate logic’, J. Symbolic Logic 41, 159–166. Preprint: Report, Mathematisch Instituut, Katholieke Universiteit Nijmegen (1974).

    Google Scholar 

  • Veldman, W. H. M.: 1981, ‘Investigations in intuitionistic hierarchy theory’, Ph.D. thesis, Katholieke Universiteit Nijmegen. With a leaflet ‘Stellingen’.

  • Veldman, W. H. M.: 1983, ‘On the constructive contrapositions of two axioms of countable choice’, to appear in: Troelstra and Van Dalen (1983).

  • Vesley, R. E.: 1979, ‘Review of Troelstra 1977’, J. Symbolic Logic 44, 275–276.

    Google Scholar 

  • Von Neumann, J.: 1925, ‘Eine Axiomatisierung der Mengenlehre’, Journal für reine und angew. Math. 154, 219–240.

    Google Scholar 

  • Wendel, N.: 1978, ‘The inconsistency of Bernini's very strong intuitionistic theory’, Studia Logica 37, 341–347.

    Google Scholar 

  • Yessenin-Volpin, A. S.: 1970, ‘The ultra-intuitionistic criticism and the anti-traditional program for the foundations of mathematics’, in Kino et al. (1970), pp. 3–45.

  • Yessenin-Volpin, A. S.: 1981, ‘About infinity, finiteness and finitization (in connection with the foundations of mathematics)’, in Richman (1981), pp. 274–313.

  • Zermelo, E.: 1908, ‘Untersuchungen über die Grundlagen der Mengenlehre I’, Math. Annalen 65, 261–281.

    Google Scholar 

  • Zermelo, E.: 1930, ‘Über Grenzzahlen und Mengenbereiche’, Fund. Math. 16, 29–47.

    Google Scholar 

Download references

Authors

Rights and permissions

Reprints and permissions

About this article

Cite this article

Troelstra, A.S. Analysing choice sequences. J Philos Logic 12, 197–260 (1983). https://doi.org/10.1007/BF00247189

Download citation

  • Issue Date:

  • DOI: https://doi.org/10.1007/BF00247189

Navigation