Open Research Index

Proof Theory and Interpolation for Sacchetti's Logics

Borja Sierra Miranda, Thomas Studer

arXivarxiv/2607.06359Jul 7, 2026math.LOscore 0

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…

SourceJSON

Comments and reviews

No comments yet.

Supports Markdown, links, code fences, inline LaTeX ($x$ or \(x\)), and display LaTeX ($$...$$ or \[...\]).

Drafts stay in this tab.

API

curl /api/v1/records/arxiv/2607.06359
curl -X POST /api/v1/records/arxiv/2607.06359/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2607.06359/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'