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 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.
-
Modelling natural language in some form is a core motivation for computational linguists and logicians, and more recently big tech firms which favour (often very impressive) engineering solutions over rigour. Compositional-distributional models of meaning combine rigorous models of grammar, in the form of Lambek calculus, and modern NLP models, forming a framework for model meaning using structure and statistics. This framework can be neatly specified using category theory which connects sequent calculus, residuated monoids and pregroups as well as surprising links to quantum informatics.
-
Gödel intended his Dialectica interpretation to provide a foundational reduction of first-order arithmetic to a quantifier-free theory T. It has widely been objected, however, that this theory T tacitly presupposes the very quantificational logic that Gödel was trying to eliminate, hidden within its complicated definition of “computable function of finite type.” This would render the translation philosophically circular. Gödel was adamant that there was no circularity here. He sketched a defense of this claim in a page-long footnote, which however has left readers baffled. In this talk, I will explain Gödel’s footnote and show that there really is no circularity here. Thus, Gödel has achieved a significant foundational reduction. The foundations of T turn out to be stranger than meets the eye; they utilize a (broadly) Leibnizian notion of analyticity in a surprising way.
-
In this talk I will briefly outline Krister’s biography, focusing mainly on the early nineties onwards when I became Krister’s first PhD student. By appeal (mostly) to anecdote I will try to highlight what I take to be some of the most notable features in Krister’s approach to and views on pilosophically inspired logical research and education.
-
Krister Segerberg was one of the architects of modal logic as we know it today. I will highlight a few of his major contributions and show some of their subsequent impact in various academic communities. I conclude with some thoughts on the blend of philosophical logic and formal philosophy embodied in Krister’s distinguished career.
-
On Monday, 25 August the Nordic Online Logic Seminar will host a special event in memory of Krister Segerberg, who passed away in January this year. Krister Segerberg was Professor of Theoretical Philosophy at Uppsala and, among logicians, is widely known for his pioneering work in modal logic where he initiated an influential systematic study of completeness proofs that still is standard in the field.
The seminar will feature talks by two academics that knew Krister Segerberg well:
- Johan van Benthem (UvA), Building Modern Modal Logic: Honoring Krister Segerberg
- John Cantwell (KTH), Some reflections on Krister’s philosophy of philosopy
A URL for this seminar will be distributed via the GU Logic and Nordic Online Logic mailing lists.
-
Opponent: Makoto Fujiwara, Assistant Professor, Tokyo University of Science
Abstract This dissertation concerns first-order theories of iterated 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 positive fixpoints and compositional and disquotational truth for truth-positive sentences, and a comparison with the classical case.
It is known that these theories over classical Peano arithmetic (PA) are mutually interpretable and exceeds the strength of PA. Over intuitionistic Heyting arithmetic (HA), on the other hand, finite iterations of strictly positive fixpoints have been shown to be conservative.
After introducing the setting and presenting the earlier results, as well as the technical tools, the main section of the dissertation can be roughly divided into two parts. The first presents a novel proof of the conservativity result above. The proof interprets the theories into the logic of partial terms where a realizability interpretation is used to reduce the problem to fixpoints for almost negative operator forms. A diagonal argument using a hierarchy of almost negative formulae with corresponding partial satisfaction predicates yields the result.
The second part generalises the tri-interpretation result from the second paragraph to intuitionistic theories, by proposing a new generalisation of positivity called guarded positivity with the aim to better capture the behaviour of intuitionistic implications and their interplay with transfinite iterations of truth and fixpoint predicates. As a corollary, these transfinite theories are stronger than HA.
A discussion of the results and the methods used concludes the dissertation.
Examination committee:
- Vera Koponen, chair (Uppsala University)
- Takako Nemoto (Tohoku University)
- Benno van den Berg (University of Amsterdam)