Borja Sierra Miranda

Borja Sierra Miranda

he/him

PhD Candidate at the Computer Science Institute of the University of Bern

Publications

You can also find my articles on my Google Scholar profile.

Journal Papers

Cut Elimination for a Non-wellfounded System for the Master Modality Permalink

Published in Journal of Symbolic Logic, 2026

In [10], 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 article 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.

Download Paper

Conference Papers

Knowledge and Common Knowledge of Strategies Permalink

Published in 32nd Workshop on Logic, Language, Information and Computation (to appear), 2026

Most existing work on strategic reasoning simply adopts either an informed or an uninformed semantics. We propose a model where knowledge of strategies can be specified on a fine-grained level. In particular, it is possible to distinguish first-order, higher-order, and common knowledge of strategies. We illustrate the effect of higher-order knowledge of strategies by studying the game Hanabi. Further, we show that common knowledge of strategies is necessary to solve the consensus problem. Finally, we study the decidability of the model checking problem.

Download Paper

Uniform Lyndon Interpolation via Non-wellfounded Proofs Permalink

Published in Advances in Modal Logic, 2026

Non-wellfounded proof theory has been applied to establish uniform interpolation and Lyndon interpolation (separately) for multiple logics. However, it has not yet been used to prove uniform Lyndon interpolation. We close this gap by showing uniform Lyndon interpolation for the provability logic GLS. This logic was known to have uniform interpolation, but it was open whether it has uniform Lyndon interpolation (or at least non-uniform Lyndon interpolation). The methodology we provide is easy to adapt to other provability logics if a non-wellfounded sequent calculus is available for them. In addition, we offer an alternative proof of cut elimination for GLS via non-wellfounded proofs.

Download Paper

Non-wellfounded Proof Theory for Interpretability Logic Permalink

Published in Automated Reasoning with Analytic Tableaux and Related Methods, 2025

We provide a simple cut elimination proof for the interpretability logic of IL. To achieve this, we introduce a traditional Gentzen- style sequent calculus for IL and a non-wellfounded version of it. The non-wellfounded calculus makes it possible to avoid diagonal formulas. Hence, we can give a simple argument based on a general proof-theoretic method for calculi of this kind. Our results provide a useful basis for further research; in particular, they will allow us to establish uniform interpolation for IL.

Download Paper

Coalgebraic Proof Translations for Non-Wellfounded Proofs Permalink

Published in Advances in Modal Logic, 2024

Non-wellfounded proof theory results from allowing proofs of infinite height in proof theory. To guarantee that there is no vicious infinite reasoning, it is usual to add a constraint to the possible infinite paths appearing in a proof. Among these conditions, one of the simplest is enforcing that any infinite path goes through the premise of a rule infinitely often. Systems of this kind appear for modal logics with conversely well-founded frame conditions like GL or Grz.

Download Paper

Cyclic Proofs for iGL via Corecursion Permalink

Published in Proceedings Twelfth Workshop on Fixed Points in Computer Science, 2024

Cyclic proof theory studies proofs where cycles are allowed. This is useful for developing proof theory for logics with fixpoint operators: cycles can be used to represent the unfolding of a fixpoint. However, this cyclic character is not unique to such explicit fixpoints. For example, modal logics whose frames have a Noetherian (conversely wellfounded) condition, such as GL (Goedel-Loeb logic), S4Grz (Grzegorczyk logic) and K4Grz also have cyclic proof systems.

Download Paper

Arxiv Manuscripts

Proof Theory and Interpolation for Sacchetti’s Logics Permalink

Published in ArXiv, 2026

We study the proof theory of Sacchetti’s modal logics, a family of logics generalizing Gödel–Löb provability logic by replacing transitivity with n-transitivity. We make three main contributions. First, we solve an open problem of Iwata by providing an effective cut elimination procedure for Sacchetti’s logics. Second, building on this result, we introduce a new non-wellfounded sequent calculus for this family of logics with an improved subformula property. Third, using this calculus together with interpolation templates, we prove that Sacchetti’s logics have the uniform Lyndon interpolation property, substantially strengthening previous interpolation results for these logics.

Download Paper

Proof Theory for Bimodal Provability Logics Permalink

Published in ArXiv, 2026

We provide the first (non-labelled) sequent calculi for bimodal provability logics with “usual” provability predicates. In particular, we introduce calculi for the logics CS, CSM and ER. Additionally, we present non-wellfounded versions of our calculi, and use them to establish a cut-elimination procedure. Finally, we prove the first interpolation results for these logics showing that they all enjoy the uniform Lyndon interpolation property.

Download Paper

Uniform interpolation for interpretability logic Permalink

Published in ArXiv, 2025

We present a proof-theoretical study of the interpretability logic IL, providing a wellfounded and a non-wellfounded sequent calculus for IL. The non-wellfounded calculus is used to establish a cut elimination argument for both calculi. In addition, we show that the non-wellfounded proof theory of IL is well-behaved, i.e., that cyclic proofs suffice. This makes it possible to prove uniform interpolation for IL. As a corollary we also provide a proof of uniform interpolation for the interpretability logic ILP.

Download Paper

Provability Models Permalink

Published in ArXiv, 2025

In this paper, we study a new Kripke-style semantics for classical modal logic, named as provability models. We study provability models for the propositional modal logics K, K4, S4 GL, GLP and the interpretability logic ILM. Provability models combine features of Kripke models with the assignment of logics to individual worlds. Originally introduced in [Mojtahedi, 2022], these models allowed the first author to establish arithmetical completeness for intuitionistic provability logic. Interestingly, we show that the ILM is complete for the same provability models of GL. We improve provability models to predicative and decidable provability models in the case of GL and ILM. Furthermore, we prove a soundness and completeness of GLP for provability models.

Download Paper

Coalgebraic Proof Translations for Non-Wellfounded Proofs Permalink

Published in ArXiv, 2025

We exhibit a uniform method for obtaining (wellfounded and non-wellfounded) cut-free sequent-style proof systems that are sound and complete for various classes of action algebras, i.e., Kleene algebras enriched with meets and residuals. Our method applies to any class of *-continuous action algebras that is defined, relative to the class of all *-continuous action algebras, by analytic quasiequations. The latter make up an expansive class of conditions encompassing the algebraic analogues of most well-known structural rules. These results are achieved by wedding existing work on non-wellfounded proof theory for action algebras with tools from algebraic proof theory.

Download Paper