arXiv subjects

Borja Sierra Miranda

Publications and source records attributed to Borja Sierra Miranda.

10 recordsLinked to original sources

arXiv2026

Proof Theory and Interpolation for Sacchetti's Logics

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.

math.LO↗

arXiv2026

Uniform Lyndon Interpolation via Non-wellfounded Proofs

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.

cs.LO↗

arXiv2026

Proof Theory for Bimodal Provability Logics

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.

math.LO↗

arXiv2025

Provability Models

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.

math.LO↗

arXiv2025

Cyclic Proofs for iGL via Corecursion

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. Particularly, Shamkanov introduces a non-wellfounded and a cyclic sequent system GL. He proves the equivalence of these two systems with an acyclic finite system via proof translations. In order to go from the finite system to the non-wellfounded system he defines the translation by corecursion. Iemhoff generalized the work of Shamkanov studying when, for a given modal logic proof system, there exists another modal logic proof system such that proofs in the first are equivalent to cyclic proofs in the second. There, she shows that iGL, an intuitionistic version of GL, also has a natural cyclic proof system. We provide an alternative proof of the equivalence of a standard calculus for iGL and a cyclic one.

math.LO↗

arXiv2025

Cut elimination for a non-wellfounded system for the master modality

In previous work 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 the non-wellfounded character of proofs. We will employ the method to obtain syntactic cut elimination for $K^+$, a system of modal logic with the master modality.

math.LO↗

arXiv2025

Uniform interpolation for interpretability logic

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.

math.LO↗

arXiv2025

Knowledge and Common Knowledge of Strategies

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.

cs.LO↗

arXiv2025

Coalgebraic proof translations for non-wellfounded proofs

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. In this paper, we provide a uniform method to define proof translations for such systems, guaranteeing that the condition on infinite paths is preserved. In addition, as particular instance of our method, we establish cut-elimination for a non-wellfounded system of the logic Grz. Our proof relies only on the categorical definition of corecursion via coalgebras, while an earlier proof by Savateev and Shamkanov uses ultrametric spaces and a corresponding fixed point theorem.

math.LO↗

arXiv2025

Algebraic Proof Theory for Infinitary Action Logic

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.

cs.LO↗