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.

First International Conference on Formal Structures for Computation and Deduction (FSCD), Leibniz International Proceedings in Informatics Jun 2016 [Refereed]