Relative formal topology, namely, the binary positivity predicate comes first

In this paper we introduce relative formal topology in order to deal constructively with the closed subsets of a topological space as well as with the open ones. In fact, within standard formal topology the cover relation allows for the definition of the formal opens, namely, what is supposed to be the formal counterpart of the open subsets, and within balanced formal topology the binary positivity predicate allows for the definition of the formal closed subsets, namely, what is supposed to be the formal counterpart of the closed subsets. However, these approaches are fully satisfactory (according to the criterion introduced by the author in "The problem of the formalization of constructive topology", Archive for Mathematical Logic (44/1), pp.115--129) only if an adequate formalization of the cover relation and the positivity predicate can be provided. But the present formalizations fail in this respect since some intuitionistically valid relations between the open and the closed subsets of a concrete topological space can not be expressed. Our central result is that a generalization of the standard cover relation together with a binary positivity predicate enjoying the positivity axiom solve the problem.