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.

Nina Gierasimczuk (Danish Technical University)
Nina Gierasimczuk

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.

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

Ivano Ciardelli (University of Padua)
Inquisitive modal logic: an overview
Inquisitive modal logic is a generalization of standard modal logic where the language also contains questions, and modal operators that can be applied to them. In this talk, I will provide an introductory overview of inquisitive modal logic. I will review some motivations for the approach, present some prominent examples of inquisitive modal logics, mention some results about them, and outline directions for future work.

Ana María MoraMárquez (University of Gothenburg)
Medieval Aristotelian Logic is Scientific Method
This presentation aims to show that medieval Aristotelian logic can be generally characterized as scientific method. To be sure, this method includes formal logic as one of its parts, but formal logic is by no means the crucial part. In fact, if, as I intend to show, the main aim of medieval Aristotelian logic is to provide methods for knowledge production and distribution, so its crucial parts are the methods for scientific proof provided in commentaries on Aristotle’s Posterior Analytics and Topics.
In the first part of the presentation, I argue for the possibility of talking of medieval ‘science’, ‘scientific knowledge’, and ‘scientific method’ from a modern perspective, and discuss how the modern perspective relates to the Latin ‘scientia’ in its different senses. In the second part, I show the progression from Nicholas of Paris (1240s) and Albert the Great (1250s), who see Aristotelian logic as a systematic scientific method where syllogistic argument is fundamental, but who struggle to coherently organize it around syllogistic argument, to Radulphus Brito (1290s) who, still seeing Aristotelian logic as scientific method, uses the notion of ‘second intention’ in order to coherently structure it around syllogistic argument.

Orvar Lorimer Olsson (FLoV)
Logics of PowerAlgebras: the Boolean case
Using semantics based on algebras commonplace in the study of logics, however this usage can take forms: Manyvalued logics are commonly described in terms of valuations into a single algebra of truth values, whereas other treatments concern full classes of algebraic structures such as varieties defined by equation theories. This has given rise to similar constructions within different fields of study, but where the direct connections may not to be fully spelled out.
Working from the manyvalued perspective, in [1], by lifting the consideration of valuations into subsets of an algebra, Priest defines what he calls the plurivalent version of a logic. This process essentially constitutes taking the poweralgebra of truth values from the original logic, as described by Brink [2], together with a conservative choice of truth condition inherited from the original algerba essentially through memberhood statements of specific elements. In the simplest example of this construction Priest can identify some well known multivalued logics as plurivalent logics on classical truth values of the two valued Boolean algebra [1]. However this identification fails if the construction was conducted on any other than this specific Boolean algebra.
Continuing work towards general methods for logics with team semantics [3] I will in this presentation consider the poweralgebras of arbitrary Boolean algebras and establish a sound and complete labelled natural deduction system for entailments of memberhood statements. This gives rise to the definition and presentation of logics that can be viewed as substructural versions of the referred manyvalued logics with proof systems for which additional rules can be added to obtain the original logic.
We will finish by reflecting on the achieved construction, and consider how it can be generalised from the class of Boolean Algebras to constructing logics based on other equational classes of algebras.
References
 Graham Priest, Plurivalent logics, The Australasian Journal of Logic, vol. 11 (2014), no. 1.
 Chris Brink, Power structures, Algebra Universalis, vol. 30 (1993), pp. 177–216.
 Fredrik Engström, Orvar Lorimer Olsson, The propositional logic of teams, arXiv preprint, (2023), arXiv.2303.14022