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

The Basic Picture: principles and summary

What I care most is to show through the Basic Picture (BP) that a new way of doing mathematics is not only reasonable and feasible, but actually also technically usable. It adopts a foundation never used before to develop mathematics, and also some methodological principles: equal importance of definitions and of proofs, anti-reductionism, dynamic balance between different components, importance of logic, modular approach, compatibility with other foundations, etc. So BP is a new field of mathematics, which is constructive from its birth.

The main principle is that only with a "weak" foundation the finer structure of mathematical reality can emerge and is respected; "strong" foundations kill this structure in a precise sense. Even accepting the notion of basic pair (which usually is unnecessary since impredicatively opens subsets form a set), the definition of closed subset is reduced to complementation of open subsets, if classical logic is assumed, or to an impredicative quantification over all open subsets. In either case, closed subsets are uniquely determined by open subsets, so that the richness of their logical duality is lost.

The foundation adopted for the development of BP is constructive type theory, and more precisely a variant of Martin-Löf's system called minimal type theory. The axiom of choice is not assumed, and this allows for a clearcut distinction between a function (meant as a program) and its graph (meant as a relation), that is, between lawlike and choice sequences. Moreover, it makes BP compatible with all other foundations, including topos theory.

The duality between open and closed is extended to pointfree, or formal topology. So the notion of cover, giving formal opens, is now accompanied by its dual notion of positivity relation, giving formal closed subsets.
Both are present in the new notion of basic topology; their link is given by a condition called compatibility. The lack of convergence allows for new interesting interpretations of basic topologies; in the game theoretic interpretation, compatibility becomes the possibility of cooperation between two players with different targets.