Schriftzug: Fachbereich Mathematik 
  UHH > Fakultäten > MIN-Fakultät > Mathematik > Bereiche > Mathematische Logik   STiNE |  KUS-Portal |  Sitemap Suchen Hilfe there is no english version of this page  

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.


Larger map

10:30-12:00 Ioanna M. Dimitriou (Bonn)
Revisiting Paulson's formal proof of AC in L, with a view on natural language
12:00-14:15 LUNCH BREAK
14:15-15:45 Sandra Uhlenbrock (Münster)
Hybrid Mice with Finitely Many Woodin Cardinals from Determinacy
15:45-16:00 Break
16:00-17:30 Paula Henk (Amsterdam)
Solovay's Technique to determine modal logics of provability

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


  Seitenanfang  Impressum 2016-01-14, BL, wwwmath (JMD)