Mathematical Logic in Padua

home | events | 2WFTop | tutorials


2WFTop 2002 - Tutorials

Peter Aczel

(a) Constructive Set Theory and formal topology

Constructive Set Theory (CST) was initiated by John Myhill in 1975 with an intuitionistic axiom system for constructive mathematics that was essentially a subsystem of ZFC, but might be an appropriate formal foundational language for Bishop style constructive mathematics that did not assume the full impredicativity of IZF (Intuitionistic Zermelo Fraenkel set theory).
In practise constructive mathematics can be carried out in CST in much the same style as classical mathematics can be carried out in ZFC, with natural numbers, ordered pairs, functions etc. treated in the usual set theoretical style.

In my first tutorial I will focus on the axiom systems CZF and CZF+REA, the first of which which is closely related to Myhill's axiom system, except that Myhill assumed DC (Dependent Choices). CZF+REA+DC has a natural interpretation in Martin-Löf's Type Theory, showing that the ideas of constructive set theory have a natural interpretation on the basis of the fundamental constructive ideas of the type theory.

There are good reasons to drop DC and focus on CZF and CZF+REA, one reason being that sheaf reinterpretations generally hold in CZF and probably also in CZF+REA, but DC often fails.

The tutorial will be divided into the following parts:

  • Introducing CZF
  • Elementary Mathematics in CZF (e.g. the Cauchy and Dedekind reals)
  • Formal Topology in CZF
  • Inductive Definitions in CZF and CZF+REA (The Regular Extension Axiom (REA), the Set-Compactness Theorem and its application to formal topology)


  • Peter Aczel and Michael Rathjen, (2001) "Notes on Constructive Set Theory", Mittag-Leffler Technical Report No.40, 2000/2001.
  • Nicola Gambino and Peter Aczel,(2001) "Frame-valued Semantics for Constructive Set Theory" , Mittag-Leffler Technical Report No.39, 2000/2001.
  • John Myhill, (1975) "Constructive Set Theory", J. Symbolic Logic, , Vol 40, 347-382.

(b) Logic-enriched type theory and formal topology

Logic-enriched Type Theory is a variant of Martin-Löf's Type Theory which treats both data types and propositions as primitive and so does not assume the type theoretic axiom of choice.
By including suitable collection principles in the type theory constructive mathematics can be developed in the type theory.

The advantage of logic-enriched type theory over standard Martin-Löf type theory is that sheaf reinterpretations are generally expected to be possible for logic-enriched type theories in a form that mirror such reinterpretations in set theory and category theory.

In the first part of this tutorial I focus on logic-enriched type theory, its relationships with constructive set theory and with standard Martin-Löf type theory. In the second part I look at how some of the notions of formal topology might be presented in logic-enriched type theory.


  • Peter Aczel and Nicola Gambino, (2001) "Collection Principles in Dependent Type Theory", to appear in the Proceedings of Types'00.

Bernhard Banaschewski

(a) Uniformity in pointfree topology

An introduction to the notion of uniformity on a frame and various concepts connected with this such as: completeness, completion, Cauchy completeness and Cauchy completion, uniformities and compactifications, special uniformities.


  • J. R. Isbell, Atomless parts of spaces, Math. Scand. 31 (1972), 5-32, section 3
  • B. Banaschewski and A. Pultr, Paracompactness revisited, Appl. Cat. Struct. 1 (1993), 181-190
  • B. Banaschewski, Completion in pointfree topology, Lecture Notes in Mathematics and Applied Mathematics No.2/96, University of Cape Town, 1996
  • B. Banaschewski, S. S. Hong and A. Pultr, On the completion of nearness frames, Quaest. Math. 21 (1998), 19-37

(b) The real numbers in pointfree topology

The frame L(R) of reals and some of its basic properties. The completeness of L(R) as uniform frame. The real-valued continuous functions on a frame L ( = the homomorphisms L(R) -->L) and their role in relation to complete regularity and normality of frames. The ring RL of real valued continuous functions on a frame L and its subring ZL of integer-valued functions. The real uniformity of a completely regular frame.


  • P. T. Johnstone, Stone spaces, Cambridge University Press, Cambridge 1982, Chapter IV
  • B. Banaschewski, The real numbers in pointfree topology. Textos de Matematica, Serie B, No. 12, Departamento de Matematica da Universidade de Coimbra 1997
  • B. Banaschewski, A uniform view of localic realcompactness, J. Pure Appl. Alg. 143 (1999), 49-68

Giovanni Sambin

(a) Basic picture and formal topology I

  • analysis of the definition of topological space from a predicative point of view
  • definition of concrete space (i.e. X points, S index-set for a base)
  • basic pairs (= X,S sets, and an arbitrary relation between them)
  • existential operators ext and Diamond, universal operators rest and Box
  • interior = ext Box, closure = rest Diamond and their logical duality
  • by symmetry, A = Box ext is a closure operator (giving formal opens subsets) and J = Diamond rest an interior operator on S (giving formal closed subsets)
  • isomorphism between concrete open and formal open, concrete closed and formal closed
  • the essence of continuity = a commutative square diagram


  • G. Sambin, The basic picture, a structure for topology (The Basic Picture 1)
  • S. Gebellato and G. Sambin, The essence of continuity (The Basic Picture 2)

(b) Basic picture and formal topology II

  • how to obtain pointfree, or formal definitions, and some of the reasons to do it (mainly, of foundational value)
  • formal basic topology = the formal side of a basic pair
  • formal topology obtained by adding convergence of approximations
  • formal opens subsets form a frame (or locale)
  • notion of morphism between formal topologies
  • formal points and formal spaces
  • formal points = completely prime filters of the frame of f. open subsets


  • G. Sambin, Basic topologies, formal topologies, formal spaces (The Basic Picture 3), in preparation
  • S. Gebellato and G. Sambin, Pointfree continuity and convergence (The Basic Picture 4)

Silvio Valentini

(a) A primer for type theory

This part of the tutorial is meant to be a short introduction to that fragment of type theory which is relevant to formal topology.
Thus I intend to give a general introduction to Martin-Loef type theory first by focusing on the idea of inductively generated type and then by observing that this lead to the fact that the collection of the subsets of a given set cannot be a set.
Then I will recall that it is still possible to deal with subsets, and their algebra, within type theory if quantification over them is avoided or limited to the case of set-indexed families of subsets.

(b) A complete formalization of formal topology

The second part of my tutorial will deal with the problem of the completeness of the actual formalization of formal topology. Indeed the conditions that we require on the cover relation and the positivity predicate are clearly valid in any concrete topological space but nothing guarantee for their completeness. To solve this problem I will analyze the structure of the subsets of a Heyting algebra which correspond to the concrete closed and open sets of a topological space. In this way the rules for a complete formalization of constructive topology are disclosed.


For type theory, the classical references are the books by Martin-Löf and by Nordstrom-Peterson-Smith, but many other shorter introduction are available, also in the internet. As concerning the second part it can be useful to read my paper "A complete and predicative formalization of constructive topology" which can be found in my web page within the section "work in progress".

Statistiche web e counter web