Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
My Menu
Saved Items

Theory of Judgments and Derivations
Dedicated to the Memory of Professor Katuzi Ono

Masahiko SatoContact Information

(2)  Graduate School of Informatics, Kyoto University, Japan
Abstract
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.

Contact Information Masahiko Sato
Email: masahiko@kuis.kyoto-u.ac.jp
Fulltext Preview (Small, Large)
Image of the first page of the fulltext

References secured to subscribers.



Export this chapter
Export this chapter as RIS | Text
 
Remote Address: 38.107.191.108 • Server: mpweb20
HTTP User Agent: CCBot/1.0 (+http://www.commoncrawl.org/bot.html)