Hamburg Set Theory Workshop 2016
18 January 2016
Hamburg (Germany)

The Hamburg Set Theory Workshop 2016 is part of the ML Colloquium of the Arbeitsbereich Mathematische Logik und interdisziplinäre Anwendungen der Logik. Everyone is cordially invited to attend. There will be an informal lunch in the student restaurant (Mensa) and an informal dinner.

Location. Room 415, 4th Floor, Geomatikum, Bundesstraße 55, 20146 Hamburg.

Abstracts

Ioanna M. Dimitriou (Bonn)
Revisiting Paulson's formal proof of AC in L, with a view on natural language

Abstract: Lawrence Paulson’s Isabelle formalization of Gödel’s relative consistency result for the Axiom of Choice stands out as an early formalization of a long and sophisticated theory including a general introduction to Zermelo-Fraenkel set theory. The metamathematical aspects of the theorem and its proof present veritable challenges. Peter Koepke and I are currently pursuing a project to understand and revise the formalization into a more "readable" form, in parallel with modern introductions to set theory and constructibility theory. Eventually methods of the Naproche-project (Natural proof checking) will be brought in to obtain a natural language layer on top of the new Isabelle text. We hope that such endeavours will facilitate the public acceptance of formal mathematics.

Sandra Uhlenbrock (Münster)
Hybrid Mice with Finitely Many Woodin Cardinals from Determinacy

Abstract: Mice are countable sufficiently iterable models of set theory. Hybrid mice are mice which are equipped with some iteration strategy for a mouse they are containing. This allows them to capture stronger sets of reals.

W. Hugh Woodin has shown in so far unpublished work that boldface Π¹_n+1-determinacy implies that M_n^#(x) exists and is ω₁-iterable for all reals x. We will generalize parts of this to hybrid mice and levels of determinacy in the L(IR)-hierarchy.

Paula Henk (Amsterdam)
Solovay's Technique to determine modal logics of provability

Abstract: The modal system GL (named after Gödel and Löb) is intimately connected to formal provability. Interpreting the GL-modality as a provability predicate of some sufficiently strong arithmetical theory (for example Peano Arithmetic), GL captures exactly what is provable in this theory, in propositional terms, about provability in itself. We say that GL is arithmetically sound and complete.

I will explain this result, focusing in particular on the proof of arithmetical completeness due to Robert Solovay. The main idea is to simulate a given GL-Kripke model inside PA, by constructing a function that climbs up the accessibility relation of the Kripke model in a rather specific manner. For each node w in the Kripke model, the construction yields an undecidable arithmetical sentence S_w representing w in PA.

Time permitting, I will also show how Solovay’s method can be extended to bimodal systems, where one of the modalities corresponds to ordinary provability, and the other one to some nonstandard notion of provability.