20 citations · 30 across the 14 of their papers we have counts for
8 papers · 1 filter
The strength of the minimum principle in constructive reverse mathematics
Tatsuji Kawai
The minimum principle states that every real-valued uniformly continuous function f : X -> R on a compact metric space X attains its minimum. Working in the base system EL0 of cons…
Constructive equivalence between Brouwer's fixed-point theorem and weak König's lemma
Tatsuji Kawai
In the context of constructive reverse mathematics, we show that Brouwer's fixed-point theorem and weak König's lemma (WKL) are equivalent. To derive WKL from Brouwer's fixed-point…
Decidable fan theorem and uniform continuity theorem with continuous moduli
Makoto Fujiwara, Tatsuji Kawai
The uniform continuity theorem (UCT) states that every pointwise continuous real-valued function on the unit interval is uniformly continuous. In constructive mathematics, UCT is s…
Equivalents of the finitary non-deterministic inductive definitions
Ayana Hirata, Hajime Ishihara, Tatsuji Kawai +1
We present statements equivalent to some fragments of the principle of non-deterministic inductive definitions (NID) by van den Berg (2013), working in a weak subsystem of construc…
Representing definable functions of by neighbourhood functions
Tatsuji Kawai
Brouwer (1927) claimed that every function from the Baire space to natural numbers is induced by a neighbourhood function whose domain admits bar induction. We show that Brouwer's…
A continuity principle equivalent to the monotone fan theorem
Tatsuji Kawai
The strong continuity principle reads "every pointwise continuous function from a complete separable metric space to a metric space is uniformly continuous near each compact image.…
Principles of bar induction and continuity on Baire space
Tatsuji Kawai
Brouwer-operations, also known as inductively defined neighbourhood functions, provide a good notion of continuity on Baire space which naturally extends that of uniform continuity…
Formally continuous functions on Baire space
Tatsuji Kawai
A function from Baire space to the natural numbers is called formally continuous if it is induced by a morphism between the corresponding formal spaces. We compare formal continuit…