Constructive Mathematics Day

It is folklore that if a continuous equation has approximate solutions and - in a quantitative manner - at most one solution, then it has a (of course, uniquely determined) exact solution. I first review the standard ways to validate this heuristic principle both in classical mathematics and in constructive mathematics with countable choice, and then indicate how this can be carried over to the choice-free way of doing completions put forward by Mulvey, Stolzenberg, Richman, et al. Moreover, I sketch how the crucial "at most one" hypothesis can be obtained, by invoking Brouwer's fan theorem or Goedel's Dialectica interpretation, from appropriate preconditions of a qualitative nature.

In an intuitionistic and predicative setting, the notions of open and of closed subset are defined independently of each other, and yet one can observe a clear logical duality between them, which only classically is reduced to complementation. A generalization of topology, which I called the basic picture, can be developed in such a way that this duality is preserved. In particular, the independent treatment of open and closed subsets leads to a new "pointfree" notion, that of basic topology, in which the covering relation is accompanied by its dual, namely the positivity relation. The notions of formal point, formal space and continuous function are modified accordingly. The aim of my talk is to discuss the meaning of these definitions, and compare them with the corresponding notions in traditional topology and in locale theory. I will illustrate the claim that the new definitions are more expressive than the existing ones. I will propose some open problems related to this.

In which I intend to furnish "models" for CZF augmented by Brouwerian principles such as Continuous Choice, the Fan Theorem, and Bar Induction. This will also provide calibrations of the proof-theoretic strengths of systems which arise from augmenting CZF by these principles.

If we try to relate topos theory and constructive set theory (CST), we naturally try to interpret the logic of CST in terms of the categorical structure of toposes. However, there two difficulties that arise from the nature of CST. One is its reliance - as a set theory - on the "element of" relation as uniform structuring principle, for there is no simple correlate of this in categorical structure. The other is the distinction between classes and sets. A topos is normally viewed as a "category of sets". Then some classes - such as powerclasses - can be internalized as sets, but only by using impredicative features, while others must be dealt with externally to it in a metatheory (perhaps not so well defined).
Gambino's talk describes one solution using the Algebraic Set Theory of Joyal and Moerdijk. This works with a category "of classes", equipped with additional structure of "smallness" that allows one to discuss the sets within the category of classes.
I shall present an approach in the opposite direction, starting with a category "of sets" and then discussing classes within it. The basic idea, of "classifying categories", is an old one, but I shall try to explain it without relying on too much category theory, and I shall also relate it to my recent work with Erik Palmgren. The classifying category for a theory is - up to categorical equivalence - independent of the way the theory is presented, and in a certain sense represents the class of models of the theory.
In my paper with Palmgren, "Partial Horn logic and cartesian categories", we give a new treatment of partial logic, i.e. logic in which function symbols are interpreted as partial functions. It is particularly well adapted to providing a predicative proof of the initial model theorem for cartesian (or essentially algebraic) theories, a theorem that, in its better known special case for algebraic theories, underlies many techniques of universal algebra.
As an application, we use that same initial model theorem to construct classifying categories for cartesian theories. The classifying category is small and so, insofar as it represents the class of models of the theory, does so internally to the category of sets.
Although our results so far are for the limited class of cartesian theories, I shall explain why it is reasonable to hope for the same techniques to apply more widely. I conjecture that it will extend to (most of) the geometric theories that underly point-free topology, so the small classifying categories can also serve as topological spaces.

The aim of this talk is to introduce and study categorical models for constructive set theories within the context of Joyal and Moerdijk's Algebraic Set Theory. This approach provides a homogeneous presentation of various known models, and guidance in the development of new ones. The talk will end with a survey of independence results for constructive and intuitionistic set theories. The talk will be aimed to a general audience familiar with CST, and will not assume prior knowledge of Algebraic Set Theory.