Seminars

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.

Spring 2021

Lindström Lecture
Sara Negri (University of Genoa) – On modal embeddings

Motivated by the difficulty in proving faithfulness of various modal embeddings (starting with Gödel’s translation of intuitionistic logic into S4), we use labelled calculi to obtain simple and uniform faithfulness proofs for the embedding of intermediate logics into their modal companions, and of intuitionistic logic into provability logic, including extensions to infinitary logics.


Lindström Lecture
Sara Negri (University of Genoa) – Syntax and semantics in synergy

Syntax and semantics, often considered as conflicting aspects of logic, have turned out to be intertwined in a methodology for generating complete proof systems for wide families of non-classical logics. In this formal semantics, models can be considered as purely mathematical objects with no ontological assumptions upon them. More specifically, by the “labelled formalism”, which now is a well-developed methodology, the semantics is turned into an essential component in the syntax of logical calculi. Thus enriched, the calculi not only constitute a tool for the automatisation of reasoning, but can also be used at the meta-level to establish general structural properties of logical systems and direct proofs of completeness up to decidability in the terminating case. The calculi, on the other hand, can be used to find simplified models through conservativity results. The method will be illustrated with gradually generalised semantics, including topological ones such as neighbourhood semantics.


Mauricio Martel (CSE, GU) – On the Complexity of Conservative Extensions in the Two-Variable Guarded Fragment

Conservative extensions are a fundamental notion in logic. In the area of description logic, deciding whether a logical theory is a conservative extension of another theory is a fundamental reasoning problem with applications in ontology engineering tasks, such as ontology modularity, ontology reuse and ontology versioning. It has been observed in recent years that conservative extensions are decidable in many modal and description logics, given that they can often be characterized elegantly in terms of appropriate notions of bisimulations. But no work has been done for more expressive logics such as the two-variable fragment and the guarded fragment, which are considered to be generalizations of modal and description logics, and are typically used to explain their good computational behavior.

In this talk, I attempt to fill this gap by considering the decidability of conservative extensions in the two-variable guarded fragment (gfo2). I will show that conservative extensions are decidable in gfo2 and that the computational complexity is 2exptime-complete. To prove these results I will rely on an automata-based approach, which consists in first giving a model-theoretic characterization of conservative extensions in terms of guarded bisimulations, to then use it as a foundation for a decision procedure based on tree automata. Since the usual notion of guarded bisimulations fail to characterize conservative extensions in gfo2, I will report on alternative model-theoretic characterizations in terms of bounded guarded bisimulations and the challenge of combining them with automata techniques.

This talk is based on joint work with Carsten Lutz, Jean Christoph Jung, Thomas Schneider, and Frank Wolter: https://drops.dagstuhl.de/opus/volltexte/2017/7464/pdf/LIPIcs-ICALP-2017-108.pdf


Nordic Online Logic Seminar
Øystein Linnebo (University of Oslo) – Potentialism in the philosophy and foundations of mathematics

Aristotle famously claimed that the only coherent form of infinity is potential, not actual. However many objects there are, it is possible for there to be yet more; but it is impossible for there in fact to be infinitely many objects. Although this view was superseded by Cantor’s transfinite set theory, even Cantor regarded the collection of all sets as “unfinished” or incapable of “being together”. In recent years, there has been a revival of interest in potentialist approaches to the philosophy and foundations of mathematics. The lecture provides a survey of such approaches, covering both technical results and associated philosophical views, as these emerge both in published work and in work in progress.

This talk is part of the Nordic Online Logic Seminar.

Daichi Hayashi (Hokkaido University) – Universes for the supervaluational theory of Frege structure

In constructive type theory and explicit mathematics, the idea of universes has been used to strengthen the expressive power or the proof-theoretic strength of a given system. Similarly, Cantini (1996) and Kahle (2003) introduced universes for axiomatic truth theories over TON (total applicative theory). Set-theoretic universes are usually large sets that are closed under several operations like complements, whereas truth-theoretic universes can be seen as quasi-truth predicates which satisfy some axioms for the truth predicate. Cantini and Kahle then showed that by adding the axiom assuring the existence of universes, several truth theories become proof-theoretically stronger.

In this talk, I will formulate the theory VFU, an extension of Cantini’s supervaluational truth theory VF (cf. Kahle, 2002) with the universe-generating axiom, and then prove that VFU has the same proof-theoretic strength as KPi (Kripke-Platek set theory with the recursively inaccessible universe) and T0 (Feferman’s explicit mathematics with the inductive generation axiom). To determine the lower bound, I show that T0 is relatively interpretable in VFU. As for the upper bound, I give a truth-as-provability interpretation for VFU, where the truth predicate is understood as the provability in a certain infinite derivation system. As this is formalisable in KPi, a relative interpretation of VFU in KPi is obtained. Therefore, all the three systems are proof-theoretically equivalent. Finally, I would like to mention the possibility of constructing natural numbers in VFU.


Rasmus Blanck (FLoV) – Never trust an unsound theory

What is a Gödel sentence? Is there such a thing as the Gödel sentence of a given theory?

Lajevardi and Salehi, in a short paper from last year, argue against the use of the definite article in the expression ‘the Gödel sentence’, by claiming that any unsound theory has Gödelian sentences with different truth values. We show that the two theorems of their paper are special cases (modulo Löb’s theorem and the first incompleteness theorem) of general observations pertaining to fixed points of any formula, and argue that the false sentences of Lajevardi and Salehi are in fact not Gödel sentences. We conclude with a discussion of the roles played by soundness and truth in drawing further consequences from the incompleteness theorems.

This paper on which this talk is based is joint work with Christian Bennet.


Nordic Online Logic Seminar
Michael Rathjen (University of Leeds) – Completeness: Turing, Schütte, Feferman (and Löb)

Progressions of theories along paths through Kleene’s Omega adding the consistency of the previous theory at every successor step, can deduce every true \(\Pi^0_1\)-statement. This was shown by Turing in his 1938 thesis who called these progressions “ordinal logics”. In 1962 Feferman proved the amazing theorem that progressions based on the “uniform reflection principle” can deduce every true arithmetic statement. In contrast to Turing’s, Feferman’s proof is very complicated, involving several cunning applications of self-reference via the recursion theorem. Using Schütte’s method of search trees (or decomposition trees) for omega-logic and reflexive induction, however, one can give a rather transparent proof.

This talk is part of the Nordic Online Logic Seminar.

Paul Gorbow (Stockholm University and University of Oslo) – A solution to the knower paradoxes with applications to common knowledge and iterated knowledge

I present an untyped theory of knowledge and truth that solves the knower paradoxes of Kaplan and Montague from the 1960’s. The underlying idea is (1) to formalize the principle of veracity (that whatever is known is true) more precisely, and (2) to embrace self-reference in the spirit of the Friedman-Sheard theory of truth and its associated revision semantics. It turns out that this facilitates expedient reasoning with common-knowledge predicates defined by self-referential formulas obtained by Gödel diagonalization. Moreover, the revision semantics is generalized to accommodate my theory. Apart from answering questions of consistency, this opens up for philosophical insights on the meaning of sentences involving iterations of knowledge and truth, such as ‘“Kim knows A” is true’ and ‘Kim knows “Kim knows A”’.


Nordic Online Logic Seminar
Juliette Kennedy (University of Helsinki) – Reading syntax off semantics

The practice of foundations of mathematics is built around a firm distinction between syntax and semantics. But how stable is this distinction, and is it always the case that semantically presented mathematical objects in the form e.g. of a model class might give rise to a “natural logic”? In this talk I will investigate different scenarios from set and model theory in which an investigation of the notion of an implicit or internal logic or syntax becomes possible. Time permitting we will also discuss the question whether logics without a syntax can be considered logics at all.

This talk is part of the Nordic Online Logic Seminar.

Abhishek De (IRIF) – The proof theory of substructural logics with fixed points

Substructural logics are logics with restricted use of structural rules like weakening, contraction and exchange. There are several motivations for investigating substructural logics from the study of algebraic structures like residuated (semi)lattices to the study of type systems which allow for greater control over the number of times and the order in which variables are used.

Enriched with fixed point operators, these logics are highly expressive. In this talk, I will give a brief overview of substructural logics with fixed points and concentrate specifically on linear logic with fixed points discussing various proof systems, their expressivity, and semantics.


Marianna Girlando (University of Birmingham) – Cyclic hypersequents for Transitive Closure Logic

Transitive Closure Logic (TCL) enriches the language of first order logic with a recursive operator, expressing the transitive closure of a binary relation. Cyclic sequent calculi proofs for this logic have been introduced in the literature. In this talk, I will present a new cyclic proof system for TCL, which employs hypersequents. The main motivation behind this work is that, differently from sequent TCL proofs, hypersequent proofs for TCL successfully simulate cyclic proofs in the transitive fragment of Propositional Dynamic Logic (PDL+), without using the non-analytic rule of cut.

After introducing the cyclic hypersequent calculus for TCL, I will present two main results. First, I will sketch a proof of soundness for the calculus, which requires a more involved argument than the one used in traditional cyclic proofs. Second, I will show how PDL+ cyclic proofs can be translated into TCL hypersequent proofs. This result allows to lift the completeness result for cyclic PDL+ to the hypersequent calculus. This talk is based on joint work with Anupam Das.


Nordic Online Logic Seminar
Thierry Coquand (Gothenburg University) – Formalization of Mathematics and Dependent Type Theory

The first part will be about representation of mathematics on a computer. Questions that arise there are naturally reminiscent of issues that arise when teaching formal proofs in a basic logic course, e.g. how to deal with free and bound variables, and instantiation rules. As discussed in a 1962 paper of Tarski, these issues are “clearly experienced both in teaching an elementary course in mathematical logic and in formalizing the syntax of predicate logic for some theoretical purposes.” I will present two quite different approaches to this problem: one inspired by Tarski’s paper (N. Megill, system Metamath) and one using dependent type theory (N.G. de Bruijn).

The second part will then try to explain how notations introduced by dependent type theory suggest new insights for old questions coming from Principia Mathematica (extensionality, reducibility axiom) through the notion of universe, introduced by Grothendieck for representing category theory in set theory, and introduced in dependent type theory by P. Martin-Löf.

This talk is part of the Nordic Online Logic Seminar.

Sebastian Enqvist (Stockholm University) – Cyclic proofs for the first-order μ-calculus

Josephine Dik (FLoV) – The Proof Theory of Description Logic

Description Logics (DLs) are a family of knowledge representation languages, used to reason with information sets in a structured and well-understood way. They play a big role in any field using large amounts of data, e.g. artificial intelligence, databases, and they are of importance in providing a logical formalism for ontologies and the Semantic Web. A common battle in the world of DLs is the one between expressivity, where we add fixpoints, inverses, role restrictions, etc, to a standard DL, and decidability. That is why more expressive as well as light-weight DLs are considered, which both benefit from different derivation system. In this talk I will first give an introduction on the general area of Description Logic, and then focus on the different reasoning problems and how they are solved proof-theoretically. The main result will be on Martin Hofmann’s paper, presenting the sequent calculus for the light description logic EL with the fixpoint extension, and see how cyclic proofs are used in this context. This talk is based on the reading course I did together with Bahareh Afshari as a preparation for my Master thesis.


Nordic Online Logic Seminar
Johan van Benthem (University of Amsterdam, Stanford University, and Tsinghua University) – Interleaving Logic and Counting

Reasoning with generalized quantifiers in natural language combines logical and arithmetical features, transcending divides between qualitative and quantitative. This practice blends with inference patterns in ‘grassroots mathematics’ such as pigeon-hole principles. Our topic is this cooperation of logic and counting on a par, studied with small systems and gradually moving upward. We start with monadic first-order logic with counting. We provide normal forms that allow for axiomatization, determine which arithmetical notions are definable, and conversely, discuss which logical notions and reasoning principles can be defined out of arithmetical ones. Next we study a series of strengthenings in the same style, including second-order versions, systems with multiple counting, and a new modal logic with counting. As a complement to our fragment approach, we also discuss another way of controlling complexity: changing the semantics of counting to reason about ‘mass’ or other aggregating notions than cardinalities. Finally, we return to the basic reasoning practices that lie embedded in natural language, confronting our formal systems with linguistic quantifier vocabulary, monotonicity reasoning, and procedural semantics via semantic automata. We conclude with some pointers to further entanglements of logic and counting in the metamathematics of formal systems, the philosophy of logic, and cognitive psychology. (Joint work with Thomas Icard)

Paper available at: https://eprints.illc.uva.nl/id/eprint/1813/1/Logic.Counting.pdf

This talk is part of the Nordic Online Logic Seminar.

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 iris-project.org 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.

References

[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.

References:

  • 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 https://www.researchgate.net/publication/353496287_Axiomatizations_of_Peano_Arithmetic_A_truth-theoretic_view

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).

References:

  • 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.

References

[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.