WORKSHOP: LEEDS SYMPOSIUM ON PROOF THEORY & CONSTRUCTIVISM

本次研究研讨会的目的是汇集世界领先的专家来发展证明论和建设性集合论的新主题，并追求一些尚未解决的核心问题。研讨会还将为人们提供一个讨论该领域现状和未来前景的机会。计划有关于序数分析、证明挖掘和计算复杂性、数学建构性基础和建构性方法的问题讨论。会议将由知名专家主持，他们将为讲习班的所有与会者调查这一主题的现状，并在此基础上引领事态发展。在更有限的层面上，经典的证明理论方法在各种各样的中心数学领域中发现了新的和重要的应用：例如，在数学证明和程序规范中隐含的复杂性界限的提取；用于证明算术、分析、组合学、拓扑学等基本定理的数学原理的相对强度的分层测量；以及各种计算复杂度类的表征，如多项式时间和线性空间。此外，由于Rathjen和Arai在Pi-1-2理解的序数分析方面的独立工作，纯证明理论本身目前正在经历重大的发展，这是一个强大的基础理论，现代数学的大多数部分可以在其中形式化和发展。这项工作最有趣的方面之一是其中使用了来自集合论的一些大的基本概念，这反过来又提出了许多关于证明论和集合论之间的相互关系的问题，以及它们的建设性或经典解释。这种相互联系是我们深入理解数学证明的基础。虽然集合论被认为是严谨的，并且已经赢得了为形式化数学提供全面系统的地位，但它以非计算性和非建设性而闻名。这在一定程度上对经典集合理论是正确的，但是集合没有本质上的非构造性和非计算性。建构性集合论（和数学）与传统的、经典的对应物区别在于，它坚持数学中存在定理的证明尊重建构性存在：一个存在的主张必须提供构造它的一个实例的方法。在Curry-Howard范式中，命题被视为类型，命题的构造性证明被视为各自类型的居民，从而以代数方式将程序和构造性证明的概念联系起来。范畴论提供了一个更新的，更具数学吸引力的抽象视角：然而，经典地，人们只想象一个基本的集合概念，有许多不同的类别（拓扑），它们的行为就像集合论的宇宙，但它们有自己的内在逻辑，本质上是建设性的。因此，建构性集合论构成了建构主义、集合论、证明论、类型论和拓扑论之间相互作用的主要场所，为建构性数学的发展提供了一个集合理论框架，并提供了一个精炼的框架，在这个框架中，在经典语境中不明显的概念之间的区别得以揭示。因此，建设性证明程序具有将数学推理的有效性扩展到尽可能广泛的背景的效果。该研讨会将是首批在利兹大学数学学院新成立的研究访客中心举行的研讨会之一。

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.