Uniform Lyndon interpolation is shown for GLS via non-wellfounded proofs, closing a prior gap and yielding an alternative cut-elimination proof.
Proof Theory for Bimodal Provability Logics
1 Pith paper cite this work. Polarity classification is still indexing.
1
Pith paper citing it
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.
fields
cs.LO 1years
2026 1verdicts
UNVERDICTED 1representative citing papers
citing papers explorer
-
Uniform Lyndon Interpolation via Non-wellfounded Proofs
Uniform Lyndon interpolation is shown for GLS via non-wellfounded proofs, closing a prior gap and yielding an alternative cut-elimination proof.