Formal spaces and their effective presentations (Q1902337)

We investigate to what extent the theory of formal spaces can be used as a general framework for studying effective structures. Thus we examine and develop the theory from an effective point of view. The fundamental concept of the paper is that of a presentation of a formal space in terms of a pre-neighbourhood system \(P\) and generators for a covering relation on \(P\). The covering relation gives rise to an equivalence relation on the subsets of \(P\). The equivalence classes form a frame and every frame is obtained in this way. The main interest is to study effectivity in formal spaces. The concrete objects of a formal space are its pre-neighbourhoods. We say that a frame is effective if it has a presentation in terms of a semicomputable pre- neighbourhood system. We define the notion of a presentation of a formal space, and carefully examine the theory of formal spaces, to see how much of it can be expressed in terms of presentations. Then we define and study the notion of an effective formal space.