ABM 2017, Arbeitstagung Bern-München
14.12.2017-15.12.2017

Thursday dinner

Abstracts

• 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.
  

  Accommodation

  • Das Hotel, Türkenstrasse 35.

  Organizers

  • Iosif Petrakis
  • Michael Bärtschi

  Last change

  11. Dezember 2017