Direct elimination of additive-cuts in GL4ip: verified and extracted
Advances in Modal Logic 2022, 2022
Abstract
Recently, van der Giessen and Iemhoff proved cut-admissibility for the sequent calculus GL4ip for propositional intuitionistic provability logic. To do so, they were forced to use an indirection via the GL3ip calculus as GL4ip resists all standard direct cut- admissibility techniques. This indirection leaves little hope for the extraction of a comprehensible cut-elimination procedure for GL4ip from their work. We eliminate this indirection: we prove the admissibility of additive cut for GL4ip in a direct way by using a recently discovered proof technique which requires the existence of a terminating backward proof-search procedure in this calculus. By formalising our results in Coq we: (1) exhibit a successful direct proof technique for cut-admissibility for GL4ip ; (2) extract a syntactic cut-elimination procedure for GL4ip in Haskell ; and (3) use a local measure on sequents based on the shortlex order to show that the proof- search terminates. Once again, we see an unusual phenomenon in that terminating backward proof-search forms the basis for syntactic cut-elimination rather than for semantic cut-free completeness.
Recommended citation: Goré, Rajeev and Shillito, Ian. (2022). "Direct elimination of additive-cuts in GL4ip: verified and extracted" Advances in Modal Logic 2022.
Download Paper