The problem of the formalization of constructive topology |
| |
Authors: | Silvio Valentini |
| |
Institution: | (1) Dipartimento di Matematica Pura ed Applicata, Università di Padova, via G. Belzoni n.7, 35131 Padova, Italy |
| |
Abstract: | Formal topologies are today an established topic in the development of constructive mathematics. One of the main tools in formal topology is inductive generation since it allows to introduce inductive methods in topology. The problem of inductively generating formal topologies with a cover relation and a unary positivity predicate has been solved in CSSV]. However, to deal both with open and closed subsets, a binary positivity predicate has to be considered. In this paper we will show how to adapt to this framework the method used to generate inductively formal topologies with a unary positivity predicate; the main problem that one has to face in such a new setting is that, as a consequence of the lack of a complete formalization, both the cover relation and the positivity predicate can have proper axioms. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|