Autumn Semester HS2024

Unless stated otherwise, all talks will take place in room ExWi 228 of the Exakte Wissenschaft Building (ExWi) at the University of Bern.
Please note that the seminar room has changed with respect to previous years.

Schedule

Date Time Speaker Title
25.09.2024 14:00-15:00 Borja Sierra Miranda, University of Bern Cut elimination for non-wellfounded master modality
02.10.2024 14:00-15:00 George Metcalfe, University of Bern Substructural logics with minimally true tautologies
09.10.2024 14:00-15:00 Jim de Groot, University of Bern Intuitionistic modal logics between CK and IK
16.10.2024 14:00-15:00 Jean-Yves Beziau, University of Brazil - Rio de Janeiro Sequent Calculus, Truth and Proof
13.11.2024 14:00-15:00 Simon Santschi, University of Bern TBA
20.11.2024 14:15-15:00 Michael Heusser, University of Bern TBA
04.12.2024 14:00-18:00 Elisabeth Bouscaren, Rosario Mennuni SGSLPS Winter Meeting - Model Theory (Location: EPFL at Lausanne)
11.12.2024 14:00-15:00 Johanna Brunar - TU Wien (Room Change: Bern Neubrückstrasse 10, Floor 3, Room 302)
13.12.2024 14:00-18:00 TBA Swiss Logic Gathering (Location: ExWi 228)
18.12.2024 14:00-15:00 Ludovico Fusco, University of Urbino TBA

Abstracts

Cut elimination for non-wellfounded master modality

Borja Sierra Miranda

In [1], we provided a method for eliminating cuts in non-wellfounded proofs with a local-progress condition, these being the simplest kind of non-wellfounded proofs. The method consisted of splitting the proof into nicely behaved fragments. This paper extends our method to proofs based on simple trace conditions. The main idea is to split the system with the trace condition into infinitely many local-progress calculi that together are equivalent to the original trace-based system. This provides a cut-elimination method using only basic tools of structural proof theory and corecursion, which is needed due to working in a non-wellfounded setting. We will employ our method to obtain syntactic cut-elimination for K+, a system of modal logic with the master modality.

[1]: Borja Sierra Miranda, Thomas Studer and Lukas Zenger. "Coalgebraic Proof Translations of Non-Wellfounded Proofs". In Agata Ciabattoni, David Gabelaia and Igor Sedlár (eds). (2024) Advances in Modal Logic, Vol. 15. College Publications.

Substructural logics with minimally true tautologies

George Metcalfe

The tautologies of propositional classical logic are always interpreted by the same (greatest) element in a Boolean algebra, but such uniformity is typically lacking in "weakening-free" substructural logics. In particular, a tautology "A implies A" may be mapped to a value in a structure for the logic that is strictly greater than the element t representing minimal truth; that is, "A implies A" is a tautology of the logic, but it is not the case that "A implies A" is equivalent to t. Several weakening-free substructural logics may be found in the literature, however, that have “minimally true” tautologies: notably, the logics of Iseki’s BCI-algebras and Raftery and van Alten’s sircomonoids, and the comparative logics of Casari, including Abelian logic, introduced independently by Meyer and Slaney. In this talk, based on a joint paper with José Gil-Férez and Frederik Lauridsen [1], I will explain how proof theory and decidability results can be obtained for these logics by adding a restricted form of weakening, justified by a Glivenko-style property, to suitable sequent calculi.

Intuitionistic modal logics between CK and IK

Jim de Groot

The fusion of intuitionistic and modal logic has led to a wide variety of intuitionistic modal logics. For example, the intuitionistic modal logics between Constructive K (CK) and Intuitionistic K (IK) differ in their treatment of the possibility (diamond) connective. It was recently rediscovered that some logics between CK and IK also disagree on their diamond-free fragments.
In this talk I will recall various intuitionistic modal logics, and describe a semantic approach to comparing their diamond-free fragments. This allows us to answer open questions about the (non-)conservativity of such logics over the basic intuitionistic modal logic without diamond.

Sequent Calculus, Truth and Proof

Jean-Yves Beziau

In this lecture, I explain the conditions under which the intuitive semantic interpretation of sequent rules, given by Gerhard Gentzen himself, applies. It is a general completeness theorem based on some abstract notions in the spirit of universal logic, involving in particular an abstract form of the Lindenbaum extension lemma. This theorem has applications to many systems of logic, in particular systems having no truth functional semantics or being non self-extensional.