### Formal Topology

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.

• A note on choice sequences (2018) Here is a more recent version (2020)
• tutorial

Tutorials in the last formal topology workshop on the positivity predicate. Notice that all properties are stated only with the reflexivity and transitivity property.

• talk1 talk2

Tutorials in Padova. General introduction to the use of formal topology in constructive algebra.

• On Weyl's theorem

A note on the equirepartition theorem of Weyl, reading in a point-free way a proof by Cigler.

• A completeness proof for geometric logic

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

• x^2+1 is positive

An direct proof of a remark of Krivine (1964). An application is a constructive direct proof of Kadison-Dubois.

• Peter-Weyl's theorem

Inspired by the thesis of Bas Spitters, should converge to a self-contained elementary presentation of Peter-Weyl's theorem

• Stone's Notion of Spectra

Talk given for the Second Workshop on Formal Topology

Article version of this talk. This is a revised version, thanks to comments from Robert Lubarsky.

• Constructive Baire Category Theorem

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.

• Notions Invariant by Change of Bases

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)

• How to Measure Borel Sets
• ps version

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.

• About Stone's notion of Spectrum

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

• On the measure problem

How to formulate a basic result of Tarksi (1929) on the existence of additive functions over a monoid