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