Nordic Online Logic Seminar
An online seminar for logicians and logic aficionados worldwide.
The Nordic Online Logic Seminar (NOL Seminar) is a monthly seminar series initiated in 2021 presenting expository talks by logicians on topics of interest for the broader logic community. Initially the series focused on activities of the Nordic logic groups, but has since expanded to offer a variety of talks from logicians around the world. The seminar is open to professional or aspiring logicians and logic aficionados worldwide.
The tentative time slot is Monday, 16.00–17.30 (Stockholm/Sweden time). If you wish to receive the Zoom ID and password for it, as well as regular announcements, please subscribe to the NOL Seminar mailing list.
NOL seminar organisers
Valentin Goranko and Graham Leigh
-
-
-
Propositional dynamic logic (PDL) is a well-known modal logic which originates from the wave of so-called process logics that emerged in the 1970s. Characteristic to PDL is that its collection of modalities is given as the set of regular expressions over some set of atomic programs and (possibly) so-called test program. The main results on PDL, such as a sound and complete axiomatisation and the decidability and computational complexity of its satisfiability problem, were obtained relatively soon after its introducton. In the talk I will review some results on PDL that have been discovered (or re-discovered) in more recent years. Topics to be discussed include the relation of PDL with other fixpoint logics, expressive completeness results and cut-free proof systems. The main issue that I want to address concerns the Craig interpolation property for PDL, a long-standing problem that can finally be settled. I will finish with mentioning some open problems.
The talk is based on work with and by many co-authors.
-
Sun Tzu was a military strategist who lived in China about 2500 years ago. His book is still popular today, especially in business circles.
This talk presents a study of “The Art of War” from the perspectives of logic, mathematics, and computer science. We explain briefly what a mind map is and our strict text tree interpretation of it, for the purpose of analyzing Sun Tzu’s text. We show that you can improve the translation and find more meaning in the text, representing the text as mind maps. If time permits, we will illustrate that, surprisingly, the text still helps us to understand what is happening in warfare today.
The title of this talk is also the title of our book, co-authored by Kaibo Xie (Tsinghua Univ. Beijing), and Bonan Zhao (Univ. of Edinburgh), and published in 2022 by Springer. The book is the result of a joint study of the Institute of Language, Logic and Computation, Univ. of Amsterdam and the Institute for Philosophy, Tsinghua University, Beijing, China.
-
What is the meaning of a logical connective? This is a very difficult and controversial question, primarily because its answer depends on the underlying logical framework. In model-theoretic semantics, the meaning of logical connectives is grounded in mathematical structures that define validity in terms of truth. Proof-theoretic semantics (PtS), by contrast, offers an alternative perspective in which truth is replaced by proof. This shift highlights the role of proofs as the foundation for demonstrative knowledge, particularly in mathematical reasoning. Philosophically, PtS aligns with inferentialism, which holds that the meaning of expressions is determined by inference rules. This makes PtS particularly well-suited for understanding reasoning, as it defines logical connectives based on their role in inference.
Base-extension semantics (BeS) is a strand of PtS where proof-theoretic validity is defined relative to a given collection of inference rules regarding basic formulas of the language. Although the BeS project has been successfully developed for intuitionistic propositional logic, first-order classical logic and the multiplicative fragment of linear logic among others, its progression as a comprehensive foundation for logical reasoning is still in its early stages.
In this talk, we will explore Pt-S with a focus on BeS. First, we will introduce an ecumenical perspective to BeS, inspired by Prawitz’s proposal of a system combining classical and intuitionistic logics. The aim is to deepen our understanding of logical reasoning disagreements by investigating the ecumenical approach and developing a unified proof-theoretic foundation for logical reasoning.
We will then address a major challenge in PtS, often called its “original sin”, which is its strong reliance on the natural deduction framework. To overcome this, we propose a version of BeS that employs atomic systems based on sequent calculus rules rather than natural deduction. In this approach, structural rules are treated as properties of atomic systems rather than the logical calculus itself. This allows for a semantics of substructural logics to emerge naturally by modifying the underlying atomic systems. Furthermore, this framework supports a Sandqvist-style completeness proof, but instead of extracting a proof in natural deduction, we obtain one in sequent calculus.
This is based is an ongoing and joint work with Victor Barroso-Nascimento, Luiz Carlos Pereira and Katya Piotrovskaya.
-
Team semantics extends traditional semantics by shifting the interpretation of formulas from individual semantic objects (e.g., assignments, valuations, or worlds) to sets of such objects, commonly referred to as teams. This approach enables the expression of properties, such as variable dependency, that are inaccessible in traditional semantics. Since its introduction by Hodges and subsequent refinement by Väänänen, team semantics has been used to develop expressively enriched logics that retain desirable properties such as compactness.
However, these logics are typically non-substitutional, limiting their algebraic treatment and preventing the development of schematic proof systems. This limitation can be attributed to the flatness principle which is commonly adhered to in many constructions of team semantics for logics.
In this talk, we approach the formation of propositional logic of teams from an algebraic perspective, explicitly discarding the flatness principle. We propose a substitutional logic of teams that is expressive enough to axiomatize key propositional team logics, such as propositional dependence logic.
Our construction parallels the algebraic construction of classical propositional logic from Boolean algebras. The algebras we are using are powersets of Boolean algebras equipped with both internal (pointwise) and external (set-theoretic) operations. The resulting logic is clearly substitutional, and is shown to be sound and complete with respect to a labelled natural deduction system.
If time permits, we will also discuss how we might do to extend this construction to the framework of first-order logic.
-
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.
- P.A.M. Dirac. The principles of Quantum Mechanics, 3rd ed, Clarendon Press, Oxford, 1947.
- Å. Hirvonen, T. Hyttinen, On eigenvectors, approximations and the Feynman propagator, Ann. Pure Appl. Logic 170 (2019).
- Å. Hirvonen, T. Hyttinen, On Ultraproducts, the Spectral Theorem and Rigged Hilbert Spaces, to appear in J. Symb. Log.
- 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.