WORKSHOP: LEEDS SYMPOSIUM ON PROOF THEORY & CONSTRUCTIVISM

The objective of this research workshop is to bring together leading world experts to develop newly emerging themes in proof theory and constructive set theory, and to pursue central questions which have remained unresolved for some time. The workshop will also provide an opportunity for people to discuss the state of and future prospects for the field. It is planned to have problem sessions on ordinal analysis, proof mining and computational complexity, constructive foundations, and constructive methods in mathematics. They will be chaired by renowned experts who will survey the current state of the subject for all participants of the workshop and lead developments from there. At the more finitistic level, classical proof theoretic methods are finding new and important applications in a wide variety of central mathematical fields: e.g. to the extraction of complexity bounds implicit in mathematical proofs and program specifications; to the hierarchical measurement of the relative strengths of mathematical principles used in proving fundamental theorems of arithmetic, analysis, combinatorics, topology etc.; and to the characterization of various computational complexity classes such as polynomial time and linear space. In addition, pure proof theory itself is presently undergoing significant development as a result of the independent work of Rathjen and Arai on the ordinal analysis of Pi-1-2 Comprehension, a strong foundational theory in which most parts of modern mathematics can be formalised and developed. One of the most intriguing aspects of this work is the use therein of certain large cardinal notions from set theory, and this in turn raises many questions about the inter-relationships between proof theory and set theory, and their constructive or classical interpretations. Such interconnections are fundamental to our deeper understanding of mathematical proof.While set theory is identified with rigour and has earned the status of providing a full scale system for formalizing mathematics, it has a reputation for being non-computational and nonconstructive. This is to some extent true for classical set theory but there is nothing intrinsically non-constructive and non-computational about sets. Constructive set theory (and mathematics) distinguishes itself from its traditional, classical counterpart by insisting that proofs of existential theorems in mathematics respect constructive existence: that an existential claim must afford means for constructing an instance of it. Within the Curry-Howard paradigm, propositions are viewed as types and constructive proofs of propositions are viewed as inhabitants of their respective types, thereby connecting the concepts of programme and constructive proof in an algebraic way. Category theory provides a newer, more mathematically appealing abstract perspective: whereas, classically, one imagines just one basic notion of set , there are many different categories (toposes) that behave like set-theoretic universes, but have their own internal logic which is essentially constructive. Constructive set theory thus constitutes a major site of interaction between constructivism, set theory, proof theory, type theory and topos theory, providing a set theoretical framework for the development of constructive mathematics, and a refining framework within which distinctions between notions which are not apparent in the classical context, become revealed. Constructive proof procedures thus have the effect of extending the validity of mathematical reasoning to the widest possible context. The Workshop will be one of the first to be held in the newly established Research Visitors' Centre within the School of Mathematics at the University of Leeds.