Formalised Cut Admissibility for Display Logic

Abstract. We use a deep embedding of the display calculus for relation algebras ffiRA in the logical framework Isabelle/HOL to formalise a machine-checked proof of cut-admissibility for ffiRA. Unlike other "implementations", we explicitly formalise the structural induction in Isabelle/HOL and believe this to be the first full formalisation of cutadmissibility in the presence of explicit structural rules. 1 Introduction Display Logic [1] is a generalised sequent framework for non-classical logics. Sinceit is not really a logic, we prefer the term display calculi and use it from now on. Display calculi extend Gentzen's language of sequents with extra, complex, n-ary structural connectives, in addition to Gentzen's sole structural connective,the "comma". Whereas Gentzen's comma is usually assumed to be associative, commutative and inherently poly-valent, no such implicit assumptions are madeabout th