Brouwer's fan theorem as an axiom and as a contrast to Kleene's alternative (Q403410)

From MaRDI portal





scientific article; zbMATH DE number 6335990
Language Label Description Also known as
default for all languages
No label defined
    English
    Brouwer's fan theorem as an axiom and as a contrast to Kleene's alternative
    scientific article; zbMATH DE number 6335990

      Statements

      Brouwer's fan theorem as an axiom and as a contrast to Kleene's alternative (English)
      0 references
      0 references
      29 August 2014
      0 references
      The author has based his paper on a tailor-made formal system, called Basic Intuitionistic Mathematics (BIM), which resembles \textit{W. A. Howard} and \textit{G. Kreisel}'s system H [J. Symb. Log. 31, 325--358 (1966; Zbl 0156.00804)] and \textit{A. S. Troelstra} and \textit{D. van Dalen}'s system EL [Constructivism in mathematics. An introduction. Volume I. Amsterdam etc.: North-Holland (1988; Zbl 0653.03040); Constructivism in mathematics. An introduction. Volume II. Amsterdam etc.: North-Holland (1988; Zbl 0661.03047)]. On this basis, he gives numerous equivalents of Brouwer's fan theorem and of Kleene's alternative. Variants of Dini's theorem on the uniform convergence of sequences of continuous functions play a prominent role, as do adequate variations of `compact' and of its negation.
      0 references
      Brouwer's fan theorem
      0 references
      Kleene's alternative
      0 references
      intuitionistic reverse mathematics
      0 references
      compact
      0 references
      positively non-compact
      0 references
      closed-and-separable
      0 references
      Baire space
      0 references
      real numbers
      0 references
      0 references
      0 references
      0 references
      0 references
      0 references
      0 references
      0 references
      0 references
      0 references
      0 references
      0 references
      0 references
      0 references
      0 references
      0 references
      0 references
      0 references
      0 references
      0 references
      0 references

      Identifiers

      0 references
      0 references
      0 references
      0 references
      0 references
      0 references
      0 references
      0 references
      0 references