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.
-
-
-
-
-
The Logic Group at the University of Gothenburg hosts its annual World Logic Day Pub Quiz. For more information on this other World Logic Day events around the world, see http://wld.cipsh.international/wld2026.html.
-
Codd’s Theorem, a fundamental result of database theory, asserts that relational algebra and relational calculus have the same expressive power on relational databases. We explore Codd’s Theorem for databases over semirings and establish two different versions of this result for such databases: the first version involves the five basic operations of relational algebra, while in the second version the division operation is added to the five basic operations of relational algebra. In both versions, the difference operation of relations is given semantics using semirings with monus, while on the side of relational calculus a limited form of negation is used. The reason for considering these two different versions of Codd’s theorem is that, unlike the case of ordinary relational databases, the division operation need not be expressible in terms of the five basic operations of relational algebra for databases over an arbitrary positive semiring; in fact, we show that this inexpressibility result holds even for bag databases.
-
Databases are typically assumed to have definite content so that users can pose queries and retrieve unambiguous answers. It is often the case, however, that a database may contain information that is incomplete, inconsistent, or uncertain. Possible world semantics provides meaning to logic-based queries on databases suffering from these deficiencies. Such databases are viewed as compact representations of all their possible rectifications; by definition, the certain answers are the query answers that hold true in every possible rectification of a deficient database.
The goal of this lecture is to provide an overview of some of the work on certain answers as a unifying framework for coping with incompleteness, inconsistency, and uncertainty in databases. Case studies include inconsistent databases, probabilistic databases, and election databases in social choice theory.
-
Opponent: Reuben Rowe, Senior Lecturer in Computer Science, Royal Holloway
Abstract Cyclic proofs are graphs, rather than trees, requiring additional soundness conditions to distinguish proofs from mere derivations. Using an abstract notion of cyclic proof system (CPS), this dissertation presents uniform results about different methods of representing the same CPS.
We prove that every traditional CPS can be represented as two other types of CPS: Reset proofs, which ‘localise’ soundness using a mechanism of sequent annotations, and stack-controlled proofs, introduced in this thesis, which align the cyclic and inductive structure of proofs.
Using stack-controlled proofs, we obtain multiple further results: a new translation from cyclic to ‘plain’ Heyting arithmetic; a correspondence between fragments of cyclic Peano arithmetic and the inductive fragments \(\mathrm{I}\Pi_n\); a proof-theoretic consistency argument for and ordinal annotation of cyclic Peano arithmetic; a general soundness argument for CPS which avoids the use of classical principles.
Reset proofs are employed to give a constructive analysis of the most common soundness condition for CPS. The condition is equivalent to the additive Ramsey theorem, the combination of two novel principles and, under unique choice, the LPO. The soundness condition can be constructivised by restricting it to periodic paths.
Examination committee
- Professor Thomas Studer, University of Bern
- Professor Mernoosh Sadrzadeh, University College London
- Associate Professor Anders Mörtberg, Stockholm University
- Professor Eleni Gregoromichelaki, Göteborgs universitet (substitute)
-
Opponent: Professor Luigi Santocanale, Aix Marseille Université
A prepatory seminar on a draft of Giacomo’s doctoral thesis.
-
-
The combination of Löwenheim-Skolem Theorem and Compactness Theorem limits the expressive power of a logic to that of first order logic. This maximality principle is the famous Lindström Theorem for first order logic. It reveals that first order logic is at an optimal point of balance: by adding expressive power to it one necessarily loses model-theoretic properties. Soon after Lindström’s result, the question was raised, whether there are other logics at a similar point of equilibrium. More precisely: are there strict strengthenings of first order logic satisfying a Lindström-type characterization? Despite the naturality of this question, it remained unanswered, until recently.
In 2012 Saharon Shelah offered a solution to this problem in the form of a new infinitary logic. It has a Lindström-type characterization in terms of model-theoretic properties combining weak forms of Compactness and a Löwenheim-Skolem type property. In all known cases, a proof of a Lindström-type characterization automatically gives a proof of Craig Interpolation. This is the case for Shelah’s logic, too. There is, however, one aspect where Shelah’s logic seems to be rather weak: the syntax. The logic is derived from a game, in the sense that a sentence is, by definition, a class of structures, closed under a certain Ehrenfeucht-Fraïssé type of a game. This results in the absence of a syntax defined in such a way that the set of all formulas could be obtained by closing the set of atomic formulas under negation, conjunction, quantifiers, and possibly other logical operations. The lack of syntax complicates further study of it and logics in its neighborhood. In the present talk, we address the general question of deriving a syntax from a game, and the more localized question of finding a syntax for Shelah’s logic. Partial answers are provided to both questions. This is joint work with Andres Villaveces and Siiri Kivimäki.
-
Dependence and independence concepts are ubiquitous in natural science, social science, humanities as well as in everyday life. The sentences “I park on this side of the road depending only on the day of the week” and “the time of descent is independent of the weight of the object” are examples of this. The question arises, do these concepts possess enough exactness for us to investigate their logic? There is currently a whole literature on this topic. It is the purpose of this talk to give a non-technical overview of this area of logic.
-
Opponent: Rafael Peñaloza Nyssen, Associate Professor, University of Milano-Bicocca
Abstract Knowledge bases are used in several industries to efficiently represent data but they sometimes contain errors. Debugging knowledge bases is, therefore, a vitally important process. It requires explanations of entailments in description logic which are used for answering knowledge base queries. Such explanations can be generated by axiom pinpointing, which is a technique to find justifications: minimal sets of axioms that entail a certain conclusion. Typically, a large set of justifications is found. It is difficult to select the one(s) which requires the least cognitive effort to understand. Four contributions are made with this thesis to solve this problem. First, the concept of relative cognitive complexity is defined. Second, the ACT-R model SHARP is created. It simulates the process of a human deciding the consistency of so-called ABoxes in the description logic \(\mathcal{ALE}\), the definition of which some justifications satisfy. SHARP is used for modelling cognitive effort and captures the relative cognitive complexity of \(\mathcal{ALE}\), ABoxes. Third, an experiment is performed to test the predictions on cognitive behaviour based on SHARP’s simulation results. The model performs quite well on the relative cognitive complexity. Fourth, three surrogate modelling techniques were tested: Random Forests (RF), Support Vector Regression (SVR) and Symbolic Regression (SR). The three techniques achieve similar performance, but SR achieves the lowest computation times.
Examination committee
- Associate Professor Nina Gierasimczuk, Technical University of Denmark
- Professor Fredrik Stjernberg, Linköpings universitet
- Senior Research Fellow Paul Mulholland, The Open University
- Professor Christine Howes, Göteborgs universitet (substitute)
-
The idea of articulating a propositional logic that adds a relevance-sensitive implication connective to the usual truth-functional ones has been approached in many ways, e.g. using axioms and derivation rules, natural deduction systems, possible worlds or states equipped with relations or operations, algebraic structures, consecution systems etc. None are very satisfactory. In the 1970s, semantic decomposition trees (aka truth-trees, semantic tableaux, analytic tableaux) were briefly considered, but they did not get far and were swept away by the tsunami of Routley/Meyer possible worlds with ternary relations. We renew that approach using a notion of parity for the branches of a tree or, alternatively, an even more global one of sibling-parity for the entire tree. There are some nice results and, above all, some big open questions.
-
Stone duality associates to each (finitary classical propositional) theory a topological space whose points are the models. The theory can be fully recovered from the space—this is a form of completeness: everything we need to know about the theory is encoded in the topology, and we can replace the bureaucracy of syntax by suitable topological notions.
Notably, ultraproducts of models can also be read on the space of models: the ultraproduct of a family of models corresponds to the limit of an ultrafilter on points. Through the Stone duality, this shows that ultraproducts encode all we need to know about the theory and explains the central role of the ultraproduct construction.
Of course, finitary classical propositional logic is very limited—we can go a lot further: geometric logic is a very powerful logic (encompassing classical first-order logic) that has a topological interpretation (actually a toposical interpretation).
In this talk I will explain how the ultraproduct operation induces a spaced-like structure on the models of a geometric theory, opening the way of a new understanding of model-theoretic results, where the ultraproduct of models become the ultraconvergence of points—in a formal way.
-
This talk introduces a coinductive perspective on provability, where proofs are not restricted to finite trees but may instead take the form of finite graphs or, more generally, non-wellfounded trees. Focusing on the linear-time μ-calculus, we present a sound and complete cyclic axiomatisation and demonstrate its use in establishing the interpolation property for the logic. We further show how this approach provides an insightful route to proving the completeness of the finitary axiomatisation. This work is part of a broader collaboration with Graham E. Leigh aimed at streamlining soundness and completeness proofs for modal and temporal logics.
-
There is a long tradition of distinguishing finistic methods of reasoning, for both philosophical and mathematical motivations. Typically, this is made precise by reducing arguments to some theory of arithmetic – usually Peano or Heyting Arithmetic, or weaker fragments thereof. However, working directly in such systems requires encoding all objects as numbers; it is easy to get the impression that such coding is an inherent and inevitable aspect of the topic.
On the contrary, most major foundational logics – in particular, ZF-style set theory and dependent type theories – admit finitistic variants, equivalent in strength to suitable systems of arithmetic. These allow us to work rigorously in a finististic foundation, while keeping the richly expressive language we’re used to from everyday mathematics.
I will survey various finitistic systems, and then focus in more detail on the categorical Arithmetic Universes of Joyal, and type theories for these, following Maietti.
-
A 2½-day workshop dedicated to current and future trends in cyclic and illfounded forms of provability and justification. The event is sponsored by the Knut and Alice Wallenberg Foundation via the research project Taming Jörmungandr: The Logical Foundations of Circularity, the Swedish Research Council through the research project Proofs with Cycles and Computation, and the Department of Philosophy, Linguistics and Theory of Science at the University of Gothenburg.
-
Justification logic is an explication of modal logic: boxes are replaced with proof terms formally through realisation theorems. This can be achieved syntactically using a cut-free proof system for a modal logic, e.g., using sequent, hypersequent, or nested sequent calculi. In constructive modal logic, boxes and diamonds are decoupled and not De Morgan dual. Previous work provides a justification counterpart to constructive modal logic CK (and some extensions) by making diamonds explicit and introducing new terms called satisfiers. We continue this line of work and provide a justification counterpart to intuitionistic modal logic IK and its extensions with the t and 4 axioms. We extend the syntax of proof terms to accommodate the additional axioms of intuitionistic modal logic and provide an axiomatisation of these justification logics with a syntactic realisation procedure using a cut-free nested sequent system for intuitionistic modal logic.
-
The notion of pure extension of modules, and the corresponding notions of pure-injectivity and pure-projectivity, play a central role in commutative algebra, aspecially in its connections to model theory. In joint work with Casarosa, motivated by applications to algebraic topology and operator algebras, we have introduced the first “higher order” generalization of purity, defining “pure extensions of order α” for every countable ordinal α. Classical purity corresponds to the particular case when α=0.
In this talk I will present connections with logic: as classical purity is characterized in terms of first order logic, we will show that higher order purity has a natural interpretation in terms of infinitary logic, in such a way that the order of purity corresponds to length of infinitary formulae.