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 ?". In recent years, my interest has expanded into other areas such as the Kyoto school, smart cities, robot ethics, and natural language processing.

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, j.w.w. Grigori Mints in Stanford Uni.) and theoretical computer science (type theory, j.w.w. Kazushige Terui in RIMS, Kyoto Uni.) 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. Recently, I'm working on a project to develop proof-theoretic semantics for mathematics (j.w.w. Alberto Naibo, Paris).

Moreover, I'm interested in the formalization of mathematics using Coq/Isabelle and in the question "what is a proof ?" from a computer science/natural language processing point of view (j.w.w. Koji Mineshima, Keio Uni.). These are based on my philosophical or historical interest in early Husserl's logical philosophy, for example, in his "Logische Undersuchungen" (j.w.w. Genki Uemura, Okayama Uni.).

Recently, I have been working on a project on Gaisi Takeuti's mathematical philosophy, who is one of Japan's leading logicians (j.w.w. Andrew Arana, Lorraine). The aim of this project is to describe his philosophical view paying attention to his philosophical background (especially the philosophy of Nishida Kitaro). As a related research, I started to work on a project to apply the philosophy of self developed in the East to digital twin and VR (j.w.w. the group of Yasuo Deguchi, Kyoto Uni.). Moreover, I am also strongly interested in applying this kind of philosophy to the real world, including working with the group of Yasuo Deguchi.

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),
(ix) Gaisi Takeuti's mathematical philosophy,
(x) logic of the digital twin and VR (intentionality),
(xi) alternatives to the "Master-Slave Model" in robot ethics,
(xii) industry-academia-government collaboration project on smart city,
(xiii) discourse relations in Japanese and analysis of informal proof focusing on inferential relations.