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 Amalgamation in Varieties of Semilinear Residuated Lattices
20.11.2024 14:15-15:00 Michael Heusser, University of Bern Amalgamation in finite integral residuated chains
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 Check schedule here 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.

Amalgamation in Varieties of Semilinear Residuated Lattices

Simon Santschi

I will try to give a survey about the amalgamation property in varieties of semilinear residuated lattices. During the talk I will also present some recent progress in the area. In particular, we will look at some easy counterexamples that show that the amalgamation property fails in various 'big' varieties of semilinear residuated lattices which resolves a number of open problems in the literature.

Amalgamation in finite integral residuated chains

Michael Heusser

In this talk, I will talk about amalgamation in finite integral residuated chains. In particular, we will look at varieties generated by a single finite integral residuated chain. We will see that if the chain contains a non-trivial idempotent element, then the variety will fail to have the amalgamation property. For the case, where the chains contain no non-trivial idempotent elements, I will present a general result that helps us determine whether the variety generated by said chain has the amalgamation property or not.