May 2-3, 2019, Ludwig-Maximilians-Universität München
| 19:00 | Welcome dinner at Atzinger, Schellingstr. 9 |
| 09:25 | Opening |
| 09:30 - 10:15 | Klaus Mainzer: From Proof Theory to Proof Assistants: Challenges of Responsible Software and AI (slides) |
| 10:15 - 10:45 | Coffee break |
| 10:45 - 11:30 | Chuangjie Xu: Ordinal Notations via Simultaneous Definitions (slides) |
| 11:30 - 12:15 | Franziskus Wiesnet: An Algorithmic Approach for Maximal Objects in Algebra |
| 12:15 - 15:00 | Lunch break |
| 15:00 - 15:45 | Gerhard Jäger: Predicative Hierarchies (slides) |
| 15:45 - 16:15 | Coffee break |
| 16:15 - 17:00 | Michael Bärtschi: Parameter-Free Versions of ATR₀ and Related Theories (slides) |
| 17:00 - 17:45 | Lukas Jaun: Category Theory in Explicit Mathematics (slides) |
| 19:00 | Dinner at Los Faroles, Nordendstr. 26 |
| 09:30 - 10:15 | Peter Hertling: Trees Describing Wadge Degrees and Topological Weihrauch Degrees of Multivalued Functions (slides) |
| 10:15 - 10:45 | Coffee break |
| 10:45 - 11:30 | Iosif Petrakis: Categories and Bishop Sets (slides) |
| Michael Bärtschi: Parameter-Free Versions of ATR₀ and Related Theories |
| Working in ACA₀ as our base theory, we will discuss relations among set parameter-free versions of ATR₀ and analogous variants of FP₀. While this restriction is not significant for ATR₀, the set parameter-free versions of FP₀ exhibit reduced proof-theoretic strength. This can be shown by considering parameter-free variants of arithmetic transfinite recursion with limited height. |
| Peter Hertling: Trees Describing Wadge Degrees and Topological Weihrauch Degrees of Multivalued Functions |
| We introduce notions of continuous strong Weihrauch reducibility and of continuous Weihrauch reducibility for functions with range in a preordered set. Then we associate with such functions certain labeled forests and trees and show that Wadge reducibility, continuous strong Weihrauch reducibility and continuous Weihrauch reducibility between such functions can be characterized by suitable reducibility relations between the associated forests when they are defined. This leads to a combinatorial description of the initial segments of these three hierarchies for those functions defined on the Baire space that have countable range in a bqo set and that are Sigma_2^0-measurable with respect to the reverse Alexandroff topology on the bqo set. Furthermore, we show that the characterization of the topological reducibility relations for bqo-valued functions can be used in order to obtain a similar characterization for the usual Wadge reducibility relation, the continuous strong Weihrauch reducibility relation, and the continuous Weihrauch reducibility relation for multi-valued functions with finite range. |
| Lukas Jaun: Category Theory in Explicit Mathematics |
| I will give an overview of three candidates for the category of sets in explicit mathematics and describe some notions of universes in this setting. |
| Iosif Petrakis: Categories and Bishop Sets |
| The influence of category theory to Bishop's set theory is found in the definition of a subset, and in Richman's notion of a family of objects of a category indexed by a set. As a special case, a set-indexed family of Bishop sets is a functor between the corresponding categories. We examine the relation between the equality defined on a totality and its corresponding category, and we prove, as in the case of Martin-Löf type theory (MLTT), a Yoneda lemma for set-indexed families of Bishop sets, and also for directed families of Bishop sets. Finally, we discuss a possible variation to Palmgren's theory CETCS, a constructive and predicative version of Lawvere's Elementary Theory of the Category of Sets (ETCS), which is obtained abstracting on category-theoretic properties of setoids in a universe in MLTT. |
| Chuangjie Xu: Ordinal Notations via Simultaneous Definitions |
| We define an ordinal notation system simultaneously with its ordering. Our simultaneous definitions generate only the ordinal terms in Cantor normal form which are in one-to-one correspondence with the ordinals below ε₀. We implement the ordinal notation system as inductive-inductive-recursive definitions in the Agda proof assistant. |
| Franziskus Wiesnet: An Algorithmic Approach for Maximal Objects in Algebra |
| The existence of ideal objects, such as maximal ideals in nonzero rings, plays a crucial role in commutative algebra. These are typically justified using Zorn's lemma, and thus pose a challenge from a computational point of view. We take an alternative approach based on Kreisel's no counterexample interpretation and sequential algorithms. We first give a computational interpretation to an abstract maximality principle in the countable setting via an intuitive, state based algorithm. We then carry out a concrete case study, in which we give an exact algorithmic account of the result that in any commutative ring, the intersection of all prime ideals is contained in its nilradical. |