Talks of the fall term 2023

Wed 13.9.2023 12-14, C124 + zoom

Aleksi Anttila: Deep inference sequent calculi for propositional logics with team semantics

Abstract: (Joint work with Rosalie Iemhoff and Fan Yang.) While natural deduction- and Hilbert-style axiomatizations of logics employing team semantics such dependence logic and inquisitive logic have been extensively studied, the development of sequent calculi and proof theory in general for these logics appears to have been hindered by the factors such as the fact these logics are not closed under uniform substitution. The sequent calculi which have been constructed for these logics thus far have been labelled or multi-type systems. We propose a different approach: by appending a few deep inference-style rules (rules which can act not only on the immediate subformulas and main connectives of formulas, but also on subformulas and connectives deeper within a formula) to a standard Gentzen-style calculus, we obtain a very simple system for at least one of these logics.

Wed 20.9.2023 12-14, C124 

Ur Ya'ar:  Iterating the stationary-logic constructible universe

Abstract: One way of generalizing Goedel's constructible universe L, is to replace the notion of definability used at successor stages, and take all subsets of the last stage which are definable using a logic L* extending first order logic. This will result in a model of ZF, denoted C(L*). In some cases it will also be a model of AC. As in the case of L, we can formulate the axiom "V=C(L*)", but unlike L, it is not always true that C(L*) |= "V=C(L*)", that is, when we construct C(L*) inside C(L*) we might get a smaller model. If that is the case, we can iterate this construction, continuing transfinitely with intersections at limit stages, until we stabilize.

We will focus on the case where L* is stationary logic, and show, as time permits, that by certain kinds of club-shooting forcing we can get models where the iterated construction is arbitrarily long.

Wed 27.9.2023 12-14, C124

Fan Yang: Generalizing propositional team semantics

Abstract: In this talk, we discuss a generalization of the standard team semantics in the propositional logic context. Team semantics was introduced by Hodges (1997) and later advanced by Väänänen (2007) in dependence logic for characterising dependency notions. The key idea of team semantics is that dependency properties can only make sense in multitudes. A formula in team semantics based logics is thus evaluated on a set of assignments or possible worlds (called teams). 

In the propositional context, team semantics is defined essentially over an underlying powerset (Kripke) frame of the teams, which also forms a bounded join-semilattice. Several authors ((Puncochar 2016 & 2017),(Holliday 2020),(Dmitrieva 2021),(Bezhanishvili & Yang 2022)) have recently defined different generalizations of the standard team semantics by modifying this powerset structure from different perspectives. In this talk, we introduce a new definition of team semantics that tries to combine these existing approaches and also preserve the key original idea of Hodges (1997). We define a team (Kripke) frame simply as an arbitrary bounded join-semilattice. The semantics for connectives and constants are generalized in a natural manner. The dependence atoms in this generalized setting still satisfy Armstrong’s Axioms of functional dependencies.

Wed 4.10.2023 12-14, C124

Melissa Antonelli: Towards a New Characterization of Parallel Complexity Classes (joint work with Arnaud Durand and Juha Kontinen).

Abstract: Implicit computational complexity is an active area of theoretical computer science, aiming to provide machine-independent characterisations of relevant complexity classes. One of the seminal works in this field appeared in 1964, when Cobham introduced a function algebra closed under bounded recursion on notation and able to capture FP, the class of functions computable in polynomial time. Since then, several complexity classes have been characterised using limited recursion schemes.

Recently, an elegant algebra has been introduced by Bournez and Durand, who in 2019 showed that ordinary differential equations (ODEs) offer a natural tool for algorithmic design and characterised FP via a special ODE schema. The overall goal of our study is precisely that of generalising this approach to parallel computation and of providing (possibly uniform) ODE-style characterisations for small circuit classes. In particular, in this talk I will present the global aim and methodology at the basis of our in progress research and sketch the (very first) results we have achieved so far.

Wed 11.10.2023 12-14, C124 

Davide Quadrellaro: Strictly n-finite varieties of Heyting algebras

Abstract. For any n < ω we construct an infinite (n+1)-generated Heyting algebra whose n-generated subalgebras are of cardinality ≤ m for some positive integer m. From this we conclude that for every n < ω there exists a variety of Heyting algebras which contains an infinite (n + 1)-generated algebra, but which contains only finite n-generated algebras. For the case n = 2 this provides a negative answer to a question posed by G. Bezhanishvili and R. Grigolia. This is a joint work with Tapani Hyttinen.

Wed 18.10.2023 12-14, C124 + zoom

Aleksi Anttila: Convexity in propositional team semantics

Abstract: (Joint work with Søren Knudstorp) The expressive power of logics employing team semantics can often be characterized in a concise and intelligible way using team-semantic closure properties such as downward closure or union closure. In this talk we examine the property of convexity: a formula is convex if truth in a team T and truth in a team S implies truth in all teams between T and S with respect to set inclusion. Convexity allows us to answer an open question concerning one of the simplest propositional logics which breaks downward closure, the extension of classical propositional logic with a non-emptiness atom NE: due to a result by Søren Knudstorp, this logic is expressively complete with respect to the class of team properties which are both union closed and convex. We introduce another logic to capture the class of all convex propositional team properties.

Wed 25.10.2023 12-14, Exam week (no seminar)

Wed 1.11.2023 12-14, C124

Johannes Schmidt: On propositional logic

Abstract: In this talk I outline how to consider systematically fragments of propositional logic, what we can do with these tools and what we can learn about the computational complexity of various problems. I will present some of the existing work in this context, and what interesting things remain to be explored.

Wed 8.11.2023 12-14, C124

Matilda Häggblom: Axiomatizing some implication problems for approximate dependence atoms.

Abstract: Väänänen (2017) introduced and axiomatized the approximate dependence atom: a team satisfies an approximate dependence atom if it has a subteam (of a certain size) that satisfies the usual dependence. This idea is suited for applications when "almost dependence" is enough.

We introduce and axiomatize approximate exclusion atoms. Motivated by exclusion and dependence atoms both being downwards closed, we use the same definition of approximation also for approximate exclusion: allowing a certain amount of lines to be removed from the team. We then prove the completeness theorem by building a counterexample team.

We also introduce approximate anonymity and axiomatize unary consequences for approximate anonymity atoms. Anonymity atoms are not downwards closed, but union closed, and our definition of approximation is slightly different due to using restricted teams. Interestingly, in this setting, allowing lines to be added or removed from the team yields two equivalent definitions of approximation. We again build a counterexample team to prove completeness.

Wed 15.11.2023 12-14, C124

Tuomo Lehtonen: On the complexity of argument construction in formal argumentation

Abstract: Formal argumentation is an approach to defeasible reasoning with intuitive dialectical semantics. For example, various forms of non-monotonic reasoning, such as default logic, autoepistemic logic and logic programming, have been given argumentative interpretations. In this talk, I give an introduction to assumption-based argumentation (ABA), an approach where deductive rules derive arguments for new facts from defeasibly true assumptions, and discuss some argument construction procedures for ABA. In particular, I note that the straightforward, conventional procedure unnecessarily introduces an exponential number of arguments. I present recent work (joint with Anna Rapberger, Markus Ulbricht and Johannes P. Wallner) showing a polynomially bounded argument construction procedure for ABA.

Wed 22.11.2023 12-14, C124

Reijo Jaakkola: This talk will consist of two parts. In the first part I will present results from [1] where we investigated the so-called special explainability problem for propositional logic. In this problem the goal is to find a short explanation for why a given truth assignment was accepted/rejected by a formula of propositional logic. I will present our result from [1] on the computational complexity of this problem. I will also mention some new results on the complexity of this problem for syntactically more restricted families of Boolean classifiers.

In the second part I will present results from [2] where we used short formulas of propositional logic as classifiers for explaining data. Short Boolean formulas have the advantage of being immediately interpretable, which makes them ideal for knowledge discovery applications. The shortness constraint is also useful for avoiding overfitting. I will present empirical results from [2], which demonstrate both the feasibility of our approach and the surprisingly good accuracy of very short Boolean formulas on real-world data sets.

 This talk is based on joint work with Tomi Janhunen, Antti Kuusisto, Masood Feyzbakhsh Rankooh and Miikka Vilander.

 [1] Explainability via Short Formulas: the Case of Propositional Logic with Implementation, RCRA 2022

[2] Short Boolean Formulas as Explanations in Practice, JELIA 2023

Wed 29.11.2023 13-14, C124

Samson Abramsky: Relating Structure to Power: an emerging landscape

Abstract: A survey of recent work on game comonads, and connections between (finite) model theory and categorical semantics.

Tue 5.12.2023, 12-14, C124

Joni Puljujärvi: Model theory of team semantics

Abstract: We discuss ongoing joint work with Tapani Hyttinen and Davide Quadrellaro on (elementary) model theory of second-order objects (that is, teams).

Wed 13.12.2023 12-14, C124

Remi Jaoui: On Liouville’s theory of elementary functions

Abstract: An elementary function is a function of one complex variable which is the composition of a finite number of arithmetic operations, exponentials, logarithms, constants and solutions of algebraic equations. Given a differential equation (E), the problem of integration in finite terms asks if one can write down explicitly the solutions of the differential equation (E) as elementary functions.

I will describe some recent progress on this problem obtained using model-theoretic techniques and the interplay between the theory of differentially closed fields of characteristic zero and Kirby’s blurred exponential.

This is joint work with Jonathan Kirby.

Wed 20.12.2023 12-14, Exam week (no seminar)