Cut elimination for provability logic. An unmechanized proof.
Ricardo Jaimes-Urbán
Authors: Ricardo Jaimes-Urbán and Favio E. Miranda-Perea
In 2015, Brighton proved the cut elimination theorem for provability logic using regress trees [1]. Six years later, Goré, Ramanayake and Shillito pointed out that Brighton’s proof is indirect and has some technical problems and presented a computer assisted proof (CAP), for the sequent calculus GLS, using the Coq proof assistant [2]. To achieve this, they defined an auxiliary sequent calculus (PSGLS) wich has a terminating proof search procedure.
Even though CAPs have became more popular lately, they are not universally accepted. Thus, in the aim of conciliating CAPs and traditional proofs, and due to the fact that a general translation between both seems to be impossible, González Huesca and Miranda-Perea proposed the concept of transitional proofs [3] which provides a translation methodology suitable for particular cases.
As a first step towards the construction of a transitional proof, we try to unmechanize the proof of cut elimination for GLS, but since Coq has received several updates, many of the libraries and tactics used by the authors have been deprecated. Due to this and other retrocompatibility issues, we were not able to review the whole proof script and consequently we were not able to complete the transitional proof.
Therefore, we opted to do a new proof, based on the sketches presented in [2], by proving all the lemmas and previous results that are enunciated without proof and including all the steps omitted by the authors in the main proof. The success of this approach shows that all the reasoning done by the proof assistant can in fact be translated to a traditional proof.
Another remarkable difference is that we proved cut elimination for PSGLS and concluded it for GLS as a corollary, unlike the original Coq proof where the authors worked in GLS and invoked PSGLS instances of the rules when needed.
This research is being supported by UNAM-DGAPA-PAPIIT grant IN101723.
Bibliography
- J. Brighton,Cut Elimination for GLS Using the Terminability of its Regress Process,Journal of Philosophical Logic,vol. 45 (2), pp.147–153.
- R. Goré, R. Ramanayake, I. Shillito,Cut-Elimination for Provability Logic by Terminating Proof-Search: Formalised and Deconstructed Using Coq,Automated Reasoning with Analytic Tableaux and Related Methods(Anupam Das and Sara Negri, editors),Springer International Publishing,Cham,2021,pp.299–313.
- F. E. Miranda-Perea, L. d. C. González Huesca,On the Conciliation of Traditional and Computer-Assisted Proofs,Philosophy of Computing(Bj{"o}rn Lundgren and Nancy Abigail Nu{ {n}}ez Hernández, editors),Springer International Publishing,Cham,2022,pp.73–112.