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