Computational Logic Seminar


Archive (summer term 2026)

June 10, 2026
Alexander Zach
title: Der Kleenesche Rekursionssatz: Beweis und Anwendungen
abstract:
Der Kleenesche Fixpunktsatz ist das formale Fundament für Selbstreferenz in der Berechenbarkeitstheorie. Wir beweisen ihn zunächst und beschäftigen uns anschließend mit seinen theoretischen sowie praktischen Auswirkungen: Wir beweisen den Satz von Rice, welcher die Unentscheidbarkeit von nicht-trivialen semantischen Eigenschaften liefert, betrachten selbstreproduzierende Programme (sogenannte Quines) und die Grundlagen von Computerviren.
April 22, 2026
Andrea Volpi (University of Warsaw)
title: The strength of Ramsey's theorem for $\a$-large sets
abstract:
We present joint work with Lorenzo Carlucci and Konrad Zdanowski on Ramsey-like principles $\RT^{!\alpha}_k$, extending Ramsey's theorem to colorings of exactly $\alpha$-large finite subsets of $\mathbb{N}$ in the sense of Ketonen and Solovay. For each countable $\alpha < \Gamma_0$ and $k \geq 2$, we show over $\RCA_0$ that these principles form a hierarchy matching closure under transfinite iterations of the Turing jump along $\alpha$, yielding a fine-grained classification between $\ACA_0$ and $\ATR_0$.
April 15, 2026
Noam Greenberg (Victoria University of Wellington)
title: Forcing, untagging, and graph colourings
abstract:
I will present a family of notions of forcing that are useful in showing that certain graphs don't have countable colourings in particular Borel classes. This is joint work with Lecomte, Turetsky and Zeleny. This kind of forcing was also used in work with J. Miller, Soskova, and Turetsky to find the Borel rank of classes of Turing degrees defined by iterating the Turing jump.
April 1, 2026
Gian Marco Osso (University of Udine)
title: Laver forcing and ATR_0
abstract:
Using forcing to prove "effective" theorems requires an understanding of the effective properties of the forcing notions at play. In the context of Laver forcing one key property is "pure decision", corresponding to a partition theorem for Laver trees. This theorem can be seen as a combinatorial common core of determinacy and the Galvin-Prikry theorem. Restricting our attention to open partitions, both determinacy and Galvin-Prikry are at the level of ATR_0. I will present work in progress (joint with Alberto Marcone) on the effective content of the Laver partition theorem for open sets.


Last Change: 2025-09-21, Stefan Hetzl.