Towards limit computable mathematics. (English) Zbl 1054.03037
Callaghan, Paul (ed.) et al., Types for proofs and programs. International workshop, TYPES 2000, Durham, GB, December 8–12, 2000. Selected papers. Berlin: Springer (ISBN 3-540-43287-6). Lect. Notes Comput. Sci. 2277, 125-144 (2002).
Summary: The notion of Limit-Computable Mathematics (LCM) is introduced. LCM is a fragment of classical mathematics in which the law of excluded middle is restricted to \(\Delta^0_2\). We can give an accountable computational interpretation to the proofs of LCM. The computational content of LCM-proofs is given by Gold’s limiting recursive functions, which is the fundamental notion of learning theory. LCM is expected to be a right means for “Proof Animation”, which was introduced by the first author [see S. Hayashi, R. Sumitomo and K. Shii, Theor. Comput. Sci. 272, 177–195 (2002; Zbl 0984.68138)]. LCM is related not only to learning theory and recursion theory, but also to many areas in mathematics and computer science such as computational algebra, computability theories in analysis, reverse mathematics, and many others.
For the entire collection see [Zbl 0988.00060].
For the entire collection see [Zbl 0988.00060].
MSC:
03F35 | Second- and higher-order arithmetic and fragments |
03D20 | Recursive functions and relations, subrecursive hierarchies |
68Q32 | Computational learning theory |
03B35 | Mechanization of proofs and logical operations |