General Information
This is the website of the research seminar of the Computational Logic Group at the
Institute of Discrete Mathematics and
Geometry of TU Wien. The seminar
usually takes places on Wednesdays from 10:00 to 11:00 in the
Zeichensaal 1, 8th floor, green area.
The seminar is organised by
J. Aguilera,
E. Fokina and
S. Hetzl.
If you want to receive talk announcements by e-mail, please subscribe to the
mailing list of this seminar on its
administration page.
Preliminary Programme
- September 23, 2026
-
Anders Lundstedt (Stockholm University)
title: Finitely non-standard models of Robinson arithmetic
abstract:
To the best of my knowledge, there is no systematic study of *finitely
non-standard* models of Robinson arithmetic—that is, there is no systematic
study of those models of Robinson arithmetic that have a non-empty finite set
of non-standard numbers. I will present a modest attempt at such a systematic
study. With addition and multiplication both defined recursively in the second
argument, the main conclusions are roughly: (1) addition and multiplication
with a non-standard first argument is "well-behaved"; and (2) addition and
multiplication with a non-standard second argument is "wild".
- October 7, 2026
-
Johannes Weiser (TU Wien)
title: t.b.a.
- October 14, 2026
-
Franziskus Wiesnet (TU Wien)
title: On the Limits of Recursive Characterizations in the Refined A-Translation
abstract:
The refined A-translation, due to Berger, Buchholz, and Schwichtenberg, is based on recursively defined classes of formulas in minimal arithmetic, in particular the classes of definite and goal formulas. Schwichtenberg and Wainer observed that one of the key proof-theoretic properties of definite formulas also holds for formulas outside the original class and asked whether all formulas satisfying this property admit a useful characterization.
In this talk, I show that this is not possible. More precisely, none of the four proof-theoretic properties associated with the formula classes in the refined A-translation admits a recursive characterization. We will also show how the original framework can nevertheless be extended, and present an extended formulation of the refined A-translation including conjunction.
- October 21, 2026
-
Elijah Schulzki (TU Wien)
title: t.b.a.
Archive
- 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: 2026-09-07, Stefan Hetzl.