Computational Logic Seminar

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 e-mail, 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 group-theoretic, 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 Cut-Elimination
abstract:
It is well-known that cut-elimination in first-order logic is non-elementary. In this work we analyse the height of the tower of exponentials for bounds related to cut-elimination.
We take up a suggestion by S. Buss that it should be possible to obtain an upper bound on the length of the cut-free 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 quantifier-free 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 first-order Gödel logic with identity is the least \omega_1-strongly compact cardinal.
November 22, 2023
Thibaut Kouptchinsky
title: Reverse Mathematics: Limits of Determinacy Axioms in Second-Order 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 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
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 co-analytic 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 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
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 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 questions. 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 Pakhomov.
September 20, 2023, 10:00, Dissertantenraum
Alexandra Bergmayr-Mann
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 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
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 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
abstract:
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
abstract:
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
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_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 Giovanni Soldà.
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
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 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
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 full-version 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 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
Leonardo Pacheco
title: The mu-calculus' collapse and non-collapse around S5
abstract:
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
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 proof-theoretic 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 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
abstract:
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 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: Quantifier-free induction on lists
abstract:
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 proving.
This is joint work with Jannik Vierling.

Last Change: 2024-04-17, Stefan Hetzl