Abstracts
Ioanna M. Dimitriou
(Bonn) 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 ZermeloFraenkel 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 Naprocheproject (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)
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.
Paula Henk (Amsterdam)
Abstract: The modal system GL (named after Gödel and Löb) is intimately connected to formal provability. Interpreting the GLmodality 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.

Impressum  20160114, BL, wwwmath (JMD) 