Masahiko Sato
Graduate School of Informatics
Kyoto University

Abstract:
We propose a computational and logical framework NF (NaturalFramework) which is suitable for presenting mathematics as adynamically extending system. Our framework is an extendableframework since it is open-ended both computationally and logically.NF will be developed in three steps. Firstly, we will introduce atheory of expressions and schemes which provides a universe forrepresenting mathematical objects, in particular, judgments andderivations as well as other usual mathematical objects. Secondly, wedevelop a theory of judgments and derivation within the syntacticuniverse of expressions and schemes. Finally, we will introduce thenotion of derivation game and will show that we can developmathematics as derivation games by regarding mathematics as anopen-ended process of defining new concepts and deriving newjudgments. Our theory is inspired by Martin-Lof's theory ofexpressions and Edinburgh LF, but conceptually much simpler.