Tuesday 11th of September
Venue:  Business School Maurice Keyworth SR 1.09

17:30– 18:00      Registration

18:00 – 19:00      The Feferman Lecture: Geoffrey Hellman: “Extending the Iterative Conception: a Height-Potentialist Perspective”

19:30 –                  Reception


Wednesday 12th of September
Venue:  Business School Maurice Keyworth SR 1.32

9:30 – 10:30        Per Martin-Löf: “Weyl’s attempted mediation between intuitionism and formalism”

10:30 – 11:00      Coffee break

11:00 – 12:00      Graham E. Leigh: “Formal truth and implicit commitment”

12.10 – 13:10      Laura Crosilla: “Weyl and a predicative concept of set”

13:10 – 15:00      Lunch break

15:00 – 16:00      Gerhard Jäger: “Weyl, Feferman and beyond”

16:00 – 16:30      Coffee break

16:30 –17:30       Stefania Centrone: “Husserl and Weyl”

17:40 – 18:40      Bahareh Afshari: “Fixed Points and Converse Modalities”


Thursday 13th of September
Venue: School of Mathematics, The Mall

9:30 – 10:30        Øystein Linnebo: “Predicativism and potential infinity”

10:30 – 11:00      Coffee break

11:00 – 12:00      Takako Nemoto: “Some properties of function spaces in reverse mathematics”

12.10 – 13:10      Stephen G. Simpson: “Predicativism: a reverse-mathematical perspective”

13:10 – 15:00      Lunch break

15:00 – 16:00      Michael Rathjen: “Weyl, Dummett, and Feferman on Indefiniteness”

16:00 – 16:30      Coffee break

16:30 –17:30       Arnon Avron: “Weyl Vindicated without Using Types”


Friday 14th of September
Venue: School of Mathematics, The Mall

9:30 – 10:30        Peter Aczel: Generalised-Predicative Constructivism (GPC)

10:30 – 11:00      Coffee break

11:00 – 12:00      Michael Detlefsen: “Weyl and Dedekind on Intuition and Proof”

12.10 – 13:10      Peter Dybjer: “Generalised predicativity, tests and the meaning explanations of intuitionistic type theory”

13:10 – 15:00      Lunch break

15:00 – 16:00      Maria Emilia Maietti: “The continuum from the predicative point of view of the Minimalist Foundation”

16:00 – 16:30      Coffee break

16:30 –17:30       Nik Weaver: “The limits of predicativity”

19:00 –                  Conference dinner


Peter Aczel

Title: “Generalised-Predicative Constructivism (GPC)”

Abstract: Hermann Weyl’s 1918 book, Das Kontinuum, provided one of the early presentations of a first order foundational system for the real numbers. At the time it made a significant contribution to the formal foundations of mathematics. It was a weak, predicative formal system that used classical logic.

The title of my talk refers to a comparitively strong, generalised-predicative, conceptual logical framework, GPC, for constructive mathematics. GPC uses intuitionistic logic and Per Martin-Löf’s dependent type theory, but it avoids any use of his equality types. My talk is intended to describe some of the ideas and concepts that led up to GPC.


Arnon Avron

Title: “Weyl Vindicated without Using Types”

Abstract: In his system W (named after Weyl), Feferman followed Weyl’s original system in using type extensively. However, W is only inspired by Weyl’s work; it is not really a faithful formalization of it. In fact, Feferman has completely ignored some important ideas that underlie Weyl’s system. In this talk we explain first what these ideas were, and provide a precise, completely faithful formalization of Weyl’s system in “Das Kontinuum”. We then show that certain set-theoretical (type-free) systems, which are formulated in the usual language that mathematicians nowadays employ, reflect much better (at least in our opinion) Weyl’s ideas. The main feature of our system is that instead of the guard provided by the types of Weyl, it uses a safety relation between formulas and finite sets of variables.


Laura Crosilla

Title: “Weyl and a predicative concept of set”

Abstract: I discuss a predicative concept of set under the light of the first chapter of Hermann Weyl’s “Das Kontinuum”.


Michael Detlefsen

Title: “Weyl and Dedekind on Intuition and Proof”

Abstract: In a footnote in Das Kontinuum, Weyl offered a striking challenge to what he took to be a view of the nature of proof supported by Dedekind in his famous essay on Number. This challenge and the view it challenged will be the focal concerns of my talk.


Peter Dybjer

Title: “Generalised predicativity, tests and the meaning explanations of intuitionistic type theory”

Abstract: Martin-Löf’s intuitionistic type theory is sometimes said to be “generalised predicative”. In this talk I will explain the meaning of this notion of predicativity and relate it to Martin-Löf’s “meaning explanations” for the judgments of this theory. These meaning explanations were first presented in the 1982 paper “Constructive Mathematics and Computer Programming”, but have subsequently been elaborated on in a number of lectures and papers. In particular I will discuss the relevance of the informal notion of “test” as a basis for these meaning explanations. The focus is on the meaning of higher order functions, and we explain why “formal neighbourhoods” in the sense of Martin-Löf 1983 provide a possible framework for testing type-theoretic judgements. In particular we make use of Coquand and Huber’s 2017 type-checking algorithm for formal neighbourhoods. I will also ask the question whether similar meaning explanations could possibly be given for impredicative type theories, such as the Calculus of Constructions.


Geoffrey Hellman

Title: “Extending the Iterative Conception: a Height-Potentialist Perspective”

Abstract: In his well-known, influential essay, “The Iterative Conception of Set”, George Boolos simply assumed that there are infinite limit stages, i.e. he didn’t derive the Axiom of Infinity from his axioms on stages; and, far from deriving Replacement, he came to doubt that is even “true” (i.e. in “the real world of sets”, to which he seems to have been committed). In this talk, we describe how simple axioms on stages can be added to Boolos’ to derive both Infinity and Replacement. In fact, we present two derivations of both, the second less open to a charge of circularity than the first. Interestingly, these derivations are available in a “height-potentialist” framework, deploying modal logic + logic of plurals; they conflict, however, with a “height-actualist” view (Boolos’, we suppose), committed to a fixed universe of all stages and all sets. Finally, we look at the situation from a predicativist standpoint, observing that the predicativist should welcome these derivations and the potentialist framework generally, especially in light of predicativist thought about the continuum as “indefinitely extensible”, but with the important change that at successor stages are formed all suitably definable sets of those of earlier stages.


Øystein Linnebo

Title: “Predicativism and potential infinity” (joint with Stewart Shapiro)

Abstract: We develop some predicativist approaches within the modal framework for potentiality that was developed in Linnebo (2010) and Linnebo and Shapiro (2018). The result is illuminating, as it puts predicativism into a more general framework and helps to sharpen some of its key theses.


Maria Emilia Maietti

Title: “The continuum from the predicative point of view of the Minimalist Foundation”

Abstract: One of the key features of the Minimalist Foundation – ideated with G. Sambin in [MS05] and completed in [M09]- is that of providing a predicative constructive framework where it is possible to distinguish different conceptions of the continuum, as those given by Dedekind, Cantor, Bishop.
The classical extension of the Minimalist Foundation includes modern representations of Weyl’s system as fragments of second order arithmetics with arithmetical comprehension and its real numbers can be shown not to form a set but only a proper collection.

[MS05] Maietti, M.E., Sambin, G.: Toward a minimalist foundation for constructive mathematics. In: L. Crosilla and P. Schuster (ed.) From Sets and Types to Topology and Analysis: Practicable Foundations for Constructive Mathematics, no. 48 in Oxford Logic Guides,pp. 91-114. Oxford University Press (2005)

[M09] Maietti, M.E.: A minimalist two-level foundation for constructive mathematics. Annals of Pure and Applied Logic 160(3), 319-354 (2009)


Takako Nemoto

Title: “Some properties of function spaces in reverse mathematics”

Abstract: Both Friedman-Simpson’s reverse mathematics and constructive reverse
mathematics use formal system of second order arithmetic. Because of this constraint, we need some trick to treat function space. In this talk, we will overview results on function space in reverse mathematics and see which can be done in “predicative” system.


Stephen G. Simpson

Title: “Predicativism: a reverse-mathematical perspective”

Abstract: Reverse mathematics is a foundationally-inspired research program which seeks to determine which axioms are needed to prove specific core-mathematical theorems. We present many examples of how reverse-mathematical research yields specific insights into foundational programs such as the finitism of Hilbert and the predicativism of Weyl and Feferman. From this perspective, we comment on Hilbert’s program of finitistic reductionism, and on a parallel program known as predicative reductionism. We discuss some fascinating reverse-mathematical open problems which are motivated by finitistic reductionism, predicativism, and predicative reductionism.