Spring Semester FS2025

Unless stated otherwise, all talks will take place in room ExWi 228 of the Exakte Wissenschaft Building (ExWi) at the University of Bern.

Schedule

Abstracts

Unification in logic concerns solving logical equations, where atomic formulas are treated as variables, Boolean connectives as operators, and logical equivalency as equality. Its primary application lies in the study of the admissibility of inference rules.

In this talk, we will first review essential results on unification for intuitionistic logic and classical modal logics and mention some known application of them. Then we will demonstrate the strong connection between uniform interpolation and the notion of projectivity, as elaborated in [1].

[1] Mojtaba Mojtahedi, Konstantinos Papafilippou: Projectivity Meets Uniform Post-Interpolant: Classical and Intuitionistic Logic. AiML 2024: 549-564

Interpretability logic extends provability logic, which is a modal treatment of Gödel's provability predicate. While the basic modality is read as ''it is provable that'' in provability logic, the language of interpretability logic has an additional binary modality, which corresponds to the notion of relative interpretability between first-order arithmetical theories. In recent decades a non-wellfounded proof theory has gained prominence. It results from allowing proofs to have infinite height. In this talk, I will present the wellfounded sequent system GIL and non-wellfounded sequent calculus G∞IL for the interpretability logic IL. Using the method presented in [1] it will also be shown how to get the cut-elimination for these sequent systems. This is a joint work with Borja Sierra Miranda and Thomas Studer.

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

Download the abstract here.

Gödel-Löb provability logic (GL) is a modal logic that formalizes reasoning about provability in Peano Arithmetic. The proof theory of GL is remarkably diverse, with numerous sequent-style proof systems, including a Gentzen system, a non-wellfounded system, a cyclic system, a labeled system, and a nested system. While proof transformations have been defined between the former three systems and between the latter two systems, the question of how to transform proofs from the latter group to the former group has remained an open problem. In this talk, we explore the proof-theoretic landscape of GL and present a solution to this open problem using a novel set of proof transformation techniques. Furthermore, we explain how these transformations lead to the discovery of a new sequent-style system for GL, formulated in terms of linear nested sequents.

After Craig’s seminal results on interpolation theorem, a number and variety of proof-techniques have been designed to establish interpolation theorems. Among them, Maehara’s method is specific due to its applicability to a wide range of logics admitting cut-free complete proof systems.

By reconsidering Maehara’s method, I will how one can extract a “proof-relevant” interpolation theorem for first-order linear-logic stated as follows: if π is a cut-free proof of A⊢B, we can find (i) a formula C in the common vocabulary of A and B and (ii) proofs π1 of A⊢C and π2 of C⊢B such that the proof π′ of A⊢B, obtained by cutting π1 with π2 on C, normalizes to π by cut-reduction. I will carry out this study of proof-relevant interpolation in two frameworks:

Then, I will move to Curien & Herbelin's "duality of computation" framework and prove a computational version of the above result in System L. System L is in Curry-Howard correspondence with sequent proofs allowing to analyze the computational content of Maehara's interpolation can therefore be understood as the factorization of a computation into a term and an evaluation context which interact through an interface-type, the interpolant.

After discussing how the result relates to a proof-relevant refinement of Prawitz’ proof of the interpolation theorem in natural deduction discovered by Čubrić in the 90’s for the simply typed λ-calculus, I will then turn to the question on the requirement needed to carry out this proof-relevant Maehara's method. While Maehara's method relies strongly both on (i) the tree structure of sequent proofs and (ii) their wellfoundedness, I will outline how our method can be extended (i) to proof nets, that are graphs where the order of inference rules has been forgotten, expoiting their correctness criteria, as well as (ii) to circular proofs in logics with fixed-points, where proofs contain cycles and wellfounded of proof objects is relaxed. This last part of the talk is based on joint work with Guido Fiorillo and Daniel Osorio.

A fruitful research programme in the study of residuated lattices has been to take inspiration from results about lattice-ordered groups and extend them to wider classes of residuated lattices. Two important classes for this purpose are the variety of GBL-algebras and its subvariety of GMV-algebras, which significantly extend the variety of lattice-ordered groups while still preserving some group-like behavior. One classical result about ordered groups which has been extended in this way is Hölder’s theorem. This theorem is an abstract characterization of the totally ordered groups which embed into the additive ordered group of reals R as precisely the Archimedean ones (i.e. those which lack infinitesimal elements). In their study of the Archimedean property in residuated lattices, Ledda, Paoli and Tsinakis recently extended Hölder’s theorem to an abstract characterization of algebras which embed either into the reals R, or into the negative cone of the reals R−, or into the standard MV-chain [0, 1] as precisely the so-called strongly simple GBL-algebras. In the present joint work with Luca Spada, we further extend Hölder’s theorem beyond the residuated setting, obtaining an abstract characterization of the dense submonoids of the totally ordered monoids R, R−, and [0, 1].

In this survey we review dynamic epistemic logics with modalities for quantification over information change. Of such logics we present complete axiomatizations, focussing on axioms involving the interaction between knowledge and such quantifiers, we report on their relative expressivity, on decidability and on the complexity of model checking and satisfiability, and on applications. We focus on open problems and new directions for research.

Stepan L. Kuznetsov, joint work with Stanislav Speranski and Tikhon Pshenitsyn
(Steklov Mathematical Institute of RAS)
Kleene iteration (Kleene star) is one of the most interesting algebraic operations used in computer science. Natural examples of structures involving Kleene star, such as algebras of formal languages and algebras of binary relations, are *-continuous, which imposes an infinitary condition on iteration. In the corresponding logical systems, namely, variants of so-called action logic, *-continuity is naturally reflected by infinitary mechanisms such as the omega-rule. In the presence of the omega-rule, proofs may be infinite, but are still required to be well-founded. This gives rise to the notion of closure ordinal, the supremum of (transfinitely measured) heights of proofs in the given calculus. In the talk, we present results on the closure ordinals for fragments of the Horn theory of *-continuous residuated Kleene lattices, and show how they lead to bounds on algorithmic complexity of those theories. Among these bounds, the most interesting is an exact properly hyperaritmetical complexity estimation for the fragment of the aforementioned Horn theory, where the hypotheses are required to be *-free.