The Weak Kőnig Lemma, Brouwer’s Fan Theorem, De Morgan’s Law, and Dependent Choice

Josef Berger; Hajime Ishihara; Peter Schuster

Titles

Abstract

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 Konig 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.

References

[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. Raﬀalli, Introduction `a la logique. Th´eorie de la d´emonstration. 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¨onig 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 ﬁnite 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, Inﬁnite 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, Paciﬁc 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 theorem and 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 ineﬀective 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.

Information

Information: Reports on Mathematical Logic, 2012, Number 47, pp. 63 - 86

DOI: https://doi.org/10.4467/20842589RM.12.003.0684

Article type: Original article

Titles:

Polish:

The Weak Kőnig Lemma, Brouwer’s Fan Theorem, De Morgan’s Law, and Dependent Choice

English:

The Weak Kőnig Lemma, Brouwer’s Fan Theorem, De Morgan’s Law, and Dependent Choice

Authors

Josef Berger

Ludwig-Maximilians-Universität München

Hajime Ishihara

Japan Advanced Institute of Science and Technology, Nomi, Ishikawa, Japan

Peter Schuster

Dipartimento di Informatica, Università degli Studi di Verona Strada le Grazie 15, 37134 Verona, Italy

Leeds University

Published at: 23.08.2012

Article status: Open

Licence: None

Percentage share of authors:

Josef Berger (Author) - 33%

Hajime Ishihara (Author) - 33%

Peter Schuster (Author) - 34%

Article corrections:

-

Publication languages:

English

View count: 2722

Number of downloads: 1934

<p> The Weak Kőnig Lemma, Brouwer’s Fan Theorem, De Morgan’s Law, and Dependent Choice</p>

Pobierz pełny tekst

Titles

Abstract

References

Information

Authors