From geometric logic to algebraic geometry

A partial realisation of Hilbert's programme has recently proved successful in commutative algebra. From a vantage point a reason for this is that algebraic statements typically can be expressed by geometric formulas, for which Barr's theorem says that classical logic with the axiom of choice is conservative over intuitionistic logic. Geometric formulas, moreover, correspond to the rules by which proof trees in dynamical algebra (Coste, Lombardi, Roy) are generated, and so allow for a neat computational interpretation as subprograms.

In realising Hilbert's programme in commutative algebra one of the key tools is Joyal's point-free presentation of the Zariski spectrum as a distributive lattice. Extending this to algebraic geometry requires to first reformulate Grothendieck's language of schemes in first-order terms. It turns out that distributive lattices even suffice for all the schemes whose underlying topological spaces are spectral. This includes the majority of schemes including the Noetherian ones.

- joint work with Thierry Coquand and Henri Lombardi -