{"id":"arxiv/2607.06359","url":"https://arxiv.org/abs/2607.06359","tags":["math.LO"],"score":0,"title":"Proof Theory and Interpolation for Sacchetti's Logics","domain":"math.LO","source":"arxiv","authors":["Borja Sierra Miranda","Thomas Studer"],"reviews":0,"subject":"math.LO","summary":"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…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-07-07","reactions":{}}