1. The Fan Theorem, its strong negation, and the determinacy of games.
- Author
-
Veldman, Wim
- Abstract
In the context of a weak formal theory called Basic Intuitionistic Mathematics BIM\documentclass[12pt]{minimal}\usepackage{amsmath}\usepackage{wasysym}\usepackage{amsfonts}\usepackage{amssymb}\usepackage{amsbsy}\usepackage{mathrsfs}\usepackage{upgreek}\setlength{\oddsidemargin}{-69pt}\begin{document}$$\textsf{BIM}$$\end{document}, we study Brouwer’s
Fan Theorem and a strong negation of the Fan Theorem,Kleene’s Alternative (to the Fan Theorem) . We prove that the Fan Theorem is equivalent tocontrapositions of a number of intuitionistically accepted axioms of countable choice and that Kleene’s Alternative is equivalent tostrong negations of these statements. We discuss finite and infinite games and introduce a constructively useful notion ofdeterminacy . We prove that the Fan Theorem is equivalent to theIntuitionistic Determinacy Theorem . This theorem says that every subset of Cantor space 2ω\documentclass[12pt]{minimal}\usepackage{amsmath}\usepackage{wasysym}\usepackage{amsfonts}\usepackage{amssymb}\usepackage{amsbsy}\usepackage{mathrsfs}\usepackage{upgreek}\setlength{\oddsidemargin}{-69pt}\begin{document}$$2^\omega $$\end{document} is, in our constructively meaningful sense, determinate. Kleene’s Alternative is equivalent to a strong negation of a special case of this theorem. We also consider auniform intermediate value theorem and acompactness theorem for classical propositional logic . The Fan Theorem is equivalent to each of these theorems and Kleene’s Alternative is equivalent to strong negations of them. We end with a note on‘stronger’ Fan Theorems. The paper is a sequel to Veldman (Arch Math Logic 53:621–693, 2014). [ABSTRACT FROM AUTHOR]- Published
- 2024
- Full Text
- View/download PDF