3 citations · 3 across the 7 of their papers we have counts for
15 papers
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…
Reflexive combinatory algebras
Marlou M. Gijzen, Hajime Ishihara, Tatsuji Kawai
We introduce the notion of reflexivity for combinatory algebras. Reflexivity can be thought of as an equational counterpart of the Meyer-Scott axiom of combinatory models, which in…
Predicative theories of continuous lattices
Tatsuji Kawai
We introduce a notion of strong proximity join-semilattice, a predicative notion of continuous lattice which arises as the Karoubi envelop of the category of algebraic lattices. St…
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…