|Budget Amount *help
¥3,600,000 (Direct Cost : ¥3,600,000)
Fiscal Year 2006 : ¥900,000 (Direct Cost : ¥900,000)
Fiscal Year 2005 : ¥900,000 (Direct Cost : ¥900,000)
Fiscal Year 2004 : ¥900,000 (Direct Cost : ¥900,000)
Fiscal Year 2003 : ¥900,000 (Direct Cost : ¥900,000)
From 2003 to 2006, for 4 years, we have done a research on computability and complexity in constructive mathematics. During the research, we have got some important and better understandings on the subject. One of the most important understanding is that computability and complexity in constructive mathematics can be dealt with better within a more general framework of constructive reverse mathematics. Moreover, progress in constructive mathematics, such as constructive set theory and topology in constructive mathematics, has produced new problems in computability and complexity in constructive mathematics, and in constructive reverse mathematics.
In this research project, we have proposed a new framework of constructive reverse mathematics. We have investigated relationship between Brouwer's fan theorem and weak Koenig's lemma, with Dr. Josef Berger, and computability in these theorems. With Professor Peter Aczel, Dr. Laura Crosilla, Professor Erik Palmgren, and Associate Professor Peter Schuster, we have dealt with a problem of constructive reverse mathematics in the constructive Zermelo-Fraenkel set theory. Concerning topology in constructive mathematics, we have worked on constructions of quotient topologies in constructive set theory and type theory, with Professor Erik Palmgren, and on quasi-apartness and neighbourhood spaces, with Professor Ray Mines, Associate Professor Peter Schuster and Dr. Luminita Vita. Furthermore, we have treated computational complexity in constructive theory of real numbers and the constructive intermediate value theorem, and a constructive version of Banach's inverse mapping theorem in F-spaces as an application of Baire's theorem.
Further research project is putting research in constructive reverse mathematics forward with progress in constructive mathematics such as constructive set theory and constructive topology.