We investigate which part of Brouwer’s Intuitionistic Mathematics is finitistically justifiable or guaranteed in Hilbert’s Finitism, in the same way as similar investigations on Classical Mathematics already done quite extensively in proof theory and reverse mathematics. While we already knew a contrast from the classical situation concerning the continuity principle, more contrasts turn out: we show that several principles are finitistically justifiable or guaranteed which are classically not. Among them are: fan theorem for decidable fans but arbitrary bars; continuity principle (...) and the axiom of choice both for arbitrary formulae; and $\Sigma _2$ induction and dependent choice. We also show that Markov’s principle MP does not change this situation; that neither does lesser limited principle of omniscience LLPO ; but that limited principle of omniscience LPO makes the situation completely classical. (shrink)

In the context of constructive reverse mathematics, we show that weak Kőnig's lemma () implies that every pointwise continuous function is induced by a code in the sense of reverse mathematics. This, combined with the fact that implies the Fan theorem, shows that implies the uniform continuity theorem: every pointwise continuous function has a modulus of uniform continuity. Our results are obtained in Heyting arithmetic in all finite types with quantifier‐free axiom of choice.

Dini's theorem says that compactness of the domain, a metric space, ensures the uniform convergence of every simply convergent monotone sequence of real-valued continuous functions whose limit is continuous. By showing that Dini's theorem is equivalent to Brouwer's fan theorem for detachable bars, we provide Dini's theorem with a classification in the recently established constructive reverse mathematics propagated by Ishihara. As a complement, Dini's theorem is proved to be equivalent to the analogue of the fan theorem, weak König's lemma, in (...) the original classical setting of reverse mathematics started by Friedman and Simpson. (shrink)

We provide a fine‐grained analysis on the relation between König's lemma, weak König's lemma, and the decidable fan theorem in the context of constructive reverse mathematics. In particular, we show that double negated variants of König's lemma and weak König's lemma are equivalent to double negated variants of the general decidable fan theorem and the binary decidable fan theorem, respectively, over a nearly intuitionistic system containing a weak countable choice only. This implies that the general decidable fan theorem is not (...) equivalent to the binary decidable fan theorem in the absence of a strong countable choice. In addition, we introduce a principle which fills the gap between König's lemma and weak König's lemma, and show that König's lemma is equivalent to weak König's lemma plus this principle. We also solve several problems arising from the investigation. (shrink)

We prove constructively that the weak König lemma and quantifier-free number-number choice imply that every pointwise continuous function from Cantor space into Baire space has a modulus of uniform continuity.

We introduce the notion of a convex tree. We show that the binary expansion for real numbers in the unit interval ) is equivalent to weak König lemma ) for trees having at most two nodes at each level, and we prove that the intermediate value theorem is equivalent to \ for convex trees, in the framework of constructive reverse mathematics.