The announcements are posted to a seminar mailing list. All people interested in the seminar and not belonging yet to the list can send an e-mail to "sara dot negri at helsinki dot fi" to be included among the recipients.

The research seminar in logic is primarily intended for the presentation of original research in logic and philosophy of mathematics by junior and senior researchers and by international guests. The detailed schedule of the seminar, with titles and abstracts of the presentations will be posted on this web page (see below).

Credits are acquired through regular attendance, active participation in the discussions and, when possible, a presentation at the seminar. The presentation can be based either on existing literature, to be agreed with the docent, or on original research.

Please cf. Web Oodi for the registration and a description of the learning goals in Finnish.

16.11.2018: Sara Negri ``Constructivizing classical reasoning: A simple proof of Barr's theorem for infinitary geometric logic''.

Abstract: Geometric logic has gained considerable interest in recent years: contributions and applications areas include structural proof theory, category theory, constructive mathematics, modal and non-classical logics, automated deduction, and even Kantian philosophy. Geometric logic studies the so-called geometric or coherent theories, i.e. first-order theories axiomatized by geometric or coherent implications. Several mathematical theories--such as the theory of torsion abelian groups, of Archimedean ordered fields, and of connected graphs--are axiomatized by infinitary geometric implications. Also notions such as the transitive closure of accessibility relations, essential in the semantical analysis of aggregation of epistemic attitudes, are expressed in infinitary geometric logic. Proof analysis is extended to all such theories by augmenting an infinitary classical sequent calculus with a rule scheme for infinitary geometric implications. The calculus is designed in such a way as to have all the rules invertible and all the structural rules (weakening, contraction, and cut) admissible. An intuitionistic infinitary multisuccedent sequent calculus is also introduced and it is shown to enjoy the same structural properties. Finally, it is shown that by bringing the classical and intuitionistic calculi close together, the infinitary Barr theorem becomes an immediate result. [This talk is based on joint work with the late Roy Dyckhoff]

2.11.2018: Annika Kanckos: ``Gödel's Koan´´.

Abstract: The problem named Gödel's Koan asks for an easy ordinal assignment showing termination of arbitrary $\beta$-reductions in Simply typed lambda calculus. This is equivalent to showing strong normalization for the implicational fragment of predicate logic. However, easy is not enough, the logic community demands an assignment of natural numbers instead of infinite ordinals. In this talk I will suggest a solution to this problem based on a submitted paper. The solution also extends to a ordinal assignment for terms of Gödel's T.

12.10.2018: Jan von Plato: ``Gödel's "Resultate Grundlagen" notebooks: a first look''.

Summary: At the time when Gödel left formal work in logic and foundations, by early 1943, he composed a set of four notebooks with continuous pagination 1-368 and a continuous numbering of theorems 1-87. These notebooks are a summary of finished work that remained unpublished, a legacy to be. They are eminently readable, modulo the archaic shorthand, with close to no cancellations or hesitation, and a good coverage that makes them largely self-contained for a trained reader.

21.9.2018: Andreas Fjellstad: Eliminating cuts on atomic formulas

In the recent paper "Restricting initial sequents: The trade-offs between identity, contraction and cut", Peter Schröder-Heister presents a sketch of a cut-elimination proof for a sequent calculus with left- and right introduction rules for one or more atomic formulas in which the active formulas may be complex formulas, but where the initial sequents are restricted to identity for the atomic formulas for which there are no left- and right introduction rules.

Given the relevance of the proof strategy for my own research, the aim of the seminar is to work out the missing details of the proof in a hands-on fashion, and then, if we do not find any errors, investigate whether it can be applied to the sequent calculus obtained by including as initial sequents identity for every atomic formula.

7.9.2018: Tarmo Uustalu (Reykjavik University): The sequent calculus of skew monoidal categories

Szlach\'anyi's skew monoidal categories from 2012 are a recent, but well-motivated variation of monoidal categories, studied by several groups of people currently. In a skew monoidal category, the unitors and associator need not be natural isomorphisms, only natural transformations in a particular direction. This talk is about skew monoidal categories from the viewpoint of structural proof theory *only*. The free skew monoidal category over a set of generating objects can be viewed as a proof system. We are interested in sequent calculus reformulations of this proof system. The main sequent calculus we introduce and study is similar to that of intuitionistic multiplicative noncommutative linear logic (corresponding to the free monoidal category), but antecedents are made of a stoup (an optional formula) and a passive context (a list of formulae). The left rules only apply in the stoup, and the stoup formula of the conclusion of and $\otimes$-right rule application must be taken from the 1st premise. We show admissibility of two forms of cut (stoup cut and context cut) and prove the sequent calculus sound and complete wrt. existence of maps in the free skew monoidal category. We further introduce an equivalence relation on sequent calculus derivations and prove that there is a bijection between equivalence classes of derivations and maps in the free skew monoidal category. We also identify a subcalculus of focused derivations and establish that it contains exactly one canonical representative from each equivalence class. Root-first proof search in the focussed sequent calculus then gives us simple algorithms both for deciding equality of maps in the free skew monoidal category and for enumerating any homset without duplicates, in particular, for deciding whether there is a map. We have fully formalized this development in the dependently typed programming language Agda. This is joint work with Niccolò Veltri (ITU Copenhagen) and Noam Zeilberger (University of Birmingham).

* Last updated September 2018 *