home | mathematics ::... 1 | 2
I have always felt uneasy with classical mathematics and set theory;
meeting Per Martin-Löf and his type theory in 1980 made me realize
that it was possible to do mathematics in a more satisfactory way.
Since then, I have been active in the building up of "satisfactory"
(which in my view requires: intuitionistic and predicative) mathematics,
topology in particular, using Martin-Löf's type theory as a foundation.
When topology is developed in this way, the pointfree approach is fundamental;
this is why it is called formal.
Begun in the 80s by myself in collaboration with Martin-Löf, formal
topology has grown considerably, both in theoretical understanding (inductive
methods in topology, predicative proof of the completeness theorem for
intuitionistic logic,...) and in scope (in particular, by the inclusion
of domain theory).
The deep motivation for predicativity is that it makes formal topology an ideal tool (perhaps the only one) to connect infinitistic methods in mathematics with the computational content, while keeping them clearly distinct. More on formal topology ::...
Two workshops on Formal Topology have been held, 1WFTop
in Padova, October 1997, and 2WFTop
in Venice, April 2002. Both have been appreciated for bringing together
different approaches to pointfree topology and for their relaxed and
constructive atmosphere. The proceedings of 2WFTop will soon appear
as a special issue of Annals of Pure and Applied Logic
(see the 2WFTop
table of contents).
I am now thinking about the 3WFTop: suggestions are welcome.
The experience of developing topology over type theory has brought me to a specific practical attitude on foundations, which I call minimalist, and also on the problem of systematic implementation of mathematics on a computer. To this aim, one needs both a ground intensional type theory (essentially, a programming language) and a stock of high level tools on top of it, or "toolbox", which provide with an extensional framework and standard mathematical notation. To preserve the computational content and systematic formalization, each tool is introduced according to a discipline, which I called the forget-restore principle. More on toolbox and the minimalist attitude ::...
