Proof Theory for Bimodal Provability Logics
Logic
2026-05-15 v2
Abstract
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.
Cite
@article{arxiv.2605.12351,
title = {Proof Theory for Bimodal Provability Logics},
author = {Borja Sierra Miranda and Thomas Studer},
journal= {arXiv preprint arXiv:2605.12351},
year = {2026}
}