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.
5.4.2019: Maria Hämeen-Anttila "Gödel on proofs, computations, and constructivity"
Abstract: In 1941, Kurt Gödel presented his functional interpretation of Heyting Arithmetic as a more constructive alternative to the BHK (Brouwer-Heyting-Kolmogorov) interpretation, which explains the meaning of logical operations in terms of their provability conditions. The crucial step was to generalise the notion of a function to that of a finite-typed function, an object that is not obviously constructive in the strict sense of the word, and it has later been argued that Gödel's concept of a functional shares the same weaknesses as the intuitionistic concept of proof. In my presentation, I will sketch a historical picture of the development of Gödel's functional interpretation and discuss his views on the constructivity question in the light of his 1941 notes.
15.3.2019: Annika Kanckos (joint work with Tim Lethen) "The Development of Gödel’s Ontological Proof"
Abstract: A formal ontological proof of the existence of God proves that necessarily God exists from a set of defined axioms. Gödel's ontological proof is by now well-known based on the 1970-version, written in Gödel's own hand, and Scott’s version of the proof. In this talk new manuscript sources found in Gödel’s Nachlass are presen\ ted. Three versions of Gödel's ontological proof have been transcribed, and comp\ leted from context as true to Gödel’s notes as possible. The discussion is based\ on these new sources and reveals Gödel’s early intensions of a liberal comprehe\ nsion principle for the higher order modal logic, an explicit use of second order Bar\ can schemas, as well as seemingly defining a rigidity condition for the system. None \ of these aspects occur explicitly in the later 1970 version, and therefore they have \ long been in focus of the debate on Gödel's ontological proof. The ontological p\ roof is an 'exercise in modal logic' that does not explicitly require belief in God, \ but only a conviction that modality matters.
Peter Schuster, Università di Verona "Krull’s Lemma: From Induction to Conservation\ ".
Abstract: The semantic Universal Krull Lemma (UKL) subsumes many a transfinite \ proof method in algebra [Rinaldi-Sch. JPAA 2016] which is usually justified by Zorn's\ Lemma. Typically such a proof method is a reduction to a special case characterised \ by additional axioms with disjunctions in positive position. For proving theorems of \ concrete character, however, the syntactical conservation principle (Con) correspondi\ ng to UKL is equally applicable, and Con moreover is of entirely finite nature [Rinal\ di-Sch.-Wessel BSL 2017 & Indag.Math. 2018]. While UKL entails Con without further ad\ o, the computation using Con that is the core of an inductive proof of UKL is in fact\ equivalent to Con. This adds evidence to Con being the very computational content of\ UKL.
15.2.2019: Edi Pavlovic ''Sequent calculi for logics of agency: the deliberative STIT''
Abstract: We develop a system of labelled sequent calculus for the deliberative see-to-it-that (Dstit) modality. Dstit is an agentive modality usually semantically defined on a tree-like structure of successive moments. The sequence of moments forms histories, with individual moments parts of different histories, but all histories sharing some moment. The tree has forward-branching time (BT), and thus indeterminacy of the future but no backward branching, and is enriched by agent choice (AC). Choice is a function mapping agent/moment pairs to a partition of all histories passing through that moment (since an agent’s choice determines what history comes about only to an extent). In such (BT+AC) frames, formulas are evaluated at moments in histories. Specifically, an agent a seeing to it that A holds at the moment m of a history h iff (i) A holds in all histories choice-equivalent to h for the agent a, but (ii) doesn’t hold in at least one history that m is a part of. In simple terms, the agent sees to it that A if their choice brings about those histories where A holds, but nonetheless it could have been otherwise (i.e. an agent can’t bring about something that would have happened anyway). Stit modalities, including Dstit, received an extensive axiomatic treatment in (Belnap et al. 2001), and the proof-theoretic approaches to it so far have been done via labelled tableaux (Wansing 2006, Olkhovikov and Wansing 2018). In contrast, in this paper (joint work with Sara Negri) we investigate Dstit modality by means of a sequent calculus. Following (Negri and von Plato 2001, 2011), we employ the axioms-as-rules approach, and develop a G3-style labelled sequent calculus. This is shown to possess all the desired structural properties of a good proof system, including being contraction- and cut-free. Moreover, we demonstrate multiple applications of the system. We prove the impossibility of delegation of tasks among independent agents, the interdefinability of Dstit with agent-relative modality 'cstit' and agent-independent modality 'settled true', as well as the treatment of refraining from (Belnap et al. 2001) and (von Wright 1963). Finally, we demonstrate the meta-theoretical properties of our system, namely soundness, completeness and decidability via a bounded proof search.
25.1.2019: Anssi Yli-Jyrä ``Robust Generalizations of String Automata''
Abstract: In this talk, I will talk about the problem of extending finite string automata and MSO to nonclassical structures, saslos (structure augmented string-like objects), without losing the good characteristics of string automata.
23.11.2018: Eugenio Orlandelli ``Interpolation in extensions of first-order logic''.
Abstract: Interpolation is a central result in first-order logic. The aim of this paper is to extend interpolation beyond first-order logic. In particular, we show how to prove interpolation in Gentzen's sequent calculi with singular geometric rules, a special case of geometric rules. Interestingly, singular geometric rules include the rules for first-order logic with identity (as well as those for the theory of strict partial orders and other order theories). Thus, from interpolation for singular geometric rules, we obtain a direct proof of interpolation for first-order logic with identity, while the existing techniques are based on indirect maneuvers such as the reduction to the case of pure first-order logic. Finally, we consider singular geometric theories over intuitionistic first-order logic (joint with G. Gherardi & P. Maffezioli).
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