Volume 7 · Number 2 · Pages 131–140

< Previous Paper · Next Paper >

Questioning Constructive Reverse Mathematics

Iris Loeb

Download the full text in
PDF (339 kB)

Abstract

Context: It is often suggested that the methodology of the programme of Constructive Reverse Mathematics (CRM) can be sufficiently clarified by a thorough understanding of Brouwer’s intuitionism, Bishop’s constructive mathematics, and classical Reverse Mathematics. In this paper, the correctness of this suggestion is questioned. Method: We consider the notion of a mathematical programme in order to compare these schools of mathematics in respect of their methodologies. Results: Brouwer’s intuitionism, Bishop’s constructive mathematics, and classical Reverse Mathematics are historical influences upon the origin and development of CRM, but do not give a full “methodological explanation” for it. Implications: Discussion on the methodological issues concerning CRM is needed. Constructivist content: It is shown that the characterisation and comparison of varieties of constructive mathematics should include methodological aspects (as understood from their practices).

Key words: constructive mathematics, reverse mathematics, mathematical programme, methodology

Citation

Loeb I. (2012) Questioning Constructive Reverse Mathematics. Constructivist Foundations 7(2): 131–140. Available at http://www.univie.ac.at/constructivism/journal/7/2/131.loeb

Export article citation data: Plain Text · BibTex · EndNote · Reference Manager (RIS)

References

Berger J. & Bridges D. S. (2006) A Bizarre Property Equivalent to the Pi01-fan theorem. Logic Journal of the IGPL 14(6): 867–871. << Google Scholar

Berger J. & Bridges D. S. (2007) A fan-theoretic equivalent of the antithesis of Specker’s theorem. Indagationes Mathematicae, New Series 18(2): 195–202. << Google Scholar

Berger J. & Bridges D. S. (2008) The anti-Specker property, a Heine-Borel property, and uniform continuity. Archive for Mathematical Logic 46 (7–8): 583–592. << Google Scholar

Berger J. & Ishihara H. (2005) Brouwer’s fan theorem and unique existence in constructive analysis. Mathematical Logic Quarterly 51(4): 360–364. << Google Scholar

Berger J. (2005) Constructive equivalents of the uniform continuity theorem. Journal UCS 11(12): 1878–1883. << Google Scholar

Berger J. (2005) The fan theorem and uniform continuity. In: Cooper S. B., Löwe B. & Torenvliet L. (eds.) New computational paradigms. Springer Lecture Notes in Computer Science 3526: 18–22. << Google Scholar

Berger J. (2006) The logical strength of the uniform continuity theorem. In: Beckmann A., Berger U., Löwe B. & Tucker J. V. (eds.) Logical approaches to computational barriers. Springer Lecture Notes in Computer Sciences 3988: 35–39. << Google Scholar

Berger J. (2008) The weak König lemma and uniform continuity. Journal of Symbolic Logic 73(3): 933–993. << Google Scholar

Berger J. (2009) A decomposition of Brouwer’s fan theorem. Journal of Logic and Analysis 1: 1–8. << Google Scholar

Berger J., Bridges D. S. & Schuster P. (2006) The fan theorem and unique existence of maxima. The Journal of Symbolic Logic 71(2): 713–720. << Google Scholar

Bishop E. & Bridges D. S. (1985) Constructive analysis. Springer, Berlin. << Google Scholar

Bishop E. (1967) Foundations of constructive analysis. McGraw-Hill, New York. << Google Scholar

Brattka V. & Gherardi G. (2011) Effective choice and boundedness principles in computable analysis. The Bulletin of Symbolic Logic, 17(1): 73–117. << Google Scholar

Bridges D. & Richman F. (1987) Varieties of constructive mathematics. Cambridge University Press, Cambridge. << Google Scholar

Bridges D. & Vîta L. (2006) Techniques of constructive analysis. Springer, Heidelberg. << Google Scholar

Bridges D. S. & Diener H. (2007) The pseudo-compactness of [0, 1] is equivalent to the uniform continuity theorem. Journal of Symbolic Logic 72(4): 1379–1384. << Google Scholar

Bridges D. S. & Diener H. (2010) The anti-Specker property, positivity, and total boundedness. Mathematical Logic Quarterly 56(4): 434–441. << Google Scholar

Bridges D. S. (2008) A reverse look at Brouwer’s fan theorem. In: van Atten M., Boldini P., Bourdeau M. & Heinzmann G. (eds.) One hundred years of intuitionism (1907–2007) Birkhäuser, Basel: 316–325. << Google Scholar

Bridges D. S. (2009) Constructive mathematics. In: Zalta E. N. (ed.) The Stanford encyclopedia of philosophy, Summer 2009 edition. Available at http://plato.stanford.edu/archives/sum2009/entries/mathematics-constructive/

Brouwer L. E. J. (1907) Over de grondslagen der wiskunde. Ph.D. thesis, University of Amsterdam. Reprinted with additional material in van Dalen D. (2001) L.E. J. Brouwer en de grondslagen van de wiskunde. Epsilon Uitgaven, Utrecht. << Google Scholar

Brouwer L. E. J. (1921) Besitzt jede reelle Zahl eine Dezimalbruchentwicklung? Mathematische Annalen 83, 201–210. << Google Scholar

Diener H. & Loeb I. (2009) Sequences of real functions on [0,1] in constructive reverse mathematics. Annals of Pure and Applied Logic 157(1): 50–61. << Google Scholar

Diener H. (2008) Compactness under constructive scrutiny. Ph.D. thesis, University of Canterbury. << Google Scholar

Diener H. (2010) Constructions and constructive reverse mathematics. Presentation at the workshop “Constructive mathematics: Proofs and computation,” 7–11 June 2010, Benedictine nunnery on Fraueninsel, Germany. Slides available at http://www.mathematik.unimuenchen.de/~cm2010/diener.pdf << Google Scholar

Ernest P. (1992) The nature of mathematics: Towards a social constructive account. Science & Education 1: 89–100. << Google Scholar

Friedman H. (1975) Some systems of second order arithmetic and their use. Proceedings of the 17th international congress of mathematicians, Vancouver BC. << Google Scholar

Iemhoff R. (2009) Intuitionism in the Philosophy of Mathematics. In: Zalta E. N. (ed.) The Stanford encyclopedia of philosophy, Winter 2009 edition. Available at http://plato.stanford.edu/archives/win2009/entries/intuitionism/

Ishihara H. & Schuster P. (2004) Compactness under constructive scrutiny. Mathematical Logic Quarterly 50(6): 540–550. << Google Scholar

Ishihara H. (1992) Continuity properties in constructive mathematics. Journal of Symbolic Logic 57(2): 557–565. << Google Scholar

Ishihara H. (2004) Informal constructive reverse mathematics. Centre for Discrete Mathematics and Theoretical Computer Science CDMTCS-229. Available at http://www.cs.auckland.ac.nz/CDMTCS/researchreports/229hajime.pdf

Ishihara H. (2005) Constructive reverse mathematics: Compactness properties. from sets and types to topology and analysis. Oxford Logic Guides. Volume 48. Oxford University Press, Oxford: 245–267. << Google Scholar

Ishihara H. (2006) Reverse mathematics in Bishop’s constructive mathematics. Philosophia Scientiae, Cahier Spécial 6: 43–59. Available at http:// philosophiascientiae.revues.org/pdf/406

Lerman S. (1989) Constructivism, mathematics and mathematics education. Educational Studies in Mathematics 20: 211–223. << Google Scholar

Loeb I. (2005) Equivalents of the (weak) fan theorem. Annals of Pure and Applied Logic 132(1): 51–66. << Google Scholar

Loeb I. (2008) Factoring out intuitionistic theorems: Continuity principles and the uniform continuity theorem. Proceedings of the 4th conference on computability in Europe 2008 (CiE 2008): 379–388. << Google Scholar

Loeb I. (2008) Indecomposability of R and R\{0} in constructive reverse mathematics. Logic Journal of the IGPL 16(3): 269–273. << Google Scholar

Loeb I. (2009) Indecomposability of negative dense subsets of R in constructive reverse mathematics. Logic Journal of the IGPL 17(2): 173–177. << Google Scholar

Mandelkern M. (1988) Limited omniscience and the Bolzano-Weierstrass principle. Bulletin of the London Mathematical Society 20, 319–320. << Google Scholar

Mandelkern M. (1989) Brouwerian counterexamples. Mathematics Magazine 62(1): 3–27. << Google Scholar

Moschovakis J. R. (2003) Classical and constructive hierarchies in extended intuitionistic analysis. Journal of Symbolic Logic 68(3): 1015–1043. << Google Scholar

Moschovakis J. R. (2008) Varieties of reverse constructive mathematics. CUNY Computational Logic Seminar. Available at http://www.math.ucla.edu/~joan/cuny08handout.pdf

Oliveri G. (2007) A realist philosophy of mathematics. College Publications, London. << Google Scholar

Sambin G. (in press) Real and ideal in constructive mathematics. In: Dybjer P., Lindström S., Palmgren E. & Sundholm G. (eds.) Epistemology versus ontology: Essays on the philosophy and foundations of mathematics in honour of Per Martin-Löf. Springer, New York. << Google Scholar

Schuster P. (2003) Unique existence, approximate solutions, and countable choice. Theoretical Computer Science 305(1–3): 433–455. << Google Scholar

Schwichtenberg H. (2005) A direct proof of the equivalence between Brouwer’s fan theorem and König’s lemma with a uniqueness hypothesis. J. UCS, 11(12): 2086–2095. << Google Scholar

Simpson S. G. (1985) Reverse mathematics. In: Nerode A. & Shore R. A. (eds.) Proceedings of the AMS-ASL summer institute on recursion theory: 461–472. << Google Scholar

Simpson S. G. (1988) Partial realizations of Hilbert’s program. Journal of Symbolic Logic 53(2): 349–363. << Google Scholar

Simpson S. G. (1999) Subsystems of second-order arithmetic. Springer, New York. << Google Scholar

Toftdal M. (2004) Calibration of ineffective theorems of analysis in a constructive context. Master’s thesis, University of Aarhus. << Google Scholar

Troelstra A. S. & van Dalen D. (1988) Constructivism in mathematics. An introduction. Volume 1. North-Holland, Amsterdam. << Google Scholar

Troelstra A. S. (1974) Note on the fan theorem. Journal of Symbolic Logic 39(3): 584–596. << Google Scholar

Troelstra A. S. (1991) History of constructivism in the 20th century. ITLI Prepublication Series ML-91–05, University of Amsterdam. << Google Scholar

van Dalen D. (1998) L. E. J. Brouwer’s intuitionism: A revolution in two installments. 13th annual IEEE symposium on logic in computer science (LICS’98): 228–241. << Google Scholar

Veldman W. (2004) Project: Intuitionistic reverse mathematics. Project description. Available at http://www.onderzoekinformatie.nl/en/oi/nod/onderzoek/OND1307986

Veldman W. (2005) Brouwer’s Fan Theorem as an axiom and as a contrast to Kleene’s alternative. Report no. 0509, IMAPP, Radboud University Nijmegen. << Google Scholar

Zach R. (2009) Hilbert’s program. In: Zalta E. N. (ed.) The Stanford encyclopedia of philosophy, Spring 2009 edition. Available at http://plato.stanford.edu/archives/spr2009/entries/hilbert-program/