Uniform Lyndon Interpolation via Non-wellfounded Proofs
For logicians studying provability logics, this work closes an open problem by establishing uniform Lyndon interpolation for GLS, and offers a methodology adaptable to other logics with non-wellfounded sequent calculi.
The paper proves uniform Lyndon interpolation for the provability logic GLS, which was previously known to have uniform interpolation but not uniform Lyndon interpolation. It also provides an alternative proof of cut elimination for GLS via non-wellfounded proofs.
Non-wellfounded proof theory has been applied to establish uniform interpolation and Lyndon interpolation (separately) for multiple logics. However, it has not yet been used to prove uniform Lyndon interpolation. We close this gap by showing uniform Lyndon interpolation for the provability logic GLS. This logic was known to have uniform interpolation, but it was open whether it has uniform Lyndon interpolation (or at least non-uniform Lyndon interpolation). The methodology we provide is easy to adapt to other provability logics if a non-wellfounded sequent calculus is available for them. In addition, we offer an alternative proof of cut elimination for GLS via non-wellfounded proofs.