arXiv · 2607.06359
Proof Theory and Interpolation for Sacchetti's Logics
Abstract
We study the proof theory of Sacchetti's modal logics, a family of logics generalizing G\"odel--L\"ob 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.
Explore related subjects
Keep this discovery
Borja Sierra Miranda, Thomas Studer. 2026-07-07. Proof Theory and Interpolation for Sacchetti's Logics. https://arxiv.org/abs/2607.06359
Cite the original work for its findings. Save a collection to share your selection of sources.