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

Abstracts

A local progress calculus is a non-wellfounded sequent calculus where the premises of some rules are marked as progress. Then, we allow non-wellfounded proofs whose infinite branches we move to progressing premises infinitely often. In previous work [1], we introduced a method to define proof translations among theses systems. A natural extension of these class of calculi is progress-reset calculus, where the premises some rules make progress but the premises of other rules reset all the progress we had constructed.

In the present talk we will describe a possible extension to the method of translations in local progress calculi to progress-reset proof systems. The main idea is to "slice" a progress-reset calculus into infinitely many local progress calculi, each of them with an assigned ordinal. Then, a proof in the progress-reset calculus can be understood as a proof in one of these local progress calculi with some open assumptions. However, the open assumptions come with a "proof witness" in a lower ordinal local progress calculus that guarantees their provability. We hope that this extension of the method allows to perform cut elimination in progress-reset systems, again having a simple method that closely resembles finitary proof theory.

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

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.

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.

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.

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.

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. 

The algebraic approach to constraint satisfaction problems (CSPs) has in recent years inspired several novel strands of interrogation within the research field of universal algebra. The proofs of Feder’s and Vardi’s dichotomy conjecture for finite-domain CSPs, independently provided by Bulatov and Zhuk, exhibit that equational non-triviality of an associated polymorphism algebra serves as the exact borderline between tractability and hardness. The well-known charac- terisation of equational non-triviality for finite idempotent algebras by means of Taylor-terms has been extended through several descriptions that rely on speci- fic non-trivial systems of identities independent of the given algebraic structure. Following this line of enquiry, I will in this talk systematically examine symme- tric identities that are weak enough to fully capture equational non-triviality of finite idempotent algebras.
Based on joint work with Michael Pinsker and Dmitriy Zhuk.

In many formal frameworks for the verification of reactive systems, computations are represented as execution traces—words over alphabets of ‘structured states’ derived from high-level specifications, such as automata or LTSs. This approach enables the description of several important system policies in terms of trace properties (sets of execution traces) and provides a natural way of classifying them according to the well-known safety/liveness dichotomy. Classical trace-based modelling techniques use infinite traces to abstract system behaviours. However, as demonstrated by results from applied research, system analysis based on finite traces is supported by some compelling reasons (e.g., a proper treatment of terminating computations). In this context, safety and liveness can be defined in terms of prefix-closure operators over residuated partially ordered monoids, which arise as powersets of free monoids of traces. My aim in this talk is to show that properties of finite executions can be systematically studied through modal extensions of the associative Lambek calculus, where the additional operators are defined in terms of the prefix relation (left-divisibility). I examine four such extensions, obtained by augmenting the base language with residuated, dually residuated, Galois-connected, and dually Galois-connected pairs of unary modalities. Some variants of these calculi have been introduced in mathematical linguistics to study and relate different forms of syntactic composition in natural languages. For each logic, I provide and compare Gentzen- and Szabo-style presentations. Finally, using category-theoretic arguments, I propose a strategy to prove completeness theorems with respect to some classes of expanded free semigroup models.