A Preview of the Basic Picture: A New Perspective on Formal Topology

If the classical definition of topological space is analysed at the light of an intuitionistic and predicative foundation as Martin-Löf’s type theory, one is lead to the notion of basic pair: a pair of sets, concrete points and observables (or formal neighbourhoods), linked by a binary relation called forcing. The new discovery is that this is enough to introduce the topological notions of open and closed subsets, both in the concrete (pointwise) and in the formal (pointfree) sense. Actually, a new rich structure arises, consisting of a symmetry between concrete and formal and of a logical duality between open and closed. Closed subsets are defined primitively, as universal-existential images of subsets along the forcing relation, while open subsets are existential-universal images. So, in the same way as logic gives a theory of subsets as the extension of unary propositional functions over a given set, now logic is seen to produce topology if we pass to two sets linked by a relation, that is a propositional function with two arguments.Usual topological spaces are obtained by adding the condition that the extensions of observables form a base for a topology, which is seen to be equivalent to distributivity. Formal topologies are then obtained by axiomatizing the structure induced on observables, with some improvements on previous definitions. A morphism between basic pairs is essentially a pair of relations producing a commutative square: this is thus the essence of continuity. Usual continuous functions become a special case. This new perspective, which is here called basic picture, starts a new phase in constructive topology, where logic and topology are deeply connected and where the pointwise and the pointfree approach to topology can live together. It also brings to the development of topology in a more general, nondistributive sense.