See below for a list of all previous and upcoming seminars in the Gothenburg Research Seminar in Logic and the Nordic Online Logic Seminar. We also run a bi-weekly Colloquium in Logic focused in the Masters in Logic; details and schedules are listed on the course page of the Masters Programme.

The research seminar meets on alternate Fridays at 10.15. Talk locations (i.e., Zoom link) are distributed in the GU Logic mailing list. Alternatively, contact Graham Leigh directly.

Autumn 2021

Nordic Online Logic Seminar
Lars Birkedal (Aarhus University) – Iris: A Higher-Order Concurrent Separation Logic Framework

I will introduce some of our research on Iris, a higher-order concurrent separation logic framework, implemented and verified in the Coq proof assistant, which can be used for mathematical reasoning about safety and correctness of concurrent higher-order imperative programs. Iris has been used for many different applications; see for a list of research papers. However, in this talk I will focus on the Iris base logic (and its semantics) and sketch how one may define useful program logics on top of the base logic. The base logic is a higher-order intuitionistic modal logic, which, in particular, supports the definition of recursive predicates and whose type of propositions is itself recursively defined.

This talk is part of the Nordic Online Logic Seminar.
Dominik Wehr (FLoV) – Abstract Cyclic Proofs

Cyclic proof systems permit derivations to contain cycles, thereby serving as finite representations of non-wellfounded derivation trees. Such cyclic proof systems have been proposed for a broad range of logics, especially those with fixed-point features or inductively defined objects of reasoning. The soundness of such systems is commonly ensured by only considering those cyclic derivations as proofs which satisfy a so-called global trace condition.

In this talk, I will present a category theoretical notion, the trace category, which generalizes the trace condition of many cyclic proof systems. Indeed, a handful of different trace categories are sufficient to capture the trace conditions of all cyclic proof systems from the literature I have examined so far. The arising abstract notion of cyclic proof allows for the derivation of generalized renditions of standard results of cyclic proof theory, such as the decidability of proof-checking and the regularizability of certain non-wellfounded proofs. It also opens the door to broader inquiries into the structural properties of trace condition based cyclic and non-wellfounded proof systems, some of which I will touch on in this talk, time permitting. The majority of this talk will be based on my Master’s thesis.

Paula Quinon (Warsaw University of Technology and FLoV) – Invariances and the number concept

Cognitive scientists Spelke and Kintzler (2007) and Carey (2009) propose objects, actions, space and numbers as ‘core domains of knowledge’ that underpin the framework of concepts people use to describe and communicate about the world. Gärdenfors (2019, 2020) argues that humans make sense of domains by appealing to various types of invariances in sensory signals. In this talk, I present work by Quinon and Gärdenfors (manuscript) in which the aim is to extend the analysis in terms of invariances to the domain of numbers. We focus on several perspectives relating invariances: cognitive modeling, formal mathematical and experimental.

As theoretical background, we assume that numbers are properties of collections (Simons 1982, 2007, 2011; Johansson 2015; Angere 2014). We observe that the domain of number is determined by two types of invariances. First, the concept of collection itself depends on being invariant under the location of its objects. Second, the determinant invariance of the domain of number is the fungibility of objects: If an object in a collection is exchanged for another object, the collection will still contain the same number of objects. Fungibility will be shown to be closely related to one-to-one correspondences.

We first introduce the concept of a collection and show how it differs from the concept of a set. Then we present the invariance of location of objects that applies to collections and we introduce fungibility as a second type of invariance. We illustrate our theoretical analysis by empirical material from experiments of developmental psychologists.

This is joint work with Peter Gärdenfors (Lund).

Nordic Online Logic Seminar
Sara L. Uckelman (Durham University) – John Eliot’s Logick Primer: A bilingual English-Wôpanâak logic textbook

In 1672 John Eliot, English Puritan educator and missionary, published The Logick Primer: Some Logical Notions to initiate the INDIANS in the knowledge of the Rule of Reason; and to know how to make use thereof [1]. This roughly 80 page pamphlet focuses on introducing basic syllogistic vocabulary and reasoning so that syllogisms can be created from texts in the Psalms, the gospels, and other New Testament books. The use of logic for proselytizing purposes is not distinctive: What is distinctive about Eliot’s book is that it is bilingual, written in both English and Wôpanâak (Massachusett), an Algonquian language spoken in eastern coastal and southeastern Massachusetts. It is one of the earliest bilingual logic textbooks, it is the only textbook that I know of in an indigenous American language, and it is one of the earliest printed attestations of the Massachusett language.

In this talk, I will:

  • Introduce John Eliot and the linguistic context he was working in.
  • Introduce the contents of the Logick Primer—vocabulary, inference patterns, and applications.
  • Discuss notions of “Puritan” logic that inform this primer.
  • Talk about the importance of his work in documenting and expanding the Massachusett language and the problems that accompany his colonial approach to this work.


[1] J.[ohn] E.[liot]. The Logick Primer: Some Logical Notions to initiate the INDIANS in the knowledge of the Rule of Reason; and to know how to make use thereof. Cambridge, MA: Printed by M.[armaduke] J.[ohnson], 1672.

This talk is part of the Nordic Online Logic Seminar.
Graham E. Leigh (FLoV) – From interpolation to completeness

I will demonstrate how Walukiewicz’ seminal proof of completeness for the propositional μ-calculus can be derived (and refined) from the cyclic proof theory of the logic, notably the uniform interpolation theorem for the logic.

Fredrik Engström (FLoV) – Foundational principles of team semantics

Team semantics is, when compared to standard Tarskian semantics, a more expressive framework that can be used to express logical connectives, operations and atoms that can’t be expressed in Tarskian semantics. This includes branching quantifiers, notions of dependence and independence, trace quantification in linear-time temporal logic (LTL), and probabilistic notions from quantum mechanics.

Team semantics is based on the same notion of structure as Tarskian semantics, but instead of a single assignment satisfying a formula (or not), in team semantics a set, or a team, of assignments satisfies a formula (or not). In other words, the semantic value of a formula is lifted from a set of assignments (those that satisfy the formula) to a set of teams of assignments.

In almost all (with only one exception that I’m aware of) logical systems based on team semantics this lifting operation is the power set operation, and as a result the set of teams satisfying a formula is closed downwards. This is often taken as a basic and foundational principle of team semantics.

In this talk I will discuss this principle and present some ideas on why, or why not, the power set operation is the most natural lift operation. By using other lift operations we can get a more powerful semantics, but, it seems, also a more complicated one.


  • Engström, F. (2012) “Generalized quantifiers in dependence logic”
  • Nurmi, V. (2009) “Dependence Logic: Investigations into Higher-Order Semantics Defined on Teams”
  • Väänänen, J. (2007) “Dependence logic: A new approach to independence friendly logic”
Nordic Online Logic Seminar
Erich Grädel (RWTH Aachen University) – Semiring semantics for logical statements with applications to the strategy analysis of games

Semiring semantics of logical formulae generalises the classical Boolean semantics by permitting multiple truth values from certain semirings. In the classical Boolean semantics, a model of a formula assigns to each (instantiated) literal a Boolean value. K-interpretations, for a semiring K, generalize this by assigning to each such literal a value from K. We then interpret 0 as false and all other semiring values as nuances of true, which provide additional information, depending on the semiring: For example, the Boolean semiring over {0,1} corresponds classical semantics, the Viterbi-semiring can model confidence scores, the tropical semiring is used for cost analysis, and min-max-semirings (A, max, min, a, b) for a totally ordered set (A,<) can model different access levels. Most importantly, semirings of polynomials, such as N[X], allow us to track certain literals by mapping them to different indeterminates. The overall value of the formula is then a polynomial that describes precisely what combinations of literals prove the truth of the formula.

This can also be used for strategy analysis in games. Evaluating formulae that define winning regions in a given game in an appropriate semiring of polynomials provides not only the Boolean information on who wins, but also tells us how they win and which strategies they might use. For this approach, the case of Büchi games is of special interest, not only due to their practical importance, but also because it is the simplest case where the logical definition of the winning region involves a genuine alternation of a greatest and a least fixed point. We show that, in a precise sense, semiring semantics provide information about all absorption-dominant strategies – strategies that win with minimal effort, and we discuss how these relate to positional and the more general persistent strategies. This information enables further applications such as game synthesis or determining minimal modifications to the game needed to change its outcome.

This talk is part of the Nordic Online Logic Seminar.
João Pedro Paulos (Chalmers) – A collection of small closed sets: sets of uniqueness

Sets of uniqueness and their properties are traditionally investigated in Harmonic Analysis. The study of such sets has a long and illustrious history, witnessing fruitful interdisciplinary interactions, often enriching the subject with a vibrant fertility for crossover of ideas. In this talk, we set up the modern framework used to study such sets with particular emphasis on some (classical) descriptive set-theoretic aspects. We present some results concerning the family of closed sets of uniqueness of a locally compact Polish group - more concretely, we will talk about their complexity and the (in)existence of a Borel basis.

Mateusz Łełyk (University of Warsaw) – Axiomatizations of Peano Arithmetic: a truth-theoretic view

We employ the lens provided by formal truth theory to study axiomatizations of PA (Peano Arithmetic). More specifically, let EA (Elementary Arithmetic) be the fragment I∆0 + Exp of PA, and CT[EA] be the extension of EA by the commonly studied axioms of compositional truth CT. The truth theory delivers a natural preorder on the set of axiomatizations: an axiomatization A is greater or equal to an axiomatization B if and only if, over CT-[EA], the assertion “All axioms from A are true” implies “All axioms from B are true”. Our focus is dominantly on two types of axiomatizations, namely: (1) schematic axiomatizations that are deductively equivalent to PA, and (2) axiomatizations that are proof-theoretically equivalent to the canonical axiomatization of PA.

The first part of the talk focuses on the axiomatizations of type (1). We adapt the argument by Visser and Pakhomov (“On a question of Krajewski’s”, JSL 84(1), 2019) to show that there is no weakest axiomatization of this form (even if the axiomatizations are ordered by relative interpretability). Secondly, we sketch an argument showing that such axiomatizations with the given ordering form a countably universal partial order. This part is based on our joint work with Ali Enayat, available at

In the second part of the talk we discuss axiomatizations of type (2). We narrow our attention to such axiomatizations A for which CT-[EA] + “All axioms from A are true” is a conservative extension of PA. We explain why such theories have very diverse metamathematical properties (e.g. large speed-up). To illustrate our methods we show that, with the given ordering, such axiomatizations do not form a lattice. This is a work still in progress.

Nordic Online Logic Seminar
Anupam Das (University of Birmingham) – On the proof theoretic strength of cyclic reasoning

Cyclic (or circular) proofs are now a common technique for demonstrating metalogical properties of systems incorporating (co)induction, including modal logics, predicate logics, type systems and algebras. Inspired by automaton theory, cyclic proofs encode a form of self-dependency of which induction/recursion comprise special cases. An overarching question of the area, the so-called ‘Brotherston-Simpson conjecture’, asks to what extent the converse holds.

In this talk I will discuss a line of work that attempts to understand the expressivity of circular reasoning via forms of proof theoretic strength. Namely, I address predicate logic in the guise of first-order arithmetic, and type systems in the guise of higher-order primitive recursion, and establish a recurring theme: circular reasoning buys precisely one level of ‘abstraction’ over inductive reasoning.

This talk will be based on the following works:

This talk is part of the Nordic Online Logic Seminar.
Nachiappan Valliappan (Chalmers) – Normalization for Fitch-style Modal Lambda Calculi

Fitch-style modal lambda calculi (Borghuis 1994; Clouston 2018) provide a solution to programming necessity modalities in a typed lambda calculus by extending the typing context with a delimiting operator (denoted by a lock). The addition of locks simplifies the formulation of typing rules for calculi that incorporate different modal axioms, but obscures weakening and substitution, and requires tedious and seemingly ad hoc syntactic lemmas to prove normalization.

In this work, we take a semantic approach to normalization, called Normalization by Evaluation (NbE) (Berger and Schwichtenberg 1991), by leveraging the possible world semantics of Fitch-style calculi. We show that NbE models can be constructed for calculi that incorporate the K, T and 4 axioms, with suitable instantiations of the frames in their possible world semantics. In addition to existing results that handle beta reduction (or computational rules), our work also considers eta expansion (or extensional equality rules).


  • Borghuis, V.A.J. (1994). “Coming to terms with modal logic : on the interpretation of modalities in typed lambda-calculus”.
  • Clouston, Ranald (2018). “Fitch-Style Modal Lambda Calculi”.
  • Berger, Ulrich and Helmut Schwichtenberg (1991). “An Inverse of the Evaluation Functional for Typed lambda-calculus”.

Spring 2021

Nordic Online Logic Seminar
Dag Normann (Oslo) – An alternative perspective on Reverse Mathematics

In his address to the International Congress of Mathematics in Vancouver, 1974, Harvey Friedman launched a program where the aim would be to find the minimal set of axioms needed to prove theorems of ordinary mathematics. More than often, it turned out that the axioms then would be provable from the theorems, and the subject was named Reverse Mathematics. In this talk we will survey some of the philosophy behind, and results of, the early reverse mathematics, based on the formalisation of mathematics within second order number theory.

In 2005, Ulrich Kohlenbach introduced higher order reverse mathematics, and we give a brief explanation of the what and why? of Kohlenbach’s approach. In an ongoing project with Sam Sanders we have studied the strength of classical theorems of late 19th/early 20th century mathematics, partly within Kohlenbach’s formal typed theory and partly by their, in a generalised sense, constructive content. In the final part of the talk I will give some examples of results from this project, mainly from the perspective of higher order computability theory. No prior knowledge of higher order computability theory is needed.

This talk is part of the Nordic Online Logic Seminar.
Victor Lisinski (Corpus Christi, Oxford) – Decidability problems in number theory

In its modern formulation, Hilbert’s tenth problem asks to find a general algorithm which decides the solvability of Diophantine equations. While this problem was shown to be unsolvable due to the combined work of Davis, Putnam, Robinson and Matiyasevich, similar question can be posed over domains other than the integers. Among the most important open questions in this area of research is if a version of Hilbert’s tenth problem for Fp((t)), the field of formal Laurent series over the finite field Fp, is solvable or not. The fact that this remains open stands in stark contrast to the fact that the first order theory of the much similar object Qp, the field of p-adic numbers, is completely understood thanks to the work by Ax, Kochen and, independently, Ershov. In light of this dichotomy, I will present new decidability results obtained during my doctoral research on extensions of Fp((t)). This work is motivated by recent progress on Hilbert’s tenth problem for Fp((t)) by Anscombe and Fehm and builds on previous decidability results by Kuhlman.

Juliette Kennedy (Helsinki) – Logicality and Model Classes

When is a property of a model a logical property? According to the so-called Tarski-Sher criterion this is the case when the property is preserved by isomorphisms. We relate this to the model-theoretic characteristics of abstract logics in which the model class is definable, resulting in a graded concept of logicality (in the terminology of Sagi’s paper “Logicality and meaning”). We consider which characteristics of logics, such as variants of the Löwenheim-Skolem Theorem, Completeness Theorem, and absoluteness, are relevant from the logicality point of view, continuing earlier work by Bonnay, Feferman, and Sagi. We suggest that a logic is the more logical the closer it is to first order logic, and offer a refinement of the result of McGee that logical properties of models can be expressed in L∞∞ if the expression is allowed to depend on the cardinality of the model, based on replacing L∞∞ by a “tamer” logic. This is joint work with Jouko Väänänen.

Nordic Online Logic Seminar
Wilfrid Hodges (Fellow of the British Academy) – How the teenage Avicenna planned out several new logics

Almost exactly a thousand years ago a teenager known today as Avicenna lived in what is now Uzbekistan. He made a resolution to teach himself Aristotelian logic, armed with an Arabic translation of Aristotle and a century-old Arabic textbook of logic. A couple of years later, around his eighteenth birthday, he wrote a brief report of what he had learned. Six months ago I started to examine this report - I suspect I am the first logician to do that. It contains many surprising things. Besides introducing some new ideas that readers of Avicenna know from his later works, it also identifies some specific points of modal logic where Avicenna was sure that Aristotle had made a mistake. People had criticised Aristotle’s logic before, but not at these points. At first Avicenna had no clear understanding of how to do modal logic, and it took him another thirty years to justify all the criticisms of Aristotle in his report. But meanwhile he discovered for himself how to defend a new logic by building new foundations. I think the logic itself is interesting, but the talk will concentrate on another aspect. These recent discoveries mean that Avicenna is the earliest known logician who creates new logics and tells us what he is doing, and why, at each stage along the way.

This talk is part of the Nordic Online Logic Seminar.
Mattias Granberg Olsson (FLoV) – A proof of conservativity of fixed points over Heyting arithmetic via truth

I will present work in progress (together with Graham Leigh) on a novel proof of the conservativity of the intuitionistic fix-point theory over Heyting arithmetic (HA), originally proved in full generality by Arai [1]. We make use of the work of van den Berg and van Slooten [2] on realizability in Heyting arithmetic over Beeson’s logic of partial terms (HAP). Let IF be the extension of Heyting arithmetic by fix-points, denoted \hat{ID}i1 in the literature. The proof is divided into four parts: First we extend the inclusion of HA into HAP to IF into a similar theory IFP in the logic of partial terms. We then show that every theorem of this theory provably has a realizer in the theory IFP(Λ) of fix-points for almost negative operator forms only. Constructing a hierarchy stratifying the class of almost negative formulae and partial truth predicates for this hierarchy, we use Gödel’s diagonal lemma to show IFP(Λ) is interpretable in HAP. Finally we use use the result of [2] that adding the schema of “self-realizability” for arithmetic formulae to HAP is conservative over HA. The result generalises the work presented at my half-time seminar 2020-08-28.


[1] Toshiyasu Arai. Quick cut-elimination for strictly positive cuts. Annals of Pure and Applied Logic, 162(10):807–815, 2011.

[2] Benno van den Berg and Lotte van Slooten. Arithmetical conservation results. Ind- agationes Mathematicae, 29:260–275, 2018.

Sonia Marin (UCL) – Focused nested calculi for modal and substructural logics

Focusing is a general technique for syntactically compartmentalising the non-deterministic choices in a proof system, which not only improves proof search but also has the representational benefit of distilling sequent proofs into synthetic normal forms. However, since focusing was traditionally specified as a restriction of the sequent calculus, the technique had not been transferred to logics that lack a (shallow) sequent presentation, as is the case for some modal or substructural logics.

With K. Chaudhuri and L. Straßburger, we extended the focusing technique to nested sequents, a generalisation of ordinary sequents, which allows us to capture all the logics of the classical and intuitionistic S5 cube in a modular fashion. This relied on an adequate polarisation of the syntax and an internal cut-elimination procedure for the focused system which in turn is used to show its completeness.

Recently, with A. Gheorghiu, we applied a similar method to the logic of Bunched Implications (BI), a substructural logic that freely combines intuitionistic logic and multiplicative linear logic. For this we had first to reformulate the traditional bunched calculus for BI using nested sequents, followed again by a polarised and focused variant that we show is sound and complete via a cut-elimination argument.

Nordic Online Logic Seminar
Jouko Väänänen (Helsinki) – Dependence logic: Some recent developments

In the traditional so-called Tarski’s Truth Definition the semantics of first order logic is defined with respect to an assignment of values to the free variables. A richer family of semantic concepts can be modelled if semantics is defined with respect to a set (a “team”) of such assignments. This is called team semantics. Examples of semantic concepts available in team semantics but not in traditional Tarskian semantics are the concepts of dependence and independence. Dependence logic is an extension of first-order logic based on team semantics. It has emerged that teams appear naturally in several areas of sciences and humanities, which has made it possible to apply dependence logic and its variants to these areas. In my talk I will give a quick introduction to the basic ideas of team semantics and dependence logic as well as an overview of some new developments, such as quantitative analysis of team properties, a framework for a multiverse approach to set theory, and probabilistic independence logic inspired by the foundations of quantum mechanics.

This talk is part of the Nordic Online Logic Seminar.
Carlo Nicolai (King's College) – A New Look at Cut Elimination for Compositional Truth

In the field of axiomatic theories of truth, conservativity properties of theories are much investigated. Conservativity can be used to argue that, despite the well-known undefinability of truth, there is a sense in which a primitive truth predicate can be reduced to the resources of an underlying mathematical theory that provides basic syntactic structure to truth ascriptions. Conservativity is typically proved model-theoretically, or proof-theoretically via the elimination of cuts on formulae containing truth (Tr-cuts). The original Tr-cut-elimination argument for the theory of Tarskian, compositional truth CT[B] by Halbach is not conclusive. This strategy has been corrected by Graham Leigh: Leigh supplemented Halbach’s strategy with the machinery of approximations (introduced by Kotlarski, Krajewski and Lachlan in the context of their M-Logic). In the talk we investigate a different, and arguably simpler way of supplementing Halbach’s original strategy. It is based on an adaptation of the Takeuti/Buss free-cut elimination strategy for first-order logic to the richer truth-theoretic context. If successful, the strategy promises to generalize to the type-free setting in a straightforward way. This is joint work with Luca Castaldo.

Nordic Online Logic Seminar
Dag Prawitz (Stockholm) – Validity of inference and argument

An account of inferences should take into account not only inferences from established premisses but also inferences made under assumptions. This makes it necessary to consider arguments, chains of inferences in which assumptions and variables may become bound. An argument is valid when all its inferences are valid, and it then amounts to a proof in case it has no unbound assumptions or variables. The validity of an inference – not to confuse with the conclusion being a logical consequence of the premisses – seems in turn best explained in terms of proofs. This means that the concepts of valid inference and valid argument depend on each other and cannot be defined independently but have to be described by principles that state how they are related. A number of such principles will be proposed. It is conjectured that inferences that can be expressed in the language of first order intuitionistic predicate logic and are implied to be valid by these principles are all provable in that logic.

This talk is part of the Nordic Online Logic Seminar.
Lance Rips (Northwestern University) – Experimenting with (Conditional) Perfection

Conditional perfection is the phenomenon in which conditionals are strengthened to biconditionals. In some contexts, “If A, B” is understood as if it meant “A if and only if B.” I’ll present and discuss a series of experiments designed to test one of the most promising pragmatic accounts of conditional perfection. This is the idea that conditional perfection is a form of exhaustification, triggered by a question that the conditional answers. If a speaker is asked how B comes about, then the answer “If A, B” is interpreted exhaustively to meaning that A is the only way to bring about B. Hence, “A if and only if B.” The evidence suggests that conditional perfection is a form of exhaustification, but not that it is triggered by a relationship to a salient question. (This is joint work with Fabrizio Cariani.)

Giacomo Barlucchi and Tjeerd Fokkens (FLoV) – PhD Project Presentations

Project presentations

Bahareh Afshari (FLoV) – Cyclic Proof Systems for Modal Logics

A cyclic proof is a, possibly infinite but, regular derivation tree in which every infinite path satisfies a certain soundness criterion, the form of which depends on the logic under study. Circular and, more generally, non-wellfounded derivations are not traditionally regarded as formal proofs but merely as an intermediate machinery in proof-theoretic investigations. They are, however, an important alternative to finitary proofs and in the last decade have helped break some important barriers in the proof theory of logics formalising inductive and co-inductive concepts. In this talk we focus on cyclic proofs for modal logics, ranging from Gödel-Löb logic to more expressive languages such as the modal mu-calculus, and reflect on how they can contribute to the development of the theory of fixed point modal logic.

Autumn 2020

Rasmus Blanck (FLoV) – Interpretability and flexible formulas

This talk is about two different generalisations of Gödel’s incompleteness theorems and the (natural?) idea of trying to merge the two into a stronger result. The first generalisation I have in mind is Feferman’s theorem on the “interpretability of inconsistency”. This result strengthens the second incompleteness theorem, by showing that the sentence expressing that PA is inconsistent is not only consistent with PA, but even that PA + “PA is inconsistent” is interpretable in PA. The second generalisation is due to Kripke, who showed that there is a flexible formula: a formula “whose extension as a set is left undetermined” by PA. In particular, he constructed a Σ-1 formula γ(x), such that for every Σ-1 formula σ(x), the theory PA + “γ = σ” is consistent. This result generalises the first incompleteness theorem, since any instance of such a γ must be independent of PA. Unfortunately, the straightforward combination of Feferman’s and Kripke’s theorems — the “interpretability of flexibility” — is a false claim. Indeed, it is easy to show that there can be no Σ-1 formula γ such that for all Σ-1 formulae σ, the theory PA + “γ = σ” is interpretable in PA.

There are, however, several weaker results available, due to Enayat, Hamkins, Shavrukov, Woodin, and me. These results either (1) relax the restriction on γ, (2) further restrict the allowed choices of σ’s, (3) strengthen the interpreting theory beyond PA, or (4) use equality modulo finite differences. I will present these four intermediate results, along with the remaining question that they all fail to answer. Finally, I will discuss why the known proof method does not seem to lend itself to giving a positive answer to this remaining question, as well as explain how any counterexample would have to look.

Rajeev Goré (Australian National University) – Bi-Intuitionistic Logics: a New Instance of an Old Problem

As anyone who reads the literature on bi-intuitionistic logic will know, the numerous papers by Cecylia Rauszer are foundational but confusing. For example: these papers claim and retract various versions of the deduction theorem for bi-intuitionistic logic; they erroneously claim that the calculus is complete with respect to rooted canonical models; and they erroneously claim the admissibility of cut in her sequent calculus for this logic. Worse, authors such as Crolard, have based some of their own foundational work on these confused and confusing results and proofs. We trace this confusion to the axiomatic formalism of RBiInt in which Rauszer first characterized bi-intuitionistic logic and show that, as in modal logic, RBiInt can be interpreted as two different consequence relations. We remove this ambiguity by using generalized Hilbert calculi, which are tailored to capture consequence relations. We show that RBiInt leads to two logics, wBIL and sBIL, with different extensional and meta-level properties, and that they are, respectively, sound and strongly complete with respect to the Kripkean local and global semantic consequence relations of bi-intuitionistic logic. Finally, we explain where they were conflated by Rauszer.

Stefan Hetzl (TU Wien) – Formula equations

A formula equation is a formula in first-order logic with unknowns representing predicates. Solving a formula equation consists of finding first-order instances of these unknowns that result in a valid formula. In this talk I will first give an overview of this topic and, in particular, describe its connections to well-known problems in logic and its applications in computer science. I will then concentrate on specific classes of formula equations and present

  1. joint work with J. Kloibhofer on solutions of Horn formula equations in first-order logic with least fixed points and
  2. joint work with S. Zivota showing that solvability of affine formula equations is decidable, thus generalising previous results about loop invariant generation.
Benno van den Berg (ILLC, Amsterdam) – Quadratic type checking for objective type theory

An important fact about type theory, and something which is also heavily exploited in implementations, is that type checking is decidable However, from a complexity-theoretic point of view the worst case upper bounds are quite serious: according to a result by Statman from 1979, the problem is not elementary recursive. Recently, in the context of homotopy type theory people have started to consider a version of type theory in which all computation rules are replaced by propositional equalities. In this talk, I will discuss this version of type theory, which one could call “objective type theory”. In particular, I will show that if one formulates this objective type theory with sufficient care, type checking can be done in quadratic time. (This is joint work with my PhD student Martijn den Besten.)

Mateusz Łełyk (Warsaw) – Between Disquotation and Compositionality

The talk will be devoted to the formal connections between two canonical types of axiomatizations for the truth predicate: the disquotational scheme and the compositional clauses. We will be interested in measuring the “logical distance” between the two canonical sets of principles and determining whether each of them “determine” the other. Working in the framework of axiomatic truth theories we shall consider various ways of formalizing the above two questions and present the current state of art. The talk initializes the project (under the same name) which started in Warsaw at the beginning of September. At the current time there are still much more questions than answers, but we believe that it is worth uncovering this research perspective. Some questions will be investigated jointly with the Gothenburg logic group.

Paul Kindvall Gorbow (FLoV) – The Copernican Multiverse of Sets

We develop an untyped semantic framework for the multiverse of set theory and show that its proof-theoretic commitments are mild. ZF is extended with semantical axioms utilizing the new symbols M(U) and M(U,σ), expressing that U is a universe and that σ is true in the universe U, respectively. Here σ ranges over the augmented language, leading to liar-style phenomena that are analysed. The framework is both compatible with a broad range of multiverse conceptions and suggests its own philosophically and semantically motivated multiverse principles.

Spring 2020

Jean-Philippe Bernardy (FLoV) – A Unified View of Modalities in Type Systems

We propose to unify the treatment of a broad range of modalities in typed lambda calculi. We do so by defining a generic structure of modalities, and show that this structure arises naturally from the structure of intuitionistic logic, and as such finds instances in a wide range of type systems previously described in literature. Despite this generality, this structure has a rich metatheory, which we expose.

Joint work with Andreas Abel.

Fredrik Engström (FLoV) – Dependence logic and generalized quantifiers

Dependence logic, proposed by Väänänen, is an elegant way of introducing dependencies between variables into the object language. The framework of Dependence logic, so-called team semantics, has turned out to be very flexible and allows for interesting generalizations. Instead of considering satisfaction with respect to a single assignment s, team semantics considers sets of assignments X, called teams. While the semantics of Dependence logic is based on the principle that a formula φ is satisfied by a team X if every assignment s ∈ X satisfies φ, we will replace this principle by the following: a formula φ is satisfied by a team X if for every assignment s: s ∈ X iff s satisfies φ, replacing an implication by an equivalence. When only first-order logic is considered nothing exciting happens, it is only when we introduce new logical operations that things start to get more exciting.

Research seminars prior to 2020 are in a separate archive.