Nordic Online Logic Seminar

Several areas of computer science (databases, knowledge representation, program verification, reasoning about knowledge and actions) feature logical languages in which one can construct complex binary relations from basic ones, through a certain set of operations (e.g., relational composition, union, inverse, …). Examples include propositional dynamic logics such as PDL and KAT (Kleene Algebra with Tests) as well as various query languages for graph databases. Underlying each of these is a “binary relation algebra” , i.e., an algebraic signature consisting of finitely many operations on binary relations. The specific set of operators, in each of the aforementioned languages, is typically chosen as a compromise between computational complexity and expressive power and/or may be based on a requirement to preserve certain natural structural properties such as functionality or bisimulation.

Preservation theorems link semantics properties of formulas to their syntactic shape. The most famous example is the Łoś-Tarski theorem, which states that a first-order formula is preserved under induced substructures (i.e., remains true if one passes from a structure to an induced substructure) if and only if it can be written without using any existential quantifiers (assuming negation normal form). In this talk, we will review some recent results (both positive and negative) about the existence of preservation theorems for algebras of binary relations. (Algebraically, the results I will present can be equivalently viewed as addressing the question whether certain clones admit a finite set of generators).

Specifically, I will discuss results about Tarski’s relation algebra from a joint paper with Bart Bogaerts, Brett McLean, and Jan van den Bussche (LMCS 2024) as well as results about Kleene Algebra with Tests (KAT) from a joint paper with Tobias Kappé (POPL 2025).

Non-classical logics have been proposed in a number of domains, including constructive mathematics and quantum mechanics. In this talk, I will identify a base logic beneath some of these non-classical logics that I suggest has a certain fundamental status. I will give an introduction to the proof theory and semantics of this “Fundamental Logic.”

An associated paper is available at https://arxiv.org/abs/2207.06993.

The axioms of quantum mechanics present the state of a quantum system as a unit vector in complex Hilbert space. However, when Dirac [1] presented his bra- and ket-vectors, he had a more general space in mind. Schwartz [4] later gave a rigorous account for Dirac’s “vectors” as distributions, but in elementary physics books one still encounters presentations where ket-vectors are presented just as elements of a Hilbert space, and treated with methods from finite-dimensional linear algebra.

During the last years Tapani Hyttinen and I [2,3] have been looking at various models justifying the finite dimensional approaches from such textbooks. Our approaches are based on various embeddings of a Hilbert space into metric ultraproducts of finite-dimensional Hilbert spaces. In this talk I will present the basic ideas, their benefits and limitations. Time permitting, I will also contrast our approach to Boris Zilber’s work on the same questions, that was the original inspiration for us.

1. P.A.M. Dirac. The principles of Quantum Mechanics, 3rd ed, Clarendon Press, Oxford, 1947.
2. Å. Hirvonen, T. Hyttinen, On eigenvectors, approximations and the Feynman propagator, Ann. Pure Appl. Logic 170 (2019).
3. Å. Hirvonen, T. Hyttinen, On Ultraproducts, the Spectral Theorem and Rigged Hilbert Spaces, to appear in J. Symb. Log.
4. L. Schwartz, Théory de Distributions, Hermann, Paris, 1950.

Natural languages vary in their quantity expressions, but the variation seems to be constrained by general properties, so-called universals. Explanations thereof have been sought among constraints of human cognition, communication, complexity, and pragmatics. In this work, we examine whether perceptual constraints and coordination dynamics contribute to the development of two universals: monotonicity and convexity. Using a state-of-the-art multi-agent language coordination model (originally applied to colour terms) we evolve communicatively usable quantity terminologies. We compare the degrees of convexity and monotonicity of languages evolving in populations of agents with and without approximate number sense (ANS). The results suggest that ANS supports the development of monotonicity and, to a lesser extent, convexity. We relate our results to some classical observations about generalised quantifiers in mathematical logic and to the research on conceptual spaces.

This is joint work with Dariusz Kalociński, Franek Rakowski and Jakub Uszyński.

Voting on two alternatives appears unproblematic compared to voting on three (or more). When faced with only two alternatives, many arguments show that Majority Rule distinguishes itself from all other ways of making a group decision. For three or more alternatives, one faces the so-called “Paradox of Voting”: there may be elections with a majority cycle in which a majority of voters prefer A to B, a majority of voters prefer B to C, and a majority of voters prefer C to A. In this talk, I will explain a series of results that axiomatically characterize rules for resolving majority cycles in elections. These rules avoid the “Strong No Show Paradox” by responding properly to the addition of new voters to an election and mitigate spoiler effects by responding properly to the addition of new candidates to an election.

This talk is based on joint work with Wes Holliday.

Inquisitive modal logic is a generalization of standard modal logic where the language also contains questions, and modal operators that can be applied to them. In this talk, I will provide an introductory overview of inquisitive modal logic. I will review some motivations for the approach, present some prominent examples of inquisitive modal logics, mention some results about them, and outline directions for future work.

Sequential theories form a fundamental class of theories in logic. They have full coding possibilities and allow us to build partial satisfaction predicates for formulas of bounded depth-of-quantifier-alernations. In many respects, they are the proper domain of Gödelian metamathematics. We explain the notion of sequential theory.

A theory is restricted if it can be axiomatised by axioms of bounded depth-of-quantifier-alernations. All finitely axiomatised theories are restriced, but, for example, also Primitive Recursive Arithmetic. We explain the small-is-very-small principle for restricted sequential theories which says that, whenever the given theory shows that a definable property has a small witness, i.e., a witness in a sufficiently small definable cut, then it shows that the property has a very small witness, i.e., a witness below a given standard number.

We sketch two proofs that restricted theories are incomplete (however complex the axiom set). One uses the small-is-very-small principle and the other a direct Rosser argument. (The second argument was developed in collaboration with Ali Enayat.)

A game that characterizes definability of classes of structures by first-order sentences containing a given number of quantifiers was introduced by Immerman in 1981. In this talk I describe two other games that are equivalent with the Immerman game in the sense that they characterize definability by a given number of quantifiers.

In the Immerman game, Duplicator has a canonical optimal strategy, and hence Duplicator can be completely removed from the game by replacing her moves with default moves given by this optimal strategy. On the other hand, in the other two games there is no such optimal strategy for Duplicator. Thus, the Immerman game can be regarded as a one-player game, but the other two games are genuine two-player games.

The talk is based on joint work with Kerkko Luosto.