ABM 2017, Arbeitstagung Bern-München
Mathematics Institute LMU, Rooms B 132 and B 349.
18:30, Cafe Puck, Türkenstrasse 33
Thursday Talks (Room B 132)
09:30-10:30, Gerhard Jäger: "Remnants from the Bookshelf" slides
10:30-11:00, Coffee break
11:00-11:45, Matthias Eberl: "Finitistic higher order logic"slides
11:45-12:30, Ulrik Buchholtz: "Groups and higher groups in homotopy type theory"slides
12:30-15:00, Lunch break
15:00-15:45, Silvia Steila: "How large are proper classes?"slides
15:45-16:30, Vasco Brattka: "The Computational Content of the Vitali Covering Theorem"slides
16:30-16:45, Coffee break
16:45-17:30, Josef Berger (jww Gregor Svindland): "A constructive supporting hyperplane theorem"
17:30-18:00, Lukas Jaun: "Category Theory and Universes in Explicit Mathematics"slides
18:30, Los Faroles, Nordendstrasse 26
Friday Talks (Room B 349)
09:30-10:15, Sam Sanders (jww Dag Normann): "Lost in translation: From Hilbert-Bernays' Grundlagen to second-order arithmetic"
10:15-11:00, Christoph-Simon Senjak: "Using DiffArrays to optimize Decompression"
- Ulrik Buchholtz: "Groups and higher groups in homotopy type theory"
Homotopy type theory (HoTT) is both a theory of homotopy types
and of infinity groupoids, because these are the same from the point of
view of Grothendieck's homotopy hypothesis. But the intuitions can be very
different, and I will explain how homotopy type theory provides a new view
even of ordinary group theory. Along the way, I'll mention some
applications to nominal reasoning about syntax with binding.
- Matthias Eberl: "Finitistic higher order logic"
We follow a finitistic approach initially presented by Jan Mycielski for first order logic (locally finite theories, JSL '86).
Different to Mycielski's approach we use a model theory based on the idea that all infinite sets are replaced by indefinitely
extensible sets --- formally these are families of sets. The interpretation then uses a kind of reflection principle whereby
the universal quantifier ranges over sufficiently large finite sets, not over infinite sets. This works fine for first order
logic in which the objects are finite and only infinite sets of objects are approximated by finite sets.
In order to extend this idea to higher order logic in form of simple type theory (STT) we additionally have to consider
infinite objects (functions), which are approximated themselves. In order to formulate a finitistic version thereof we
approximate function spaces of higher types by finite sets of finite approximations of these functions. These finite function
spaces are related by partial surjections (on higher types defined as logical relations) and we introduce a new notion of a
limit for them. The limit structure is then equipped with a family of partial equivalence relations (PERs), approximating equality.
There is a one-to-one correspondence between the families of finite sets of finite approximations and the infinite limit structures.
Different to domain theory we use total functions in order to have the usual classical truth values and use STT as a higher order logic.
- Sam Sanders (jww Dag Normann): "Lost in translation: From Hilbert-Bernays' Grundlagen to second-order arithmetic"
Large parts of mathematics are studied indirectly via countable approximations, also called codes.
Perhaps the most prominent example is the program Reverse Mathematics, as founded by Friedman
and developed extensively by Simpson. Indeed, subsystems of second-order artihmetic are used,
although the original Hilbert-Bernays system H includes higher-order objects. It is then a natural
question if anything is lost by the restriction to the countable imposed by second-order arithmetic.
We show that this restriction fundamentally distorts mathematics. To this end, we exhibit a number
of theorems, including the Cousin and Lindeloef lemmas, from basic-to-advanced mathematics
which involve uncountable objects and cannot be proved in any (higher-type version) of Pi_k^1
-comprehension. These theorems are however provable in full (higher-order) second-order
arithmetic and intuitionism, as well as often in (constructive) recursive mathematics. Furthermore,
the 'countable counterpart' of Cousin's lemma is equivalent to weak Koenig's lemma. Finally,
the Lindeloef lemma seems acceptable in predicativist mathematics, but it nonetheless yields
the impredicative system of Pi_1^1-comprehension when combined with Feferman's mu operator.
- Christoph-Simon Senjak: "Using DiffArrays to optimize Decompression"
In our thesis we gave verified compression and decompression
algorithms for the Deflate compression standard. Doing this in a
purely functional manner resulted in code which was either hard to
read and verify or inefficient. We use a solution which is convenient
by using a simple trick which allows for using destructive array
updates inside a purely functional context, without the need of monads
or linear typing. In our talk, we will show our previous approaches
and how we implemented the solution using diffarrays.
- Silvia Steila: "How large are proper classes?"
In 1923 von Neumann stated the first version of his axiom "Limitation of Size": a class is a proper class
if and only if there is a one-to-one correspondence between it and V. This formulation implies the existence
of a global well-ordering of the universe over NGB. The aim of this talk is to present different statements which deal
with largeness properties of proper classes. We compare them and some of their consequences over a conservative second
order version of Kripke Platek Set Theory.
11. Dezember 2017