May 6: Juliet Floyd: Rigor and Infinity
9:10-10:10
Abstract:
In accordance with the recent turn toward practice-based approaches to the philosophy of mathematics, I explore and stress some of the varieties of rigor encountered in the emergence of modern mathematical philosophy. In practice rigor inhabits a dynamic and evolving place, where contestation and change, generalization and reduction, conceptual innovation, interpretation, deepening and loosening of standards are to be expected. It is more of an occasion sensitive notion than is sometimes appreciated: i.e., it relies upon certain understandings of how context, needs, expectations, problems, traditions and purposes matter. Every rigorization leaves an interpretive residue behind, the trail where the human serpent brings philosophy and knowledge into the garden. I shall argue that this lesson, centrally embedded in modern mathematical philosophy, is important to how we treat the concept of rigor. I focus on Dedekind’s rigorization of the infinite, touching upon subsequent rigorizations of certain aspects of his thought by Russell, Zermelo and Turing.
To Programme page
To Meeting page
May 6: Dana Scott: Applying logic to geometry
10:10-11:10
Abstract:
Either by the Compactness Theorem or with the use of
ultraproducts, we know how to add infinitesimals to the real line.
Conway even has a definable introduction of infinitesimals, but
perhaps the properties for analysis of his surreal numbers are not
yet completely understood. In Intuitionistic Logic, synthetic
differential geometry -- much championed by Lawvere and many others
-- makes use of an interesting theory of infinitesimal structures
*inconsistent* in Classical Logic. Cohen with forcing introduced
generic reals, and Solovay introduced random reals. Using Recursion
Theory, Kolmogorov -- and many others -- have given interpretations
of randomness. Recently, Alex Simpson found that a more "canonical"
idea of randomness could be defined by using "pointless spaces". The
speaker noted that -- by using Boolean-valued models -- Simpson's
spaces have a very satisfactory notion of point, and he hopes to
encourage more investigation of this kind of model. The Boolean-
valued model also adds random elements to other structures and gives
every logical formula involving parameters a natural probability.
To Programme page
To Meeting page
May 6: Hugh Woodin: Is V an ultimate version of L?
11:40-12:40
Abstract:
Gödel's axiom V = L refutes fairly modest large cardinal axioms and so it is arguably false on the basis of the principles of infinity on which set theory is founded. The search for generalizations of L which are compatible with large cardinal axioms has played a fundamental role in set theory but it has always seemed impossible for this search to ever yield an ultimate version of L. The situation has now changed.
To Programme page
To Meeting page
May 6: Ieke Moerdijk: Sheaves, Realizability and the Axiom of Multiple Choice
13:40-14:40
Abstract:
The aim of algebraic set theory is to develop a strengthening of topos theory which allows one to construct models of set theory, while sharing the good stability properties of toposes like being closed under sheaf and realizability extensions. For predicative set theories with inductive (or W-) types, the proof of these stability properties requires an additional axiom, which we call the axiom of multiple choice. We will discuss this axiom, its relation to some axioms of CZF, and its role in formal topology. (Joint work with Benno van den Berg.)
To Programme page
To Meeting page
May 6: Michael Rathjen: The jump to impredicativity
14:40-15:40
Abstract:
By adding Powerset and (full) Separation to CZF (Constructive Zermelo Fraenkel Set Theory)
one arrives at intuitionistic Zermelo Fraenkel Set Theory, IZF, which is of the same strength as
ZF. One is naturally led to separate these steps, giving rise to the theories CZF+Separation and CZF+Powerset.
The talk will mainly be concerned with CZF+Powerset and only briefly with CZF+Separation.
An additional topic of the talk will be relativized proof theory. While ordinal-theoretic proof theory
cannot yet reach theories of this strength it is nonetheless interesting
to ponder whether some of its techniques can be relativized to provide information
about strongly impredicative theories.
To Programme page
To Meeting page
May 6: Peter Aczel: The type theoretic conception of set
16:10-17:10
Abstract:
The type-theoretic conception of set provides an
interpretation of CZF in a dependent type theory. When the logic of
the type theory is made classical by adding excluded middle, an
interpretation of ZF is obtained. When rules, analogous to Bertrand
Russell's Axiom of Reducibility, are instead added, an interpretation
of IZF is obtained. That interpretation, when combined with Harvey
Friedman's double negation interpretation of ZF in IZF provides
another interpretation of ZF.
I will provide a sketch of the type-theoretic conception of set and
claim that it provides a more explanatory conception than the
classical iterative conception. The latter conception provides an
elegant informal description of the cumulative hierarchy, but not much
of an explanation.
If there is time I will also present some results concerning a very
weak constructive set theory that is just strong enough to represent a
constructive version of Jensen's rudimentary set functions.
To Programme page
To Meeting page
May 7: Andreas Blass: Games
9:00-10:00
Abstract:
I plan to discuss a number of aspects of games (meaning two-player, zero-sum games of perfect information) arising in contexts that include classical set theory, computability theory, and constructive logic.
To Programme page
To Meeting page
May 7: Alex Simpson: Pragmatic Motivations for Constructive Set Theory
10:00-11:00
Abstract:
Constructive set theories can be motivated on
ideological grounds as formalizing constructively
acceptable forms of mathematical reasoning. Alternatively,
they can be motivated on pragmatic grounds as formalizing
the reasoning valid internally in natural classes
of mathematical models. I will focus on the latter viewpoint
and discuss some of the constructive set theories that arise
naturally in this way.
To Programme page
To Meeting page
May 7: Nik Weaver: Intuitionism and the liar paradox
11:30-12:30
Abstract:
The concept of informal mathematical proof considered in intuitionism is susceptible to a version of the liar paradox. The paradox is defused by recognizing a subtle distinction between indefinitely extensible and heuristic collections. This leads to a general resolution of the classical semantic paradoxes.
To Programme page
To Meeting page
May 7: Erik Palmgren: Set, Setoids and Groupoids. On set-like categories in type theory and
set theory
14:00-15:00
Abstract:
When formalising constructive mathematics in Martin-Löf type theory it is standard to use setoids (types with equivalence relations) to interpret sets. The notion of preset in the sense of Bishop style mathematics is well captured by a type equipped with its identity type as equivalence relation. However when it comes to families of sets it seems that there is a choice between proof relevant index sets (groupoids) and proof irrelevant index set (setoids). We aim to discuss these issues and the relation to the groupoid model of type theory by Hofmann and Streicher.
To Programme page
To Meeting page
May 7: Peter Koepke: Ordinal Orientated Set Theory
15:30-16:30
Abstract:
Kurt Gödel's model L of constructible sets which he introduced to show the relative consistency of the axiom of choice and of the continuum hypothesis is based on the idea of recursively constructing sets from (the collection of) previously constructed sets. The recursion is indexed by ordinals, and indeed we demonstrate in our talk that constructibility theory can be construed as a kind of arithmetic, extended onto the class of all ordinals. A set of ordinals is constructible if and only if it is computable by a generalized Turing machine operating on ordinals. The paradigm of computation may allow to link constructive approaches with classical set theory.
To Programme page
To Meeting page
May 7: Benno van den Berg: Inductive definitions and derived rules for constructive set theory
15:30-16:30
Abstract:
In this talk I will show how one may use sheaf-theoretic methods to obtain derived rules for the constructive set theory CZF. Such methods have already been successfully applied in the impredicative setting. To make these methods work in the predicative setting one has to develop some theory concerning inductive definitions as well as some formal topology. I will give an overview of this material and indicate how they can be used to obtain a derived fan rule and a derived bar induction rule for (extensions of) CZF. (Joint work with Ieke Moerdijk.)
To Programme page
To Meeting page
May 7: Harvey Friedman: Three aspects of constructive set theory and beyond
17:30-18:30
Abstract:
We discuss three directions in constructive set theory. The formalization of Bishop's constructive mathematics through the system B, a conservative extension of HA. The strong conservative extension of PA called ALPO = analysis with the limited principle of omniscience. And forms of intuitionistic ZF, for which there are still major open problems. We also discuss the prospects for intuitionistic large cardinal axioms.
To Programme page
To Meeting page