"** new foundations must give new math**"

from

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.