Hamburg Set Theory Workshop 2016
18 January 2016
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.
Ioanna M. Dimitriou
Revisiting Paulson's formal proof of AC in L, with a view on natural language
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 Π1n+1-determinacy implies that Mn#(x) exists and is ω1-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.