ISHIHARA, Hajime
Professor

School of Information Science, Intelligent Robotics Area, Research Center for Theoretical Computer Science

School of Information Science, Intelligent Robotics Area, Research Center for Theoretical Computer Science

B.S., M.S. and Ph.D.from Tokyo Institute of Technology (1980,1987,1990) 東京工業大学

2010 - : Japan Advanced Institute of Science and Technology , School of Information Science , Professor

1992 - 2010 : Japan Advanced Institute of Science and Technology , School of Information Science , Associate Professor

1988 - 1992 : Hiroshima University , School of Integrated Arts and Sciences , Associate

1980 - 1984 : Mitsubishi Research Institute, Inc.

1992 - 2010 : Japan Advanced Institute of Science and Technology , School of Information Science , Associate Professor

1988 - 1992 : Hiroshima University , School of Integrated Arts and Sciences , Associate

1980 - 1984 : Mitsubishi Research Institute, Inc.

Applied mathematics and statistics, Basic mathematics

intuitionistic logic, reverse mathematics, constructive set theory, 計算論, 数理論理学, 構成的数学

**Constructive Mathematics**

We have been exploring constructive mathematics as mathematics with intuitionistic logic which originated in Brouwer’s intuitionistic mathematics and formalized by Heyting and Kolmogorov. We have been dealing with constructive functional analysis such as theory of Hilbert and Banach spaces and theory of distributions, and with constructive topological spaces such as neighbourhood spaces, formal topology, and basic pair. As a foundation of constructive mathematics, we have also been studying constructive set theory (CZF) which is a predicative system and has a quite natural interpretation in Martin-Loef type theory. Furthermore, we have been advocating, and leading a research on, constructive reverse mathematics which aims at classifying, arranging and systematizing mathematical theorems, in classical mathematics, Brouwer’s intuitionistic mathematics and constructive recursive mathematics developed under different philosophies of mathematics, by logical principles and/or function existence axioms from a uniform point of view.

**Mathematical Logic**

We have been studying proof theory and semantics of intuitionisitc logic. Since there is a natural correspondence, called the Curry-Howard correspondence, between proofs in intuitionistic logic and programs (terms of lambda-calculus), we are able to extract programs from proofs in intuitionistic logic, and program extraction systems, based on this fact, such as the Minlog system at University of Munich, has been developed. We have been dealing with relationship between classical logic and intuitionistic logic, and doing a research on extracting programs from constructive contents of classical proofs. Also we have been studying proof theory and semantics of substructural logics such as linear logic.

**Theory of Computation**

We have been studying computability theory and computational complexity theory, and relationship between them and constructive mathematics. We have been characterizing classes of computable functions, such as the class of polynomial time computable functions, as function algebras, and trying to explore relationship between computational complexity and degrees of unsolvability, and logical principles and function existence axioms in constructive reverse mathematics. Furthermore, we have been dealing with lambda-calculus and type theory such as simple types, intersection types and union types.

#### ■Publications

On the independence of premiss axiom and rule

Hajime Ishihara, Takako Nemoto

Archive for Mathematical Logic, 59, 7-8, 793-815, 2020

Hajime Ishihara, Takako Nemoto

Archive for Mathematical Logic, 59, 7-8, 793-815, 2020

Equivalents of the finitary non-deterministic inductive definitions

Ayana Hirata, Hajime Ishihara, Tatsuji Kawai, Takako Nemoto

Annals of Pure and Applied Logic, 170, 10, 1256-1272, 2019

Ayana Hirata, Hajime Ishihara, Tatsuji Kawai, Takako Nemoto

Annals of Pure and Applied Logic, 170, 10, 1256-1272, 2019

The Monotone Completeness Theorem in Constructive Reverse Mathematics

Hajime Ishihara, Takako Nemoto

Mathesis Universalis, Computability and Proof, 101-112, 2019

Hajime Ishihara, Takako Nemoto

Mathesis Universalis, Computability and Proof, 101-112, 2019

The binary expansion and the intermediate value theorem in constructive reverse mathematics

Josef Berger, Hajime Ishihara, Takayuki Kihara, Takako Nemoto

Archive for Mathematical Logic, 58, 1-2, 203-217-, 2019

Josef Berger, Hajime Ishihara, Takayuki Kihara, Takako Nemoto

Archive for Mathematical Logic, 58, 1-2, 203-217-, 2019

Constructive Functional Analysis: An Introduction

Hajime Ishihara

Proof and Computation, 109-165, 2018

Hajime Ishihara

Proof and Computation, 109-165, 2018

A monad on the combinatory algebras

Operations, Sets, and Types, Muenchenwiler, Switzerland, 2016

Operations, Sets, and Types, Muenchenwiler, Switzerland, 2016

Constructive reverse mathematics: an introduction and recent results

Frontiers of Non-Classicality: Logic, Mathematics, Philosophy, Auckland, New Zealand, 2016

Frontiers of Non-Classicality: Logic, Mathematics, Philosophy, Auckland, New Zealand, 2016

Constructive reverse mathematics and omniscience pringiples

14th Asian Logic Conference, Munbai, India, 2015

14th Asian Logic Conference, Munbai, India, 2015

Intuitionistic logic and reverse mathematics

Proof, Truth, Computation: Summer School on the Interactions between Modern Foundations of Mathematics and Contemporary Philosophy, Chiemsee, Germany, 2014

Proof, Truth, Computation: Summer School on the Interactions between Modern Foundations of Mathematics and Contemporary Philosophy, Chiemsee, Germany, 2014

A monad in the combinatory algebras

Correctness by Construction CORCON 2014 Workshop, Genoa, Italy, 2014

Correctness by Construction CORCON 2014 Workshop, Genoa, Italy, 2014

#### ■Teaching Experience

Computation Theory(E), Theoretical Computer Science, Mathematical Logic(E), Fundamentals of Logic and Mathematics, 計算論(E), 理論計算機科学, 数理論理学(E), 基礎論理数学

#### ■Contributions to Society

Association for Symbolic Logic, American Mathematical Society, Mathematical Society of Japan

Workshop on Constructive Aspects of Logic and Mathematics , Japan Advanced Institute of Science and Technology, School of Information Science, Associate Professor Hajime Ishihara , 2010 - 2010 , Kanazawa

Workshop on Constructivism: Logic and Mathematics , Japan Advanced Institute of Science and Technology, School of Information Science, Associate Professor, Hajime Ishihara , 2008 - 2008 , Kanazawa

Workshop on Constructivism: Logic and Mathematics , Japan Advanced Institute of Science and Technology, School of Information Science, Associate Professor, Hajime Ishihara , 2008 - 2008 , Kanazawa