Cut-Elimination for Provability Logic by Terminating Proof-Search: Formalised and Deconstructed Using Coq

Rajeev Gore, Revantha Ramanayake, Ian Shillito*

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review


Recently, Brighton gave another cut-admissibility proof for the standard set-based sequent calculus GLS for modal provability logic GL. One of the two induction measures that Brighton uses is novel: the maximum height of regress trees in an auxiliary calculus called RGL. Tautology elimination is established rather than direct cut-admissibility, and at some points the input derivation appears to be ignored in favour of a derivation obtained by backward proof-search. By formalising the GLS calculus and the proofs in Coq, we show that: (1) the use of the novel measure is problematic under the usual interpretation of the Gentzen comma as set union, and a multiset-based sequent calculus provides a more natural formulation; (2) the detour through tautology elimination is unnecessary; and (3) we can use the same induction argument without regress trees to obtain a direct proof of cut-admissibility that is faithful to the input derivation.
Original languageEnglish
Title of host publicationAutomated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2021.
EditorsAnupam Das, S. Negri
Place of PublicationCham
Number of pages14
ISBN (Electronic)978-3-030-86059-2
ISBN (Print)978-3-030-86058-5
Publication statusPublished - 2021
Event30th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods: TABLEAUX 2021: Automated Reasoning with Analytic Tableaux and Related Methods - Birmingham, United Kingdom
Duration: 6-Sep-20219-Sep-2021

Publication series

Name Lecture Notes in Computer Science
ISSN (Print)0302-9743
NameLecture Notes in Artificial Intelligence
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference30th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods
Country/TerritoryUnited Kingdom

Cite this