×

Mathematics based on incremental learning – excluded middle and inductive inference. (English) Zbl 1086.68063

Summary: Learning theoretic aspects of mathematics and logic have been studied by many authors. They study how mathematical and logical objects are algorithmically “learned” (inferred) from finite data. Although they study mathematical objects, the objective of the studies is learning. In this paper, a mathematics whose foundation itself is learning theoretic is introduced. It is called Limit-Computable Mathematics. It was originally introduced as a means for “Proof Animation”, which is expected to make interactive formal proof development easier. Although the original objective was not learning theoretic at all, learning theory is indispensable for our research. It suggests that logic and learning theory are related in a still unknown but deep new way.

MSC:

68Q32 Computational learning theory
03D20 Recursive functions and relations, subrecursive hierarchies
03F50 Metamathematics of constructive systems
03F65 Other constructive mathematics
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Y. Akama, S. Beradi, S. Hayashi, U. Kohlenbach, An arithmetical hierarchy of the law of excluded middle and related principles, Proc. 19th IEEE Symposium LICS 2004, IEEE Computer Society 2004, pp. 192-201.; Y. Akama, S. Beradi, S. Hayashi, U. Kohlenbach, An arithmetical hierarchy of the law of excluded middle and related principles, Proc. 19th IEEE Symposium LICS 2004, IEEE Computer Society 2004, pp. 192-201.
[2] Y. Akama, S. Hayashi, Limiting Cartesian closed categories, 2002, submitted for publication.; Y. Akama, S. Hayashi, Limiting Cartesian closed categories, 2002, submitted for publication.
[3] A. Ambainis, J. Case, S. Jain, M. Suraj, Parsimony hierarchies for inductive inference, manuscript, 2003.; A. Ambainis, J. Case, S. Jain, M. Suraj, Parsimony hierarchies for inductive inference, manuscript, 2003. · Zbl 1068.68071
[4] S. Baratella, S. Berardi, in: M. Takahashi, M. Okada, M. Dezani-Ciancaglini (Eds.), Constructivization via Approximations and Examples, Theories of Types and Proofs, MSJ Memories, Vol. 2, 1998, pp. 177-205.; S. Baratella, S. Berardi, in: M. Takahashi, M. Okada, M. Dezani-Ciancaglini (Eds.), Constructivization via Approximations and Examples, Theories of Types and Proofs, MSJ Memories, Vol. 2, 1998, pp. 177-205. · Zbl 0937.03064
[5] Bardzins, J.; Freivalds, R.; Smith, C. H., A logic of discovery, Discovery Sci., 401-402 (1998)
[6] Beck, K., Test-Driven Development: By Example (2002), Addison-Wesley: Addison-Wesley Reading, MA
[7] Beeson, M., Foundations of Constructive Mathematics (1985), Springer: Springer Berlin · Zbl 0565.03028
[8] S. Berardi, Some intuitionistic equivalent of classical principles for degree 2 formulas, manuscript, 2004.; S. Berardi, Some intuitionistic equivalent of classical principles for degree 2 formulas, manuscript, 2004.
[9] S. Berardi, Classical logic as Limit Completion, a constructive model for non-recursive maps, Mathematical Structures in Computer Science 15 (2005) 167-200.; S. Berardi, Classical logic as Limit Completion, a constructive model for non-recursive maps, Mathematical Structures in Computer Science 15 (2005) 167-200. · Zbl 1068.03054
[10] Bridges, D.; Richman, F., Varieties of Constructive Mathematics (1987), Cambridge University Press: Cambridge University Press Cambridge · Zbl 0618.03032
[11] Case, J.; Suraj, M., Inductive inference of \(\Sigma_1^0\)- vs. \( \Sigma_2^0\)-definitions of computable functions, (Proc. Internat. Conf. on Mathematical Logic. Proc. Internat. Conf. on Mathematical Logic, Novosibirsk, Russia (1999))
[12] Coquand, T., A semantics of evidence for classical arithmetic, J. Symbolic Logic, 60, 1, 325-337 (1995) · Zbl 0829.03037
[13] Y. Ershov, A hierarchy of sets I, II, III, Algebra Logic 7 (1968) 47-74, transl. 7 (1968) 25-43, Algebra Logic 7 (1968) 15-47, transl. 7 (1968) 212-232, Algebra Logic 9 (1970) 34-51, transl. 9 (1970) 20-31.; Y. Ershov, A hierarchy of sets I, II, III, Algebra Logic 7 (1968) 47-74, transl. 7 (1968) 25-43, Algebra Logic 7 (1968) 15-47, transl. 7 (1968) 212-232, Algebra Logic 9 (1970) 34-51, transl. 9 (1970) 20-31. · Zbl 0216.00901
[14] S. Hayashi, Mathematics based on learning, in algorithmic learning theory, Proc. 13th Internat. Conf. ALT 2002, Vol. 272, Springer Lecture Notes in Artificial Intelligence, Vol. 2533, Springer, Berlin, 2002, pp. 7-21.; S. Hayashi, Mathematics based on learning, in algorithmic learning theory, Proc. 13th Internat. Conf. ALT 2002, Vol. 272, Springer Lecture Notes in Artificial Intelligence, Vol. 2533, Springer, Berlin, 2002, pp. 7-21. · Zbl 1024.68052
[15] S. Hayashi, H. Nakano, PX: A Computational Logic, 1988, The MIT Press, Cambridge, MA, PDF version is available at \(\&\#60;\) http://www.shayashi.jp/PXbook.html \(>\); S. Hayashi, H. Nakano, PX: A Computational Logic, 1988, The MIT Press, Cambridge, MA, PDF version is available at \(\&\#60;\) http://www.shayashi.jp/PXbook.html \(>\)
[16] S. Hayashi, M. Nakata, in: P. Challanghan, Z. Luo, J. McKinna, R. Pollack (Eds.), Towards Limit Computable Mathematics, in Types for Proofs and Programs, Lecture Notes in Computer Science, Vol. 2277, Springer, Berlin, 2001, pp. 125-144.; S. Hayashi, M. Nakata, in: P. Challanghan, Z. Luo, J. McKinna, R. Pollack (Eds.), Towards Limit Computable Mathematics, in Types for Proofs and Programs, Lecture Notes in Computer Science, Vol. 2277, Springer, Berlin, 2001, pp. 125-144. · Zbl 1054.03037
[17] S. Hayashi, Y. Pan, M. Sato, K. Mori, S. Sul, S. Haruna, Test driven development of UML models with SMART modeling system, Proc 7th UML International Conference 2004, Springer Lecture Notes in Computer Science, 3273, 2004, pp. 395-409.; S. Hayashi, Y. Pan, M. Sato, K. Mori, S. Sul, S. Haruna, Test driven development of UML models with SMART modeling system, Proc 7th UML International Conference 2004, Springer Lecture Notes in Computer Science, 3273, 2004, pp. 395-409.
[18] Hayashi, S.; Sumitomo, R.; Shii, K., Towards animation of proofs—testing proofs by examples, Theoret. Comput. Sci., 272, 177-195 (2002) · Zbl 0984.68138
[19] Lifschitz, V., \( \operatorname{CT}_0\) is stronger than \(\operatorname{CT}_0\)!, Proc. Amer. Math. Soc., 73, 101-106 (1979)
[20] Nakata, M.; Hayashi, S., Realizability interpretation for limit computable mathematics, Sci. Math. Japon., 5, 421-434 (2001)
[21] Odifreddi, P. G., Classical Recursion Theory (1989), North-Holland: North-Holland Amsterdam · Zbl 0931.03057
[22] Popper, K., The Logic of Scientific Discovery, Routledge Classics (2002), Routledge: Routledge London and New York
[23] Shapiro, E. Y., Inductive inference of theories from facts, (Lassez, J. L.; Plotkin, G. D., Computational Logic: Essays in Honor of Alan Robinson (1991), MIT Press: MIT Press Cambridge, MA), 199-255
[24] Shoenfield, J. R., On degrees of unsolvability, Ann. Math., 69, 644-653 (1959) · Zbl 0119.25105
[25] Simpson, S. G., Subsystems of Second Order Arithmetic (1999), Springer: Springer Berlin · Zbl 0909.03048
[26] F. Stephan, Y. Ventsov, Learning algebraic structures from text using semantical knowledge, Theoret. Comput. Sci. Ser. A 268 (2001) 221-273, in: Extended Abstract in Proc. Ninth Annu. Workshop on Algorithmic Learning Theory—ALT 1998, Springer Lecture Notes in Computer Science, Vol. 1501, Springer, Berlin, 1998, pp. 321-335.; F. Stephan, Y. Ventsov, Learning algebraic structures from text using semantical knowledge, Theoret. Comput. Sci. Ser. A 268 (2001) 221-273, in: Extended Abstract in Proc. Ninth Annu. Workshop on Algorithmic Learning Theory—ALT 1998, Springer Lecture Notes in Computer Science, Vol. 1501, Springer, Berlin, 1998, pp. 321-335. · Zbl 0928.03055
[27] M. Toftdal, A Calibration of Ineffective Theorems of Analysis in a Hierarchy of Semi-Classical Logical Principles, Proc. 31st International Colloquium ICALP 2004, Springer Lecture Notes in Computer Science, 3142, 2004, pp.1188-1200.; M. Toftdal, A Calibration of Ineffective Theorems of Analysis in a Hierarchy of Semi-Classical Logical Principles, Proc. 31st International Colloquium ICALP 2004, Springer Lecture Notes in Computer Science, 3142, 2004, pp.1188-1200. · Zbl 1099.03515
[28] Troelstra, A., Realizability, (Buss, S., Handbook of Proof Theory (1998), Elsevier: Elsevier Amsterdam), 407-474 · Zbl 0911.03031
[29] van Oosten, J., Lifschitz’ realizability, J. Symbolic Logic, 55, 805-821 (1990) · Zbl 0704.03040
[30] Yasugi, M.; Brattka, V.; Washihara, M., Computability aspects of some discontinuous functions, Sci. Math. Japon., 5, 405-419 (2001)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.