The weak König Lemma, Brouwer fan theorem, De Morgan's Law, and dependent choice

• Autorzy: Berger J. , Ishihara H. , Schuster P.
• Języki publikacji: EN

Abstrakty

EN

The standard omniscience principles are interpreted in a systematic way within the context of binary trees. With this dictionary at hand we revisit the weak König lemma (WKL) and Brouwer's fan theorem (FAN). We first study how one can arrive from FAN at WKL, and then give a direct decomposition, without coding, of WKL into the lesser limited principle of omniscience and an instance of the principle of dependent choices. As a complement we provide, among other equivalents of the standard omniscience principles, a uniform method to formulate most of them.

• Wydawca: Wydawnictwo Uniwersytetu Jagiellońskiego
• Czasopismo: Reports on Mathematical Logic
• Rocznik: 2012
• Tom: Vol. 47
• Strony: 63--86
• Opis fizyczny: Bibliogr. 35 poz.

Twórcy

autor

Berger J.

autor

Ishihara H.

autor

Schuster P.

• Mathematisches Institut, Universität München, Theresienstraße 39, 80333 München, Germany. Current address: Universität Greifswald, Institut fr Mathematik und Informatik, Walther-Rathenau-Straße 47, 17487 Greifswald, Germany,

Bibliografia

• [1] Y. Akama, S. Berardi, S. Hayashi, and U. Kohlenbach, An arithmetical hierarchy of the law of excluded middle and related principles. 19th IEEE Symposium on Logic in Computer Science (LICS 2004). Proceedings. IEEE Computer Society, 2004, pp. 192–201.
• [2] E. Bishop, Foundations of Constructive Analysis. McGraw–Hill, New York, 1967.
• [3] E. Bishop and D. Bridges, Constructive Analysis. Springer, Berlin etc., 1985.
• [4] S. Berardi, Some intuitionistic equivalents of classical principles for degree 2 formulas, Ann. Pure Appl. Logic 139 (2006), pp. 185–200.
• [5] J. Berger, D. Bridges, and P. Schuster, The fan theorem and unique existence of maxima, J. Symbolic Logic 71 (2006), pp. 713–720.
• [6] J. Berger and H. Ishihara, Brouwer’s fan theorem and unique existence in constructive analysis, Math. Log. Quart. 51 (2005), pp. 369–373.
• [7] J. Berger and P. Schuster, Classifying Dini’s theorem, Notre Dame J. Formal Logic 47 (2006), pp. 253–262.
• [8] D. Bridges and F. Richman, Varieties of Constructive Mathematics. Cambridge University Press, 1987.
• [9] D. Bridges and L. Vˆıt¸˘a, Techniques of Constructive Analysis. Springer, New York, 2006.
• [10] D. van Dalen, Logic and structure. 4th ed., Springer, Berlin, 2004.
• [11] R. David, K. Nour, and C. Raffalli, Introduction á la logique. Th´eorie de la demonstration. 2nd ed., Dunod, Paris, 2001.
• [12] N. Gambino and P. Schuster, Spatiality for formal topologies, Math. Structures Comput. Sci. 17 (2007), pp. 65–80.
• [13] H. Ishihara, An omniscience principle, the König lemma and the Hahn–Banach theorem, Z. Math. Logik Grundlag. Math. 36 (1990), pp. 237–240.
• [14] H. Ishihara, Markov’s principle, Church’s thesis and Lindel¨of ’s theorem,Indag. Math. (N.S.) 4 (1993), pp. 321–325.
• [15] H. Ishihara, Constructive reverse mathematics: compactness properties. In: L.Crosilla, P. Schuster, eds., From Sets and Types to Topology and Analysis. Oxford Logic Guides 48. Oxford University Press, 2005, pp. 245–267.
• [16] H. Ishihara, Weak K¨onig’s lemma implies Brouwer’s fan theorem: a direct proof,Notre Dame J. Formal Logic 47 (2006), pp. 249–252.
• [17] Kleene, S.C., Recursive functions and intuitionistic mathematics. In: L.M. Graves et al., eds., Proceedings of the International Congress of Mathematicans 1950.Amer. Math. Soc., Providence, R.I., 1952, pp. 679–685
• [18] I. Loeb, Equivalents of the (weak) fan theorem, Ann. Pure Appl. Logic 132 (2005),pp. 51–66.
• [19] I. Loeb, Indecomposability of R and R \ {0} in constructive reverse mathematics,Logic J. IGPL 16 (2008), pp. 269–273.
• [20] M. Mandelkern, Constructively complete finite sets, Z. Math. Logik Grundlag. Math.34 (1988), pp. 97–103.
• [21] R. Mines, W. Ruitenburg, and F. Richman, A Course in Constructive Algebra.Springer, New York, 1987.
• [22] T. Nemoto, Determinacy of Wadge classes and subsystems of second order arithmetic , MLQ Math. Log. Q. 55 (2009), pp. 154–176.
• [23] T. Nemoto, Complete determinacy and subsystems of second order arithmetic. In: Logic and theory of algorithms, Lecture Notes in Comput. Sci. 5028, Springer,Berlin, 2008, pp. 457–466.
• [24] T. Nemoto, M. Ould MedSalem, and K. Tanaka, Infinite games in the Cantor space and subsystems of second order arithmetic, MLQ Math. Log. Q. 53 (2007), pp. 226–236.
• [25] F. Richman, The fundamental theorem of algebra: a constructive development without choice, Pacific J. Math. 196 (2000), pp. 213–230.
• [26] F. Richman, Constructive mathematics without choice. In: P. Schuster et al., eds., Reuniting the Antipodes. Constructive and Nonstandard Views of the Continuum.Kluwer, Dordrecht, 2001, pp. 199–205.
• [27] F. Richman, Spreads and choice in constructive Mathematics, Indag. Math. (N.S.)13 (2002), pp. 259–267.
• [28] P. Schuster, Unique solutions, Math. Log. Quart. 52 (2006), pp. 534–539. Corrigendum: Math. Log. Quart. 53 (2007), p. 214.
• [29] H. Schwichtenberg, A direct proof of the equivalence between Brouwer’s fan theoremmand K¨onig’s lemma with a uniqueness hypothesis, J. UCS 11 (2005), pp. 2086–2095.
• [30] H. Schwichtenberg and S.S.Wainer, Proofs and Computations. Association for Symbolic Logic and Cambridge University Press, 2012.
• [31] S.G. Simpson, Subsystems of Second Order Arithmetic, Springer, Berlin etc., 1999.
• [32] M. Toftdal, A calibration of ineffective theorems of analysis in a hierarchy of semi-classical logical principles. In: 31st International Colloquium on Automata,Languages and Programming (ICALP 2004). Proceedings. Lecture Notes in Comput. Sci. 3142, Springer, 2004, pp. 1188–1200.
• [33] A.S. Troelstra and D. van Dalen, Constructivism in Mathematics. Two volumes.North–Holland, Amsterdam, 1988.
• [34] A. S. Troelstra and H. Schwichtenberg, Basic Proof Theory, 2nd edition, Cambridge University Press, 2000.
• [35] W. Veldman, Brouwer’s fan theorem as an axiom and as a contrast to Kleene’s alternative. Preprint, Radboud University, Nijmegen, 2005.