Abstract
This note explores the common core of constructive, intuitionistic, recursive and classical analysis from an axiomatic standpoint. In addition to clarifying the relation between Kleene’s and Troelstra’s minimal formal theories of numbers and number-theoretic sequences, we propose some modified choice principles and other function existence axioms which may be of use in reverse constructive analysis. Specifically, we consider the function comprehension principles assumed by the two minimal theories EL and M, introduce an axiom schema CFd asserting that every decidable property of numbers has a characteristic function, and use it to describe a precise relationship between the minimal theories. We show that the axiom schema AC00 of countable choice can be decomposed into a monotone choice schema AC m00 (which guarantees that every Cauchy sequence has a modulus) and a bounded choice schema BC00. We relate various (classically correct) axiom schemas of continuous choice to versions of the bar and fan theorems, suggest a constructive choice schema AC1/2,0 (which incidentally guarantees that every continuous function has a modulus of continuity), and observe a constructive equivalence between restricted versions of the fan theorem and correspondingly restricted bounding axioms \({AB_{1/2,0}^{2^{\mathbb{N}}}}\). We also introduce a version WKL!! of Weak König’s Lemma with uniqueness which is intermediate in strength between WKL and the decidable fan theorem FTd.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
Berger, J.: A separation result for varieties of Brouwer’s fan theorem. In: Arai, T., et al. (eds.) Proceedings of the 10th Asian Logic Conference, pp. 85–92, Kobe, Japan, World Scientific (2010)
Berger J., Ishihara H.: Brouwer’s fan theorem and unique existence in constructive analysis. Math. Log. Quart. 51, 360–364 (2005)
Bridges, D.: A reverse look at Brouwer’s fan theorem. In: One hundred years of intuitionism (1907–2007), The Cerisy Conference. Springer, Berlin, pp. 316–325 (2008)
Bridges D., Richman F.: Varieties of Constructive Mathematics. Cambridge University Press, Cambridge (1987)
Diener H., Loeb I.: Sequences of real functions on [0,1] in constructive reverse mathematics. Ann. Pure Appl. Logic 157, 50–61 (2009)
Heyting, A.: Die formalen regeln der intuitionistischen logik, Sitzber. Preuss. Akad. Wiss. (phys.-math. Klasse), Berlin (1930), 42–56, English trans. in Mancosu, P., From Brouwer to Hilbert, Oxford 1998, 311–327 (1998)
Heyting, A.: Die formalen regeln der intuitionistischen mathematik II, Sitzber. Preuss. Akad. Wiss. (phys.-math. Klasse), Berlin 57–71 (1930)
Heyting, A.: Sur la logique intuitionniste. Bull. Acad. Royale Belgique 16, 957–963 (1930), English trans. by A. Rocha in Mancosu, P., op. cit., 306–310 (1930)
Ishihara H.: Constructive reverse mathematics: compactness properties. In: Crosilla, L., Schuster, P. (eds) From Sets and Types to Topology and Analysis: Towards Practicable Foundations for Constructive Mathematics, pp. 245–267. Oxford University Press, Oxford (2005)
Kleene S.C.: Introduction to Metamathematics. van Nostrand, Princeton (1952)
Kleene, S.C.: Formalized recursive functionals and formalized realizability, Memoirs, no. 89. Amer. Math. Soc. (1969)
Kleene S.C., Vesley R.E.: The foundations of intuitionistic mathematics, especially in relation to recursive functions. North Holland, Amsterdam (1965)
Loeb I.: Equivalents of the (weak) fan theorem. Ann. Pure Appl. Logic 132, 51–66 (2005)
Moschovakis J.R.: Can there be no nonrecursive functions. Jour. Symb. Logic 36, 309–315 (1971)
van Oosten J.: Lifschitz’ realizability. Jour. Symb. Logic 55, 805–821 (1990)
Schwichtenberg H.: A direct proof of the equivalence between Brouwer’s fan theorem and König’s lemma with a uniqueness hypothesis. Jour. Univers. Comp. Sci. 11, 2086–2095 (2005)
Troelstra, A.S.: Intuitionistic formal systems. In: Troelstra, A.S. (ed.) Metamathematical Investigation of Intuitionistic Arithmetic and Analysis. Lecture Notes in Math., Springer, Berlin (1973)
Troelstra A.S.: Note on the fan theorem. Jour. Symb. Logic 39, 584–596 (1974)
Troelstra A.S., van Dalen D.: Constructivism in Mathematics: An Introduction, Volumes I and II. North-Holland, Amsterdam (1988)
Veldman, W.: Brouwer’s approximate fixed-point theorem is equivalent to Brouwer’s fan theorem. In: Lindstrom, S., et al. (ed.) Logicism, Intuitionism, and Formalism, Synthese Library 341, pp. 277–299. Springer, Netherlands (2009)
Weinstein S.: Some applications of Kripke models to formal systems of intuitionistic analysis. Ann. Math. Logic 16, 1–32 (1979)
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Moschovakis, J.R., Vafeiadou, G. Some axioms for constructive analysis. Arch. Math. Logic 51, 443–459 (2012). https://doi.org/10.1007/s00153-012-0273-z
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00153-012-0273-z