A New Machine-checked Proof of Strong Normalisation for Display Logic

AbstractWe use a deep embedding of the display calculus for relation algebras δRA in the logical framework Isabelle/HOL to formalise a new, machine-checked, proof of strong normalisation and cut-elimination for δRA which does not use measures on the size of derivations. Our formalisation generalises easily to other display calculi and can serve as a basis for formalised proofs of strong normalisation for the classical and intuitionistic versions of a vast range of substructural logics like the Lambek calculus, linear logic, relevant logic, BCK-logic, and their modal extensions. We believe this is the first full formalisation of a strong normalisation result for a sequent system using a logical framework