The classical definition of topological space, analysed at the light of an intuitionistic and predicative foundation, leads to the notion of basic pair, that is two sets, the set of concrete points and the set of observables (or formal neighbourhoods), linked by any binary relation called forcing.
A new discovery is that this is enough to introduce the usual topological notions of open and closed subsets, and to see both a geometrical symmetry between concrete and formal, and a logical duality between open and closed. If closed subsets are defined primitively, they turn out to be universal-existential images of subsets along the forcing relation, while open subsets are existential-universal images.
Usual topological spaces are obtained by adding the condition that the extension of observables form a base for a topology, which is seen to be equivalent to distributivity.
The notion of continuity, is treated in a similar way. Morphisms between basic pairs are just pairs of relations producing a commutative square: this is thus the essence of continuity. Usual continuous functions become a special case.
For a preview of the basic picture see A preview of the basic picture: a new trend in formal topology by G. Sambin and S. Gebellato, while the motivations underlying the approach of the basic picture and general comments on the principles of intuitionistic-predicative mathematics will be available in Some points in formal topology by G. Sambin.
Formal topologies and a formal (pointfree) notion of continuity and convergence are obtained by axiomatizing the structure induced on the formal side.
A new definition of formal topology is derived, with several improvements over the previous one. It contains a new primitive, the so-called binary positivity predicate, which gives further expressive power (previous formal topology and locale theory are special cases). Duality extends also to the generation of topologies: while the formal cover is generated inductively, the positivity predicate is generated co-inductively.
Another novelty is the introduction and systematic use of the notion of meet, which is logically dual of that of inclusion.
An exhaustive description of the approach of the basic picture will be presented in a forthcoming series of papers, containing all technical details.