Space of valuations

Annals of Pure and Applied Logic 157 (2-3):97-109 (2009)
  Copy   BIBTEX


The general framework of this paper is a reformulation of Hilbert’s program using the theory of locales, also known as formal or point-free topology [P.T. Johnstone, Stone Spaces, in: Cambridge Studies in Advanced Mathematics, vol. 3, 1982; Th. Coquand, G. Sambin, J. Smith, S. Valentini, Inductively generated formal topologies, Ann. Pure Appl. Logic 124 71–106; G. Sambin, Intuitionistic formal spaces–a first communication, in: D. Skordev , Mathematical Logic and its Applications, Plenum, New York, 1987, pp. 187–204]. Formal topology presents a topological space, not as a set of points, but as a logical theory which describes the lattice of open sets. The application to Hilbert’s program is then the following. Hilbert’s ideal objects are represented by points of such a formal space. There are general methods to “eliminate” the use of points, close to the notion of forcing and to the “elimination of choice sequences” in intuitionist mathematics, which correspond to Hilbert’s required elimination of ideal objects. This paper illustrates further this general program on the notion of valuations. They were introduced by Dedekind and Weber [R. Dedekind, H. Weber, Theorie des algebraischen Funktionen einer Veränderlichen, J. de Crelle t. XCII 181–290] to give a rigorous presentation of Riemann surfaces. It can be argued that it is one of the first example in mathematics of point-free representation of spaces [N. Bourbaki, Eléments de Mathématique. Algèbre commutative, Hermann, Paris, 1965, Chapitre 7]. It is thus of historical and conceptual interest to be able to represent this notion in formal topology



    Upload a copy of this work     Papers currently archived: 91,139

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles


Added to PP

18 (#762,892)

6 months
4 (#573,918)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Citations of this work

Constructive mathematics.Douglas Bridges - 2008 - Stanford Encyclopedia of Philosophy.
Fundamental results for pointfree convex geometry.Yoshihiro Maruyama - 2010 - Annals of Pure and Applied Logic 161 (12):1486-1501.

Add more citations

References found in this work

Inductively generated formal topologies.Thierry Coquand, Giovanni Sambin, Jan Smith & Silvio Valentini - 2003 - Annals of Pure and Applied Logic 124 (1-3):71-106.
The genesis of ideal theory.Harold M. Edwards - 1980 - Archive for History of Exact Sciences 23 (4):321-378.
Minimal invariant spaces in formal topology.Thierry Coquand - 1997 - Journal of Symbolic Logic 62 (3):689-698.

Add more references