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.