home | mathematics | basic picture | principles and summary ::... 1 | 2 | 3

Since all topological notions acquire a structural or logical motivation, BP can be seen both as applied logic and as generalized topology. Familiar topology, both with or without points, is obtained by adding a single mathematical postulate, that of convergence (or any equivalent manifestation: open subsets are closed under finite intersection, approximations of a formal point can be summed, the lattice of open subsets is distributive). By adding convergence to basic topologies, one obtains a new, more expressive notion of formal topology. Through it, previous formal topology and locale theory, as well as traditional pointwise topology become special cases.

Formal points become just convergent, inhabited closed subsets; their collection is called a formal space, an intrinsically infinitary notion. A cover can be seen as a constructive approximation of pointwise inclusion in a formal space, "from below", and in fact it is generated by induction from some given axioms. Now dually, a positivity relation can be seen as a constructive approximation of overlap in a formal space, "from above", and in fact it can be generated by coinduction.
This remark confirms that positivity (closed) is not to be uniquely determined by cover (open).

A continuous relation between formal topologies induces a function between the corresponding formal spaces, which is automatically continuous. One can thus give a precise form to Brouwer's continuity principle.

Typical of BP is a systematic use of the notion of "overlap" between two subsets (existence of a common element, which is intuitionistically different from nonempty intersection), which is logically dual of that of inclusion. This is prolonged in the primitive notions of closed subset and of positivity, dual of open and of cover respectively.

In general, every notion or condition is accompanied in BP by its dual. This is the deepest novelty brought by BP and marks the beginning of a mathematization of existential statements. That is also a positive treatment of negative information. It is visible for instance in a characterization of relations as two adjunctions, in which moreover the two left adjoint functors are symmetric (a new notion made possible by overlap).