Seminars
Seminars, workshops and other events organised by our group
The Logic Group runs a bi-weekly Research Seminar in Logic, monthly Nordic Online Logic Seminar and the annual Lindström Lecture series, as well as other events. See below for a list of recent and upcoming events or follow the links to jump straight to a category.
The research seminar in Logic meets on alternate Fridays at 10.15. Unless otherwise stated, seminars are held at the department building (Humanisten). Details of online talks are distributed in the GU Logic mailing list. Alternatively, contact Graham E Leigh directly.
-
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.
-
We investigate the cyclic proof theory of extensions of Peano Arithmetic, in particular µPA, a theory that extends Peano Arithmetic with least and greatest fixed point operators. Our cyclic system CµPA subsumes Simpson’s cyclic arithmetic and the stronger CID<ω. Our main result, which is still work in progress, is that the inductive system µPA and the cyclic system CµPA prove the same arithmetical theorems. We intend to conduct a metamathematical argument for Cyclic Arithmetic to formalize the soundness of cyclic proofs within second-order arithmetic by a form of induction on closure ordinals and then appealing to conservativity results. Since the closure ordinals of our inductive definitions far exceed the recursive ordinals we cannot rely on ordinal notations and must instead formalize a theory of ordinals within second-order arithmetic. This is similar to what is for CID<ω except here we also need to use the reverse mathematics of a more powerful version of Knaster-Tarski.
-
The Logic Group at the University of Gothenburg hosts its annual World Logic Day Pub Quiz. For information on World Logic Day events around the world, see http://wld.cipsh.international/wld2025.html.
-
Fagin’s seminal result characterizing NP in terms of existential second-order logic started the fruitful field of descriptive complexity theory. In recent years, there has been much interest in the investigation of quantitative (weighted) models of computations. In this paper, we start the study of descriptive complexity based on weighted Turing machines over arbitrary semirings. We provide machine-independent characterizations (over ordered structures) of the weighted complexity classes NP[S], FP[S], FPLOG[S], FPSPACE[S], and FPSPACEpoly[S] in terms of definability in suitable weighted logics for an arbitrary semiring S. In particular, we prove weighted versions of Fagin’s theorem (even for arbitrary structures, not necessarily ordered, provided that the semiring is idempotent and commutative), the Immerman–Vardi’s theorem (originally for P) and the Abiteboul–Vianu–Vardi’s theorem (originally for PSPACE). We also discuss a recent open problem proposed by Eiter and Kiesel.
Recently, the above mentioned weighted complexity classes have been investigated in connection to classical counting complexity classes. Furthermore, several classical counting complexity classes have been characterized in terms of particular weighted logics over the semiring N of natural numbers. In this work, we cover several of these classes and obtain new results for others such as NPMV, ⊕P, or the collection of real-valued languages realized by nondeterministic polynomial-time real-valued Turing machines. Furthermore, our results apply to classes based on many other important semirings, such as the max-plus and the min-plus semirings over the natural numbers which correspond to the classical classes MaxP[O(log n)] and MinP[O(log n)], respectively.
-
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).
-
Disquotational truth can play a justificatory role for new mathematical knowledge. In particular, we focus on the known case of consistently extending a theory of first-order arithmetic (PA) with a truth predicate governed by disquotational principles for positive sentences. One philosophically interesting feature is that the addition of this truth predicate is conservative over the arithmetical theory, giving disquotational truth the same epistemic status of a mathematical definition. Following Feferman and McGee, we argue in favour of the open-ended nature of the induction schema: once a new mathematical concept is legitimately defined the schema should hold for the extended language. For truth, this results in more justificatory power as one can prove the consistency statement of the arithmetical theory. Moreover, the exact nature of the justificatory power of positive disquotational truth can be pinned down via an ordinal analysis of the theory, as done by Halbach.
We explore the possibility of extending this disquotational definition of truth via a principle of Generalised Induction introduced by Cantini. The principle is conservative over PA, meaning it preserves the epistemic status of a definition. Furthermore, we argue that the adoption of this principle is particularly motivated in the case of positive disquotational truth. Once this new truth predicate is allowed in the induction schema, we obtain significantly more justificatory power than the original disquotational theory. I conclude by sketching a possible strategy via a collapsing procedure to show that this result is sharp.
-
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.
-
Previous works by Goré, Postniece and Tiu have provided sound and cut-free complete proof systems for modal logics extended with path axioms using the formalism of nested sequent. Our aim is to provide (i) a constructive cut-elimination procedure and (ii) alternative modular formulations for these systems. We present our methodology to achieve these two goals on a subclass of path axioms, namely quasi-transitivity axioms.
-
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.
-
This dissertation concerns the properties of and relationship between positive truth and fixpoints over intuitionistic arithmetic in three respects: the strength of these theories relative to the arithmetic base theories, relationships between theories of strictly positive fixpoints and compositional and disquotational truth for strictly truth-positive sentences, and a comparison with the classical case.
Opponent: Gerhard Jäger, Professor Emiratus University of Bern