Abstract
Brouwer was a founder of intuitionism and he developed intuitionistic mathematics in 1920’s. In particular, he proved the uniform continuity theorem using the fan theorem in 1927, which was derived from a stronger theorem called bar induction. For this principle Brouwer gave a justification which was an important source of BHK-interpretation, but it depends on an assumption which we call “the fundamental assumption” (FA). Since FA was neither explained or justified, many people have thought that Brouwer’s argument is highly controversial. In this paper, we propose a way of formalizing Brouwer’s argument using a method in infinitary proof theory. Also, based on our formalization, we give an explanation and justification of FA from the viewpoint of the practice of intuitionistic mathematics.
This work is partially supported by JSPS KAKENHI 16K16690, 17H02265, and Core-to-Core Program (A. Advanced Research Networks). We would like to thank Yasuo Deguchi, Takashi Iida, Mitsuhiro Okada, and Yuta Takahashi for their helpful comments. Special thanks go to Sam Sanders for his encouragement and organizing an opportunity of presenting this paper at Munich Center for Mathematical Philosophy. Moreover, important feedbacks from people working on constructive mathematics and proof-theory in the department of mathematics of LMU München were very helpful for finishing this paper.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Akiyoshi, R.: An interpretation of Brouwer’s argument for bar theorem via infinitary proof theory. In: Abstract Volume of XXIII World Congress of Philosophy, p. 18 (2013)
Akiyoshi, R.: An ordinal-free proof of the complete cut-elimination theorem for \(\Pi ^{1}_{1}\)-\(CA\) + \(BI\) with the \(\omega \)-rule. In: Gabbay, D., Prosorov, O., (eds.) The Mints’ Memorial Issue of IfCoLog Journal of Logics and Their Applications, pp. 867–884 (2017)
Akiyoshi, R., Terui, K.: Strong normalization for the parameter-free polymorphic lambda calculus based on the omega-rule. In: First International Conference on Formal Structures for Computation and Deduction (FSCD), Leibniz International Proceedings in Informatics, vol. 52 (2016)
Akiyoshi, R., Mints, G.: An extension of the omega-rule. Arch. Math. Log. 55(3), 593–603 (2016)
Berger, J.: The logical strength of the uniform continuity theorem. In: Beckmann, A., Berger, U., Löwe, B., Tucker, J.V. (eds.) CiE 2006. LNCS, vol. 3988, pp. 35–39. Springer, Heidelberg (2006). https://doi.org/10.1007/11780342_4
Brouwer, L.E.J.: Über definitionsbereiche von funktionen. Math. Ann. 97, 60–75 (1927). English translation with introduction by Charles Parsons in [22]
Buchholz, W.: The \(\Omega_{\mu +1}\)-rule. In: Buchholz, W., Feferman, S., Pohlers, W., Sieg, W. (eds.) Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-Theoretical Studies. Lecture Notes in Mathematics, vol. 897, pp. 188–233. Springer, Heidelberg (1981). https://doi.org/10.1007/BFb0091894
Buchholz, W.: Explaining the Gentzen-Takeuti reduction steps. Arch. Math. Log. 40, 255–272 (2001)
Dummett, M.A.E.: Frege: Philosophy of Language, 2nd edn. Duckworth, London (1993)
Dummett, M.A.E.: Elements of Intuitionism, 2nd edn. Oxford University Press, Oxford (2000). Volume 39 of Oxford Logic Guides
Kreisel, G., Howard, W.: Transfinite induction and bar induction of types zero and one, and the role of continuity in intuitionistic analysis. J. Symb. Log. 31, 325–358 (1966)
Iemhoff, R.: Intuitionism in the philosophy of mathematics. In: Zalta, E.N. (ed.) The Stanford Encyclopedia of Philosophy. Summer 2013 Edition. https://plato.stanford.edu/entries/intuitionism/
Kreisel, G., Troelstra, A.S.: Formal systems for some branches of intuitionistic analysis. Ann. Math. Log. 1, 229–387 (1970)
Maietti, M., Sambin, G.: Why topology in the minimalist foundation must be pointfree. Log. Log. Philos. 22, 167–199 (2013)
Martino, E., Giaretta, P.: Brouwer, Dummett and the bar theorem. In: Atti del Congresso nazionale di logica, Montecatini Terme, 1–5 ottobre 1979, a cura di Sergio Bernini, Bibliopolis, Napoli, pp. 541–558 (1981)
de Lavalette, G.R.R.: Extended bar induction in applicative theories. Ann. Pure Appl. Log. 50, 139–189 (1990)
Sambin, G.: The Basic Picture: Structures for Constructive Topology. Oxford University Press, to be published
Schwichtenberg, H., Troelstra, A.S.: Basic Proof Theory, 2nd edn. Cambridge University Press, Cambridge (2000)
Tait, W.W.: Infinitely long terms of transfinite type. In: Crossley, J.N., Dummet, M. (eds.) Formal Systems and Recursive Functions, pp. 176–185, North-Holland (1965)
van Atten, M.: The development of intuitionistic logic. In: Zalta, E.N. (ed.) The Stanford Encyclopedia of Philosophy. Autumn 2017 Edition. https://plato.stanford.edu/entries/intuitionistic-logic-development/
van Atten, M.: Predicativity and parametric polymorphism of Brouwerian implication. Preprint in Arxiv (2017). https://arxiv.org/abs/1710.07704
van Heijenoort, J. (ed.): From Frege to Gödel: A Source Book in Mathematical Logic, pp. 1879–1931. Harvard University Press, Cambridge (1967)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer-Verlag GmbH Germany, part of Springer Nature
About this paper
Cite this paper
Akiyoshi, R. (2018). A Formalization of Brouwer’s Argument for Bar Induction. In: Moss, L., de Queiroz, R., Martinez, M. (eds) Logic, Language, Information, and Computation. WoLLIC 2018. Lecture Notes in Computer Science(), vol 10944. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-57669-4_4
Download citation
DOI: https://doi.org/10.1007/978-3-662-57669-4_4
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-57668-7
Online ISBN: 978-3-662-57669-4
eBook Packages: Computer ScienceComputer Science (R0)
