Theory of judgments and derivations
pp. 78-122
in: Setsuo Arikawa, Ayumi Shinohara (eds), Progress in discovery science, Berlin, Springer, 2002Abstract
We propose a computational and logical framework NF (Natural Framework) which is suitable for presenting mathematics formally. Our framework is an extendable framework since it is open-ended both computationally and logically in the sense of Martin-Löf's theory or types. NF is developed in three steps. Firstly, we introduce a theory of expressions and schemata which is used to provide a universe for representing mathematical objects, in particular, judgments and derivations as well as other usual mathematical objects. Secondly, we develop a theory of judgments within the syntactic universe of expressions. Finally, we introduce the notions of derivation and derivation game and will show that we can develop mathematics as derivation games by regarding mathematics as an open-ended process of defining new concepts and deriving new judgments. Our theory is inspired by Martin-Löf's theory of expressions and Edinburgh LF, but conceptually much simpler. Our theory is also influenced by Gentzen's natural deduction systems.