Mechanising a Proof of Craig's Interpolation Theorem for Intuitionistic Logic in NominalIsabelle

摘要

Craig's Interpolation Theorem is an important meta-theoretical result for several logics. Here we describe a formalisation of the result for first-order intuitionistic logic without function symbols or equality, with the intention of giving insight into how other such results in proof theory might be mechanically verified, notable cut-admissibility. We use the package Nominal Isabelle, which easily deals with the binding issues in the quantifier cases of the proof.