Proof Theory for Bimodal Provability Logics

TL;DR

This paper introduces sequent calculi for bimodal provability logics, including non-wellfounded variants, and establishes cut-elimination and interpolation properties for these systems.

Contribution

It provides the first non-labelled sequent calculi for bimodal provability logics with provability predicates and proves key properties like cut-elimination and interpolation.

Findings

Established cut-elimination procedures for the calculi.

Proved the uniform Lyndon interpolation property for the logics.

Introduced non-wellfounded versions of the calculi.

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.