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
"Besprechungsraum" in Freihaus, 5th floor, green area.
The seminar is
organised by E. Fokina and
If you want to receive talk announcements by e-mail, please subscribe to the
mailing list of this seminar on its
- December 20, 2023
- November 29, 2023
title: The compactness number of Gödel logic
We give a proof of the theorem that the compactness number of first-order Gödel logic with identity is the least \omega_1-strongly compact cardinal.
- November 22, 2023
title: Reverse Mathematics: Limits of Determinacy Axioms in Second-Order Arithmetic and Beyond
I will introduce the method of Reverse Mathematics trough the question: « What are the right axioms to play infinite games ». We will then generalise a theorem of Montalbán and Shore. They showed what was the limit of determinacy when one work in the realm of natural numbers and set of natural numbers. We will use their arguments and add ours to prove that (almost) the same bounds show up in higher order set theoretic settings.
- November 8, 2023
Selwyn (Keng Meng) Ng
title: The strength of the 4 colour theorem
We study the reverse mathematical strength of the 4-colour theorem and various related principles. We show that the 4 colour theorem effectively reverses to WKL0, but the 8-colour theorem reverses, but not effectively. We also study the relationship between the k-colour theorem for all values of k.
- Tuesday, October 10, 2023, 10:00am, Besprechungsraum
title: Learning equivalence relations
I will report on an ongoing project with Ted Slaman and Tomasz Steifer that aims to develop a framework for the algorithmic learning of equivalence relations studied in descriptive set theory. Inspired by recent work of Fokina, Kötzing and San Mauro who formulated a framework to learn the isomorphism relation on countable classes of structures, we introduce frameworks that aim to formalize what it means for an equivalence relation on a Polish space to be learnable. Our main results connect learnability in this framework to the descriptive complexity of the equivalence relation. We also show that the set of learnable Borel equivalence relations is co-analytic complete in the codes and rediscover longstanding open questions about Borel equivalence relations.
- September 27, 2023
title: How to learn families of algebraic structures
In this talk, we present some novel results in the area of algorithmic learning theory for countable families of countable structures.
We work within the framework introduced by N. Bazhenov, E. Fokina, T. Kotzing, and L. San Mauro. Here, a learner receives larger and larger pieces of an arbitrary copy of a structure and, at each stage, is required to output a conjecture about the isomorphism type of such a structure. The learning is successful if the conjectures eventually stabilize into a correct guess.
However, the framework did not allow us to nicely calibrate the nonlearnability of a family of structures. The starting point to address this issue was to show that a family of structures is learnable if and only if its learning domain is continuously reducible to the relation E_0 of eventual agreement on reals. Then, by replacing E_0 with other equivalence relations, one unlocks the promised hierarchy of learning problems; this led us to the definition of E-learnability. We give some results on this hierarchy, and we study where other classical learning criteria coming from algorithmic learning theory lie in this hierarchy. What we present here is joint work with N. Bazhenov, S. Jain, A. Marcone, L. San Mauro, and F. Stephan (hopefully more are coming).
- Friday, September 22, 1:30pm, Dissertantenraum
title: A combinatorial principle weak over weak systems yet strong over
Better quasi orders (henceforth bqos) are a strengthening of
the notion of well quasi order. Even if their definition is more
complicated, the former enjoy nice closure properties, that make them,
in a way, easier to work with than the latter: this feature made bqos an
instrumental tool in proving landmark results like Nash-Williams'
theorem and Laver's theorem. From the reverse mathematical point of
view, the study of bqos is an interesting area still full of open
In this talk, we will focus on a property of non-bqos, the so-called
minimal bad array lemma, and in particular one version of it that we
will call MBA- . We will show that MBA- has a very odd behavior when
it comes to its reverse-mathematical strength, namely
* over ATR 0, MBA- can be seen to be equivalent to the very strong
principle of Pi 1 2 - comprehension, yet
* over ACA 0, MBA- does not imply ATR 0.
In order to prove this result, we will provide a characterization of the
quasi-orders that ACA 0 proves to be bqos.
This is joint work with Anton Freund, Alberto Marcone, and Fedor
- September 20, 2023, 10:00, Dissertantenraum
- Alexandra Bergmayr-Mann
title: Gleason's Theorem
Gleason's theorem belongs to one of the most important results in the foundations of quantum mechanics and especially in quantum logic, since it has a deep impact on quantum theory. Besides a simplified version of Gleason's theorem, known as Bell's theorem, which disproves realistic non-contextual hidden variable theories, the Kochen and Specker theorem can be seen as a consequence of Gleason's theorem, in combination with logical compactness. A similar argument as in the derivation of the Kochen Specker theorem from Gleason's theorem can be used to prove strong results about finite sets of rays in Hilbert space. Lastly, we will see that Gleason's theorem also admits an effective proof.
- August 17, 2023, 10:00, Dissertantenraum
Yong Cheng, Wuhan University
title: There are no minimal effectively inseparable theories with respect to interpretation
In this talk, we examine the limit of the first incompleteness theorem (G1). We examine the question: are there minimal theories for which G1 holds. The answer of this question depends on how we define the notion of minimality. The notion of interpretation provides us a general method to compare different theories in distinct languages. We examine the question: are there minimal theories for which G1 holds with respect to interpretation. We know that G1 holds for essentially undecidable theories, and it is proved in  that there are no minimal essentially undecidable theories with respect to interpretation. G1 holds for effectively inseparable (EI) theories and effective inseparability is much stronger than essential undecidability. A natural question is: are there minimal EI theories with respect to interpretation? We negatively answer this question and prove that there are no minimal effectively inseparable theories with respect to interpretation: for any EI theory T, we can effectively find a theory which is EI and strictly weaker than T with respect to interpretation. We give two different proofs of it.
 Fedor Pakhomov, Juvenal Murwanashyaka and Albert Visser. There are no minimal essentially undecidable Theories. Journal of Logic and Computation, doi.org/10.1093/logcom/exad005, 2023.
- August 16, 2023
Noam Greenberg, Victoria University of Wellington
title: Borel Wadge classes, viewed effectively
Day, Downey and Westrick, and then Day and Marks, in their work on the decomposability conjecture, showed that Montalbán's "true stages" technique can be used to understand membership in Borel sets in a dynamic way. This technique originated in work by Ash, Knight, Harrington and others in computable structure theory.
I will discuss how to use true stages to obtain results such as the Hausdorff-Kuratowski theorem, and Wadge's characterisation of ambiguous Borel classes of limit level. The power of the technique though lies in the ability to perform iterated priority arguments, one of which gives a new proof of the Louveau and Saint-Raymond separation theorem. This leads to a new scheme for describing Borel Wadge classes, that in turn can be used to understanding properties such as reduction, and characterise containment of Borel Wadge classes using clopen games. Our descriptions can also be used to extend Selivanov's fine hierarchy beyond the arithmetic sets.
- August 2, 2023
Bob Lubarsky, Florida Atlantic University
title: Topological Models for Constructive Mathematics
Forcing is well known to be equivalent with Boolean-valued models. If
you generalize from Boolean to Heyting algebras, you keep the same
construction, but lose classical logic. Hence Heyting-valued models are
essentially forcing for constructive mathematics. This talk will present
some basic examples of such.
- July 26, 2023
Masaya Taniguchi, RIKEN AIP, Tokyo, Japan
title: Bridging the Gap: Combinatorial Categorical Grammars and Proof Theory
The expressive capabilities of ordinary natural language
(spoken/written) are commonly believed to lie somewhere between
context-free language (weaker) and context-sensitive language
(stronger). However, many existing grammatical theories tend to focus
on capturing only what is grammatically correct, disregarding
ungrammatical constructs. As a result, the algorithms employed by such
theories are often semi-decidable.
To address this limitation, we propose an approach by reinterpreting
Combinatorial Categorical Grammar (CCG) as a proof system for natural
deduction. Through this perspective, we have developed an efficient
proof search method for CCG including the well-known unary rule T.
This work represents a step towards bridging the divide between proof
theory and formal grammar theory, enhancing our understanding of the
generative power of natural language.
- July 19, 2023
Fedor Pakhomov, Ghent University and Steklov Mathematical Institute of Russian Academy of Sciences, Moscow
title: \Pi^1_2-CA_0 is equivalent to Minimal Bad Array Lemma
Better quasi orders are special class of well quasi orders that enjoys better
closure properties and serve as a crucial tool in study of well quasi orders.
Minimal Bad Array Lemma is the main technical tool used to prove that orders
are better quasi orders. In this talk I will discuss the reverse mathematics of
the statement. I'll present the results that Minimal Bad Array Lemma is
equivalent to \Pi^1_2-CA_0 over ATR_0 and that this equivalence couldn't be proved
over ACA_0. Based of joint works with Anton Freund, Alberto Marcone, and
- July 5, 2023
Uri Andrews (University of Wisconsin-Madison) and Meng-Che Ho (California State University)
title: Word problems of groups and the structure of Ceers
Novikov and Boone showed in the 50s that some simply presented groups can have undecidable word problem. Since then, there have been many results about the complexities of word problems of groups, and comparing these across various classes of groups. We'll present what we believe is a very natural perspective: To consider the word problems within the structure of Ceers, the computably enumerable equivalence relations. In this setting, we'll talk about some of our recent results.
- June 28, 2023
title: Varieties of rational languages and finite monoids
This talk is about a fundamental correspondence between algebra and automata
theory. We will first present the theorem of Eilenberg which shows that there
is a 1-1 correspondence between varieties of finite monoids and varieties of
regular languages. Then we will concentrate on the theorem of Reiterman which,
in a way similar to Birkhoff's theorem from universal algebra, characterises
varieties of finite monoids as those classes of finite monoids which satisfy
certain identities (profinite identities).
- June 21, 2023
Eitetsu Ken, University of Tokyo
title: A brief introduction to Proof Complexity via Ajtai's theorem
A large part of Proof Complexity, the field in which we investigate lengths of
mathematical proofs, is nowadays focusing on proof complexity of propositional
logic. An interesting thing is that the following three are closely related:
1. Propositional proof complexity, 2. Bounded arithmetics, 3. Computational
In this talk, we briefly go through the connections between these three by
discussing one of the most significant breakthroughs in the field, namely,
Ajtai's theorem: A relativised bounded arithmetic I\Delta_0(R) cannot prove the
pigeonhole principle for R.
Lastly, we take a look at some variations of Ajtai's theorem and related open
problems, including some of my recent interests (e.g. on the comparison between
the injective pigeonhole principle and the full-version of the bijective
[ slides (with notes), literature ]
- May 31, 2023
title: Isomorphism Relations on Classes of C.E. Structures
An isomorphism relation on a class of c.e. algebras can be viewed as
an equivalence relation on the natural numbers. This allows us to
compare complexities of different isomorphism relations using known
methods from computability theory. We use computable reducibility, a
common method for comparing equivalence relations. As a case study we
focus on the classes of n-generated commutative semigroups, for
different n. Our preliminary results indicate that they are all
\Delta_2^0 (in the arithmetical hierarchy) and form a strictly
increasing sequence in the hierarchy of computable reducibility.
- May 3, 2023
title: The mu-calculus' collapse and non-collapse around S5
The mu-calculus is obtained by adding (positive) fixed-point operators to modal
logic. By mixing least and greatest fixed-point operators, we generate the
mu-calculus' alternation hierarchy. Bradfield showed that, over general Kripke
frames, the alternation hierarchy is strict. On the other hand, Alberucci and
Facchini showed that, over frames of S5, every mu-formula is equivalent to a
formula without fixed-point operators. That is, the mu-calculus' alternation
hierarchy collapses to modal logic.
We show that the collapse still happens over frames quite similar to those of
S5. We also show that the alternation hierarchy is strict over bimodal S5.
- April 26, 2023
title: The proof theoretic analysis of incorrect proofs
The analysis of incorrect proofs is one of the most essential
mathematical activities. Incorrect proofs are usually considered to be
beyond logical investigations. In this lecture we present simple
proof-theoretic approaches to handle some classes of incorrect proofs.
- April 19, 2023
title: Decidability of Diophantine equations in a theory adjacent to IOpen
Hilbert's 10th problem is the question whether there is an algorithm which,
given a polynomial with integer coefficients, determines whether it has integer
roots. It has been shown that no such algorithm exists as a consequence of the
MRDP theorem. In other words: Diophantine satisfiability is undecidable for
arithmetic. One can now ask whether the problem of Diophantine satisfiability
is decidable for weaker theories of arithmetic.
In this thesis we present a novel proof-theoretic approach for deciding
Diophantine satisfiability problems. We work in a base arithmetical theory A
in the language with successors, predecessors, addition and multiplication and
use a result by Shepherdson to extract a subtheory AB which is one axiom schema
short of the theory of open induction over A. We show that Diophantine
satisfiability in AB is decidable.
- March 29, 2023
Luca San Mauro
title: Investigating the computable Friedman-Stanley jump
The Friedman-Stanley jump, extensively studied by descriptive set
theorists, is a fundamental tool for gauging the complexity of Borel
isomorphism relations. In this talk, the paper focuses on a natural
computable analog of this jump operator, recently introduced by
Clemens, Coskey, and Krakoff in the setting of computable reducibility
of equivalence relations on the natural numbers. We show that the
computable Friedman-Stanley jump gives benchmark equivalence relations
going up the hyperarithmetic hierarchy and we unveil the intricate
highness hierarchy that arises from it. This is joint work with Uri
- March 22, 2023
- Johannes Weiser
title: Star height of regular languages
Regular languages can be described using both automata and regular expressions.
The star height of a regular expression is the maximal number of nested stars
of that expression. In this talk, I will present two major theorems regarding
the star height of regular languages: The star height corresponds to the loop
complexity of an automaton. Moreover, it is possible to find languages of
arbitrary star height. The corresponding problem for regular expressions with
complement is still open.
- March 15, 2023
- Stefan Hetzl
title: Quantifier-free induction on lists
We investigate quantifier-free induction for Lisp-like lists constructed
inductively from the empty list nil and the operation cons, that adds an
element to the front of a list. First we show that open m-step induction does
not simulate open (m + 1)-step induction. Secondly, we show that open big-step
induction does not prove the right cancellation property of the concatenation
operation on lists. These results are relevant for automated inductive theorem
This is joint work with Jannik Vierling.
Last Change: 2023-12-01, Stefan Hetzl