Speaker
Ricardo JaimesUrbán
Facultad de Ciencias, UNAM
Talks at this conference:
Friday, 14:25, J335 
Cut elimination for provability logic. An unmechanized proof. 
Authors: Ricardo JaimesUrbán and Favio E. MirandaPerea 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 MirandaPerea 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. Bibliography
