The beginning of formal (or point-free topology) can be traced back to Whitehead (1915: revue de Metaphysique, ``Theorie relationnelle de l'espace''), and a survey of the state of the art in 1940 was written by Menger.
There is another older algebraic tradition: Dedekind and Weber (1882) analysed a purely algebraic presentation of Riemann surfaces where the notion of points is derived. This seems to have been inspired by the work of Kronecker. In this work, what are primary are polynomials with integer coefficients, and the solutions of these equations are considered to be ideal elements. Typically also, one does not work in one ``big'' algebraic closure given a priori, but one adds new symbolic elements that should satisfy some constraints (polynomial equations) when needed. We have started a formal presentation of the work of Dedekind and Weber in this work on valuations and this development. It is somewhat remarkable that the treatment of algebra in the XIXth century was in some sense logically more satisfactory than the one in the XXth century. The intensive use of Zorn's lemma in abstract algebra does not appear to be necessary.
The relevance of these concepts to constructive mathematics and computer science (especially domain theory) is that this gives a method to describe infinite objects (the points) in a purely finitary and algebraic way.
Tutorials in the last formal topology workshop on the positivity predicate. Notice that all properties are stated only with the reflexivity and transitivity property.
Tutorials in Padova. General introduction to the use of formal topology in constructive algebra.
A general talk about constructive algebra
A note on the equirepartition theorem of Weyl, reading in a point-free way a proof by Cigler.
A simple point-free proof of a geometric form of Hahn-Banach's theorem.
The published constructions of the generic site model of a geometric theory are not optimal, since they use logic in the construction of the model. We present a logic-free construction of the generic model. A pdf version is here And here is a pdf version of some slides presenting examples
Talk given at the Edinburgh meeting on proofs and algorithms, march 2003
A remark on Segal's notion of integration algebra
A summary of a discussion with Peter Schuster (february 2003)
An direct proof of a remark of Krivine (1964). An application is a constructive direct proof of Kadison-Dubois.
Inspired by the thesis of Bas Spitters, should converge to a self-contained elementary presentation of Peter-Weyl's theorem
A simple proof of the key lemma of Stone-Weierstrass theorem.
Some remarks on geometrical logic.
Talk given for the Workshop on Domain Theory VI
Talk given for the Second Workshop on Formal Topology
About Stone's Notion of Spectrum
Article version of this talk. This is a revised version, thanks to comments from Robert Lubarsky.
A general talk on ``algebraization'' of Functional Analysis
A beginning of constructive descriptive set theory. We present Borel subsets of Cantor space following Martin-Lof, and establish Baire category theorem in this framework.
We give a direct inductive proof that the notion of compact space and of Noetherian ring are invariant under changes of base (intuitively, invariant under addition of new quantities)
We give a direct inductive proof of Steenord's theorem
We present a constructive theory of Riesz space and Dedekind sigma-complete Riesz space. In particular we present a constructive version of Stone's representation theorem of Riesz space. This gives a point-free definition of bounded Baire functions over a compact Hausdorff's space. Also, we show how to define the measure of Borel sets for measure which takes value in an arbitrary monotone sigma-complete ordered space.
We present Stone's version of Gelfand duality in a constructive setting. This gives an algebraic representation of compact Hausdorff's spaces and gives a convenient setting for describing constructively measures on such spaces
With Giovanni Sambin, Jan Smith and Silvio Valentini. We analyse some connections between formal topology and the intuitionistic theory of inductive definitions.
How to formulate a basic result of Tarksi (1929) on the existence of additive functions over a monoid
Contains what maybe the right ``finitary'' definition of compact regular space, as normal lattices. This definition is explored in the paper on lattices
A proof of the marriage lemma using completness of hyperresolution (actually close to the one of Rado)