
Hajime Ishihara Professor
School of Information Science、Area of Inteligent Robotics
■Degrees
B.S., M.S. and Ph.D.from Tokyo Institute of Technology (1980,1987,1990)
■Professional Career
Researcher at Mitsubishi Research Institute, Inc. (1980), Associate at Hiroshima University (1988), Associate Professor at Japan Advanced Institute of Science and Technology (1992)
■Specialties
Constructive Mathematics, Mathematical Logic, and Foundations of Mathematics
■Research Keywords
constructive mathematics, intuitionistic logic, reverse mathematics, constructive set theory
■Research Interests
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 MartinLoef 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 CurryHoward correspondence, between proofs in intuitionistic logic and programs (terms of lambdacalculus), 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 lambdacalculus and type theory such as simple types, intersection types and union types.
■Publications
◇Published Papers
 Nondeterministic inductive definition and Fullness，Hajime Ishihara and Takako Nemoto，In: Dieter Probst and Peter Schuster (eds.), "Concepts of Proof in Mathematics, Philosophy, and Computer Science". Ontos Mathematical Logic. Walter de Gruyter, Berlin，pp.163170，2016
 Embedding classical in minimal implicational logic，Hajime Ishihara and Helmut Schwichtenberg，MLQ Math. Log. Q.，62，94101，2016
 A note on the independence of premiss rule，Hajime Ishihara and Takako Nemoto，MLQ Math. Log. Q.，62，7276，2016
Display All
◇Lectures and Presentations
 A monad on the combinatory algebras，Hajime Ishihara，Operations, Sets, and Types，Muenchenwiler, Switzerland，April 18  20, 2016
 Constructive reverse mathematics: an introduction and recent results，Hajime Ishihara，Frontiers of NonClassicality: Logic, Mathematics, Philosophy，Auckland, New Zealand，January 2629, 2016
 Constructive reverse mathematics and omniscience pringiples，Hajime Ishihara，14th Asian Logic Conference，Munbai, India，January 58, 2015
Display All
■Extramural Activities
◇Academic Society Affiliations
 Association for Symbolic Logic，1992
 American Mathematical Society，1989
 Mathematical Society of Japan，1988
◇Other Activities
 Computability and Complexity in Analysis 2011，Scientific Programme Committee，2011/01/31  2011/02/04
 Constructive Mathematics: Proof and Computation，Programme Committee，2010/06/07  2010/06/11
 Computability and Complexity in Analysis (CCA) 2009，Scientific Program Committee，2009/08/18  2009/08/22
Display All
