- Supervisor
- Peter Schuster - Mathematisches Institut, Universitaet Muenchen / Dipartimento di Filosofia, Universita' degli Studi di Firenze
- Date and time
- Tuesday, May 5, 2009 at 5:00 PM - Ore 17 caffe' e pasticcini, ore 17.15 inizio seminario
- Place
- Ca' Vignal - Piramide, Floor 0, Hall Verde
- Programme Director
- Lidia Angeleri
- External reference
- Publication date
- April 22, 2009
- Department

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 -

© 2002 - 2021
Verona University

Via dell'Artigliere 8, 37129 Verona |
P. I.V.A. 01541040232 |
C. FISCALE 93009870234