Seminars
Seminars, workshops and other events organised by our group
The Logic Group runs a biweekly 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.

Paraas Padhiar (University of Birmingham)
Nested sequents for ScottLemmon path axioms
Previous works by Goré, Postniece and Tiu have provided sound and cutfree complete proof systems for modal logics extended with path axioms using the formalism of nested sequent. Our aim is to provide (i) a constructive cutelimination 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 quasitransitivity axioms.

Mattias Granberg Olsson (FLoV)
Fixed IDs about truth: Truth and fixpoints in intuitionistic logic (final seminar)
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 truthpositive sentences, and a comparison with the classical case.
Opponent: Gerhard Jäger, Professor Emiratus University of Bern

Lide Grotenhuis (University of Amsterdam)
Intuitionistic mucalculus with the Lewis arrow
Modal logic can be traced back to Lewis’ introduction of a modal connective for ‘strict implication’, also known as the Lewis arrow. Classically, the Lewis arrow is interdefinable with box, and so the connective has fallen into disuse over time. Over an intuitionistic base, however, the arrow is more expressive than the box.
With the aim of setting up a general framework for intuitionistic fixed point modal logics, we study an intuitionistic version of the mucalculus with the Lewis arrow as modal connective. Formulas are interpreted over birelational Kripke models, which satisfy a confluence condition to ensure monotonicity with respect to the intuitionistic order.
In this talk, I will introduce both algebraic and game semantics for the logic, and provide a complete nonwellfounded proof system for guarded formulas. Moreover, I will show how Ruitenburg’s theorem can be used to prove that every formula is equivalent to a guarded one, thereby showing that this wellknown result for the classical mucalculus still holds in the intuitionistic case.
This is joint work with Bahareh Afshari.

Nina Gierasimczuk (Danish Technical University)
Coordinating quantity terms: a simulation study in monotonicity and convexity
Natural languages vary in their quantity expressions, but the variation seems to be constrained by general properties, socalled 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 stateoftheart multiagent 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.

Lide Grotenhuis (University of Amsterdam)
(Cancelled) Intuitionistic mucalculus with the Lewis arrow
Talk postponed to 10 October.
Modal logic can be traced back to Lewis’ introduction of a modal connective for ‘strict implication’, also known as the Lewis arrow. Classically, the Lewis arrow is interdefinable with box, and so the connective has fallen into disuse over time. Over an intuitionistic base, however, the arrow is more expressive than the box.
With the aim of setting up a general framework for intuitionistic fixed point modal logics, we study an intuitionistic version of the mucalculus with the Lewis arrow as modal connective. Formulas are interpreted over birelational Kripke models, which satisfy a confluence condition to ensure monotonicity with respect to the intuitionistic order.
In this talk, I will introduce both algebraic and game semantics for the logic, and provide a complete nonwellfounded proof system for guarded formulas. Moreover, I will show how Ruitenburg’s theorem can be used to prove that every formula is equivalent to a guarded one, thereby showing that this wellknown result for the classical mucalculus still holds in the intuitionistic case.
This is joint work with Bahareh Afshari.

Zach McKenzie (University of Chester)
Wellfounded models of fragments of Collection
Let M be the weak set theory obtained from ZF by removing the Collection Scheme, restricting the Separation Scheme to bounded formulae, and adding an axiom asserting that every set is contained transitive set. In this talk I will consider two formulations of the settheoretic Collection Scheme restricted formulae that are Π_{n} in the Levy hierarchy: Π_{n}Collection and Strong Π_{n}Collection. It is known that, over M, Strong Π_{n}Collection is equivalent to Π_{n}Collection plus Σ_{n+1}Separation, and Strong Π_{n}Collection proves the consistency of M + Π_{n}Collection. In this talk I will show that for all n > 0, every wellfounded model of M + Π_{n}Collection satisfies Strong Π_{n}Collection. In particular, for n > 0, M + Strong Π_{n}Collection does not prove the existence of a transitive model of M + Π_{n}Collection. And, for n > 0, the minimum model of M + Strong Π_{n}Collection and M + Π_{n}Collection coincide. If time permits, I will indicate how the assumption that that the model is wellfounded can be replaced with the assumption that the model instead satisfies a fragment of Foundation. This reveals new equivalences between subsystems of ZF that include the Powerset axiom.

Daniël Otten (University of Amsterdam)
Cyclic Type Theory
We explain some of the connections between two research areas: cyclic proof theory and proof assistants. This talk is based on joint workinprogress with Lide Grotenhuis.
In cyclic proof theory, we replace induction axioms with circular reasoning. By carefully placing restrictions on cycles, we can make sure that we do not prove more than with induction. Such cyclic proofs can be interpreted as programs using the CurryHoward correspondence: cycles correspond to recursive calls, while the restrictions make sure that the program always terminates. Using this perspective, we show how the type theory implemented by proof assistants can be seen as a cyclic proof system: one where programs/proofs are defined using (co)pattern matching. We show some of the difficulties that come up specifically in dependent type theory: why unification becomes important, and how one can translate cyclic proofs to inductive proofs while preserving computational behavior. In addition, we show how some of the techniques from cyclic proof theory might be used to extend proof assistants.

Eric Pacuit (University of Maryland)
From paradox to principles: Splitting cycles and breaking ties
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 socalled “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.

The Logic Colloquium 2024
The 2024 Annual European Meeting of the Association for Symbolic Logic, also known as the Logic Colloquium, will be held in Gothenburg on 2428 June, 2024 and hosted by the Faculty of Humanities at the University of Gothenburg. The colloquium comprises 3 tutorials, 7 plenary lectures and 6 special sessions as well as contributed talks. In addition, the 2024 Gödel Lecture was delivered at the meeting.
See lc2024.se for full information.

Dominik Kirst (Inria Paris)
Mechanised metamathematics: synthetic computability and incompleteness in Coq