Profile Information

Waseda Institute for Advanced Study Adjunct Researcher
(Concurrent) Faculty of Letters, Arts and Sciences
(Concurrent) Faculty of Science and Engineering
Keio University Faculty of Letters Part-time lecturer
Université Paris 1 L'Institut d'Histoire et de Philosophie des Sciences et des Techniques Associate Member
Meiji University School of Arts and Letters
The University of Tokyo College of Arts and Sciences
PhD (Philosophy)(3 2010 Keio University)

Contact information
Researcher number

External link

My research fields are philosophy of mathematics and logic, mathematical logic (proof theory), and theoretical computer science (type theory). The main philosophical question in my research is "what is a proof ?".

The origin of modern philosophy of mathematics was the foundational debate in the beginning of 20th century. This debate had involved mathematicians, logicians, and philosophers. After this debate, many philosophical works have been done independently of the modern development of mathematical logic. I'm doing philosophy of logic and mathematics, mathematical logic (proof theory) and theoretical computer science (type theory) in the way that they are essentially related to one another. In particular, by analyzing finitism (Hilbert), intuitionism (Brouwer), and logicism (Frege) by proof-theoretic methods, I would like to find a common base for these seemingly different positions in philosophy of mathematics.

More recently, I'm interested in the formalization of mathematics using Coq or Minlog and in the question "what is a proof ?" from this point of view too. These are based on my philosophical or historical interest in early Husserl's logical philosophy (for example, his "Logische Undersuchungen"). Moreover, I started to work on Gaisi Takeuti's finitism behind his proof theoretic works and cyber security as an application of proof theory.

Research Topics:

(i) Goedel's theorem and Hilbert's program,
(ii) Gentzen's consistency proofs,
(iii) Brouwer's proof of bar induction,
(iv) early Husserl's philosophy of logic,
(v) proof theoretic analysis of Frege's logical system,
(vi) the meaning of logical constants, proof theoretic semantics,
(vii) proof theory of impredicative subsystems of second-order arithmetic, ordinal analysis (cut-elimination, normalization theorem),
(viii) intuitionistic analysis (point-free topology),
(xi) Gaisi Takeuti's finitism,
(x) cyber security as an application of proof theory.

Committee Memberships


Books and Other Publications








Research Projects