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
"Dissertantenraum" in Freihaus, 8th floor, green area.
The seminar is
organised by E. Fokina and
S. Hetzl.
If you want to receive talk announcements by email, please subscribe to the
mailing list of this seminar on its
administration page.
Preliminary Programme
 May 8, 2024

Martin Ritter
 May 22, 2024

Alexander Leitsch
 June 5, 2024

Vittorio Cipriani
 June 19, 2024

Johanne Müller Vistisen
 t.b.d.

Dino Rossegger
Archive
 April 10, 2024

Fabian Wöhrer
title: Reversible Automata: Characterizations and Construction
abstract:
A finite automaton is called reversible, if every letter induces a partial injective map from the set of states into itself. We will characterize the corresponding class of reversible languages from a grouptheoretic, algebraic and topological perspective.
Afterwards we solve the membership problem algorithmically and present a procedure that transforms the minimal DFA of a reversible language into an equivalent reversible automaton.
 March 20, 2024

Florian Grünstäudl
title: Beth's Definability Theorem and the Complexity of Explicit Definitions
abstract:
We will briefly discuss the proof of Beth's Definability Theorem for first order logic.
The main part of the presentation will be dedicated to Friedman's proof of the fact that the
quantifier complexity of the explicit definitions obtained by Beth's Theorem is not computable.
 March 13, 2024

Johannes Weiser
title: Complexity Bounds for CutElimination
abstract:
It is wellknown that cutelimination in firstorder logic is nonelementary.
In this work we analyse the height of the tower of exponentials for bounds
related to cutelimination.
We take up a suggestion by S. Buss that it should be possible to obtain an
upper bound on the length of the cutfree proof in terms of d+1 iterations of
the exponential function where d is the number of quantifer alternations in the
cut formulas of the original proof. We show this result by combining Buss' work
with a result by Weller on the elimination of quantifierfree cuts.
 December 20, 2023

Clara Pichler
title: The Tutte Polynomial
abstract:
Matroids provide a notion of independence that generalises concepts from linear
algebra, graph theory and other subjects.
This presentation will concentrate on the connection between the Tutte
polynomial, a bivariate polynomial defined on matroids, and the chromatic
polynomial, a univariate polynomial defined on graphs. It also provides an
introduction to matroids and their association to graphs, so that prior
knowledge in matroid theory is not necessary.
 November 29, 2023

Juan Aguilera
title: The compactness number of Gödel logic
abstract:
We give a proof of the theorem that the compactness number of firstorder Gödel logic with identity is the least \omega_1strongly compact cardinal.
 November 22, 2023

Thibaut Kouptchinsky
title: Reverse Mathematics: Limits of Determinacy Axioms in SecondOrder Arithmetic and Beyond
abstract:
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
abstract:
We study the reverse mathematical strength of the 4colour theorem and various related principles. We show that the 4 colour theorem effectively reverses to WKL0, but the 8colour theorem reverses, but not effectively. We also study the relationship between the kcolour theorem for all values of k.
 Tuesday, October 10, 2023, 10:00am, Besprechungsraum

Dino Rossegger
title: Learning equivalence relations
abstract:
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 coanalytic complete in the codes and rediscover longstanding open questions about Borel equivalence relations.
 September 27, 2023

Vittorio Cipriani
title: How to learn families of algebraic structures
abstract:
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 Elearnability. 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

Giovanni Soldà
title: A combinatorial principle weak over weak systems yet strong over
strong systems
abstract:
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 NashWilliams'
theorem and Laver's theorem. From the reverse mathematical point of
view, the study of bqos is an interesting area still full of open
questions.
In this talk, we will focus on a property of nonbqos, the socalled
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 reversemathematical 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
quasiorders that ACA 0 proves to be bqos.
This is joint work with Anton Freund, Alberto Marcone, and Fedor
Pakhomov.
 September 20, 2023, 10:00, Dissertantenraum
 Alexandra BergmayrMann
title: Gleason's Theorem
abstract:
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 noncontextual 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
abstract:
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 [1] 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.
[1] 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
abstract:
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 HausdorffKuratowski 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 SaintRaymond 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
abstract:
Forcing is well known to be equivalent with Booleanvalued models. If
you generalize from Boolean to Heyting algebras, you keep the same
construction, but lose classical logic. Hence Heytingvalued 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
abstract:
The expressive capabilities of ordinary natural language
(spoken/written) are commonly believed to lie somewhere between
contextfree language (weaker) and contextsensitive 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 semidecidable.
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 wellknown 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_2CA_0 is equivalent to Minimal Bad Array Lemma
abstract:
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_2CA_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
Giovanni SoldÃ .
 July 5, 2023

Uri Andrews (University of WisconsinMadison) and MengChe Ho (California State University)
title: Word problems of groups and the structure of Ceers
abstract:
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

Johannes Weiser
title: Varieties of rational languages and finite monoids
abstract:
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 11 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
abstract:
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
complexity.
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 fullversion of the bijective
pigeonhole principle).
[ slides (with notes), literature ]
 May 31, 2023

Martin Ritter
title: Isomorphism Relations on Classes of C.E. Structures
abstract:
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 ngenerated 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

Leonardo Pacheco
title: The mucalculus' collapse and noncollapse around S5
abstract:
The mucalculus is obtained by adding (positive) fixedpoint operators to modal
logic. By mixing least and greatest fixedpoint operators, we generate the
mucalculus' 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 muformula is equivalent to a
formula without fixedpoint operators. That is, the mucalculus' 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

Matthias Baaz
title: The proof theoretic analysis of incorrect proofs
abstract:
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
prooftheoretic approaches to handle some classes of incorrect proofs.
 April 19, 2023

Fabian Achammer
title: Decidability of Diophantine equations in a theory adjacent to IOpen
abstract:
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 prooftheoretic 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 FriedmanStanley jump
abstract:
The FriedmanStanley 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 FriedmanStanley 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
Andrews.
 March 22, 2023
 Johannes Weiser
title: Star height of regular languages
abstract:
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: Quantifierfree induction on lists
abstract:
We investigate quantifierfree induction for Lisplike 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 mstep induction does
not simulate open (m + 1)step induction. Secondly, we show that open bigstep
induction does not prove the right cancellation property of the concatenation
operation on lists. These results are relevant for automated inductive theorem
proving.
This is joint work with Jannik Vierling.
Last Change: 20240417, Stefan Hetzl