Inductively generated formal topologies. (Q1412832): Difference between revisions

This paper introduces the very useful concept of inductively generated formal topology (without or with the positivity predicate) in a predicative framework. Formal topology was introduced by P. Martin-Löf and G. Sambin to provide a predicative representation of the concept of locale and open locale [see \textit{G. Sambin}, ``Intuitionistic formal spaces -- a first communication'', in: Mathematical Logic and its Applications, 187--204 (1987; Zbl 0703.03040), and ``Some points in formal topology'', Theor. Comput. Sci. 305, No. 1--3, 347--408 (2003; Zbl 1044.54001)]. The inductive generation in topology is a very important tool since it allows one to reason on topology by induction, that is, by using proof-theoretic methods, and it provides predicative examples of formal topologies. One of these remarkable examples is the inductive formal topology of real numbers. In the paper, the authors start with discussing that the axiomatic definition of formal topology in the cited papers by G. Sambin is not inductive predicatively. At the end they also provide a counterexample of a predicative formal topology that is not inductive by taking the Dedekind-MacNeille cover on the Boolean set. Another difference between generic formal topologies and inductive ones is that, while inductively generated formal topologies are easily seen to be closed predicatively under suitable constructions, such as the closure under binary products, for formal topology it is still not known (predicatively!).