CONFERENCE
Type Theory, Constructive Mathematics and Geometric Logic
Théorie des types, mathématiques constructives et logique géométrique
1 – 5 May 2023
Scientific Committee
Comité scientifique
Marc Bezem (University of Bergen)
Olivia Caramello (University of Insubria)
Hajime Ishihara (Japan Advanced Institute of Science and Technology)
Henri Lombardi (Université de Franche-Comté)
Erik Palmgren (Stockholm University) was a member of the scientific committee. He passed away in November 2019. We deeply miss him.
Monika Seisenberger (Swansea University)
Organizing Committee
Comité d’organisation
Thierry Coquand (University of Gothenburg)
Sara Negri (University of Genova)
Michael Rathjen (University of Leeds)
Peter Schuster (University of Verona)
The debate between Hilbert and Brouwer, which took place at the beginning of the 20th century, is without doubt one of the most important events in the history of foundations of mathematics. In that debate Brouwer rejected transcendent proof methods and insisted on the exclusive use of intuitionist (or constructive) arguments for a conceptually correct development of mathematics. Hilbert, on the contrary, viewed these transcendental and non-effective proofs as the very essence of mathematical thinking. He introduced proof theory in the hope to justify these transcendent methods by purely effective means. While Gödel’s second incompleteness theorem is generally said to contravene Hilbert’s hopes, it is remarkable that Gödel himself insisted on the fact that his result does not contradict at all Hilbert’s program. In fact, the impact of Gödel’s result on Hilbert’s program was the topic of a discussion between Gödel, Herbrand and Neumann about the fundamental question of the scope of constructive mathematics.
Recent results in different fields of mathematics, such as proof theory, type theory, constructive algebra and categorical logic, shed new light on this question. For instance, proof theory seems to indicate precise limits to intuitionistic type theory, while on the other hand the Univalence Axiomallows for a rather unexpected extension of constructive methods. The goal of this workshop is precisely to bring together experts in these different fields to evaluate the impact of those new results on foundations of mathematics.
Le débat entre Hilbert et Brouwer, qui a eu lieu au début du 20ème siècle, est sans doute un des évènements les plus importants dans l’histoire des fondements des mathématiques. Dans ce débat, Brouwer rejetait les méthodes de preuve transcendantes et insistait sur l’utilisation exclusive d’arguments intuitionistes (ou constructifs) pour un développement conceptuellement correct des mathématiques. Hilbert au contraire voyait dans ces preuves transcendantes et non effectives l’essence même de la pensée mathématique. Il introduit la théorie de la démonstration dans l’espoir de justifier ces méthodes transcendantes par des arguments purement effectifs. Bien que l’on considère généralement que le deuxième théorème d’incomplétude de Gödel porte un coup d’arrêt à ces espoirs Hilbert, on peut remarquer que Gödel lui-même insiste sur le fait que son résultat ne contredit en rien le programme de Hilbert. En fait, la portée de ce résultat a fait l’objet d’un débat passionnant entre Gödel, Herbrand et Neumann ; ce qui est en jeu dans ce débat est la question fondamentale de quelle est l’étendue des mathématiques constructives.
Des résultats récents, venant de domaines différents comme la théorie de la démonstration, la théorie des types, l’algèbre constructive et la logique catégorique, apportent de nouveaux éléments sur cette question. Par exemple, la théorie de la démonstration semble indiquer des limites précises à la théorie intuitioniste des types, alors que, d’un autre côté, l’axiome d’univalence permet une extension inattendue des méthodes constructives. Le but de ce workshop est précisément de réunir des experts de ces différents domaines pour évaluer l’impact de ces nouveaux résultats sur les fondements des mathématiques.
SPEAKERS
Sergei Artemov (City University of New York) Serial Properties and the Provability of Consistency
Matthias Baaz (Vienna University of Technology) Constructivity within classical logic
Ulrich Berger (Swansea University) Program Extraction for Higher-Order Logic
Ingo Blechschmidt (University of Augsburg) New modal operators for constructive mathematics
Felix Cherubini (University of Gothenburg) A Foundation for Synthetic Algebraic Geometry
Anupam Das (University of Birmingham) Computational expressivity of (circular) proofs with fixed points
Tom De Jong (University of Nottingham) The set-theoretic and type-theoretic ordinals are the same
Martin Escardó (University of Birmingham) Ordinals in HoTT/UF
Simon Henry (University of Ottawa) On Compact Haussdorf locales in (presheaf) toposes
Joost Joosten (University of Barcelona) Formalised provability in constructive arithmetic
Peter Lumsdaine (Stockholm University) The cumulative hierarchy in type theory
Samuele Maschio (University of Padua) Implicative algebras, supercompactness and assemblies
Dale Miller (Inria Saclay) From axioms to synthetic inference rules via focusing
Sarah Negri (University of Genoa) Gödel, Barr, andmodal embeddings
Takako Nemoto (Japan Advanced Institute of Science and Technology) On the decomposition of WKL!!
Ming Ng (Queen Mary University of London) Foundations in Non-Archimedean & Arithmetic Geometry: Topology vs. Set Theory
Nicola Olivetti (Aix-Marseille Université) A taste of Intuitionistic Modal Logic: normal and non-normal modalities
Iosif Petrakis (Ludwig Maximillians-University of Munich) From algebras of complemented subsets to swap algebras
Thomas Powell (University of Bath) Recursive inequalities in applied proof theory
Luigi Santocanale (Aix-Marseille Université) Lifting structure(s) from the base to the total category of a predoctrine
Andrew Swan (Carnegie Mellon University) Oracle Modalities
Steve Vickers (University of Birmingham) Dependent type theory of point-free topological spaces
Chuangjie Xu (SonarSource) From Double-Negation Translation of Proofs to
Static Analysis of Code
Ihsen Yengui (University of Sfax) The Gröbner Ring Conjecture
SPONSOR
