Mathematics Based on Learning
(invited lecture for ALT 2002 and DS 2002)
Author: Susumu Hayashi
Affiliation: Department of Computer Science and Engineering,
Faculty of Engineering, Kobe University, Kobe, Japan
Abstract.
LimitComputable Mathemacs (LCM) tries to give
semantics for fragments of classical mathematics by means of Gold's notion
of limiting computable (recursive) functions. Instead of thinking learnability
of properties in classical mathematics, we give semantics of mathematical
statements by means of Gold's learning theoretic notions. For example,
``A or B'' means ``we can indentify
A or B in the limit.''
Thus ``A or not A''
does not mean true, but means ``we can identify A
is true or false in the limit.''
LCM is expeceted to be a foundation of the formal technique ``proof animation,''
which aims to ``test'' formal proofs by execution of programs.
©Copyright 2002 Author and Springer
