A preview of the basic picture: A new perspective on formal topology (Q4944859)

This paper presents, among other things, two possible generalisations of formal topology (as introduced by the first author in ``Intuitionistic formal spaces -- a first communication'' [Mathematical logic and its applications, Proc. Adv. Int. Summer Sch. Conf., Druzhba/Bulg. 1986, 187-204 (1987; Zbl 0703.03040)]: one is the introduction of the dual of the notion of formal open (formal closed) and the corresponding dual of the covering relation (this dual is called here binary Pos), and the other generalisation is obtained by taking away the distributivity axiom (so, formal opens do form a complete lattice, but it may not be distributive in general). These generalisations are suggested by the notion of a basic pair, which is given by two sets and a relation between them. The intuition is that one set is the set of points while the other is a set of basic open sets, the relation being the membership relation. Several interesting symmetries and dualities, all valid intuitionistically, are already present at this level. The binary positivity predicate, dual of the covering relation between basic open sets and sets of basic open sets, generalises the unary positivity predicate of formal topology, but for the positivity axiom. While the present paper shows the heuristic usefulness of considering simultaneously the ``set'' of points and a set of basic open sets, it should be stressed (as it is done in the present paper, p. 196) that, in most examples, the collection of points of a formal topology does not have an inductive description and does not form a set in constructive type theory. For the entire collection see [Zbl 0929.00065].