Equivalents of the (weak) fan theorem (Q703836): Difference between revisions

The author proves that several theorems are equivalent to the fan theorem over an intuitionistic base system. The base system, WKV, is a weakened version of an axiom system used by \textit{S. C. Kleene} and \textit{R. E. Vesley} [The foundations of intuitionistic mathematics. Especially in relation to recursive functions. Amsterdam: North-Holland Publishing Company (1965; Zbl 0133.24601)]. Theorems that are shown to be equivalent to the fan theorem include the Heine-Borel theorem for \([0,1]\), various properties of continuous functions on closed intervals (uniform continuity, Riemann integrability, and boundedness), the Lindenbaum Lemma, and completeness and compactness theorems of propositional calculus. Intuitionistically, the fan theorem is not equivalent to weak König's lemma, so the preceding results are distinct from the parallel results of reverse mathematics as presented by \textit{S. G. Simpson} [Subsystems of second order arithmetic. Berlin: Springer (1999; Zbl 0909.03048)].