权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

WORKSHOP: LEEDS SYMPOSIUM ON PROOF THEORY & CONSTRUCTIVISM

研讨会：利兹证明论研讨会

基本信息

批准号：
EP/G058024/1
负责人：
Michael Rathjen
金额：
$ 2.09万
依托单位：
University of Leeds
依托单位国家：
英国
项目类别：
Research Grant
财政年份：
2009
资助国家：
英国
起止时间：
2009 至无数据
项目状态：
已结题

来源：
https://gtr.ukri.org/projects?ref=EP%2FG058024%2F1
关键词：
WORKSHOP LEEDS SYMPOSIUM PROOF THEORY

项目摘要

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.

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