"new foundations must give new math"

from "The Basic Picture. Structures for constructive topology"

by Giovanni Sambin, Oxford University Press, forthcoming

Registration

To register send an e-mail to maietti @ math.unipd.it

Registration fee: 40 euros
(to be paid at arrival).

Under the patronage of

Dipartimento di Matematica Pura ed Applicata, Università degli Studi di Padova, Italy

University of Padova, Italy

AILA (Italian Association of Logic and Applications), whose first president was Giovanni Sambin (from 1987 to 1994).

Abstracts » Curi

Giovanni Curi
Verona

A cocomplete extension of the category of formal topologies

The notion of formal topology, as considered in this context, provides a description of the concept of frame (or locale) that is suited to be formulated within intuitionistic and (generalized) predicative systems such as constructive type theory (CTT) and constructive set theory (CZF).

Considered in fully impredicative settings such as topos logic, the category FTop of formal topologies is equivalent to the category of frames (dually equivalent to that of locales).

In contrast with what happens in a topos, no uniform method is available for constructing colimits of formal topologies in CZF, CTT, not even for binary coproducts; such a method instead exists for diagrams in the full subcategory IFTop of FTop, of inductively generated formal topologies, though under the assumption of strong set inductive definition principles (of the axiom REA in constructive set theory).
Since, moreover, in fully impredicative settings, IFTop is still equivalent to the category of frames, the general attitude has been to focus on IFTop as the main object of study.

In a previous occasion we showed that this restriction is however a very severe one, as important classes of formal topologies (notably the Boolean ones) are left out.

In this talk we recapitulate these results and describe a new class of formal topologies that cannot be inductively generated. Via formally minor modifications of the notions of formal topology and formal topology morphism, we define then in CZF the category CSites of class-sites.
One may think of a class-site as been defined by a family of generators and relations that need not predicatively present a frame (whereas a formal topology always determines a class-sized frame).

The category CSites is cocomplete (has all colimits), contains the category of formal topologies as a full subcategory, and, as FTop and IFTop, is equivalent in topos logic to the category of frames.

The concept of class-site may in particular be of interest in weaker systems, especially those lacking axioms that allow for very general inductive definitions of sets.