Craig Interpolation in Displayable Logics

James Brotherston

Craig interpolation of a logic is the property that, for any provable entailment F |- G between formulas, one can find an "interpolant" formula I such that F |- I and I |- G are both provable and I contains only those nonlogical constants that occur in both F and G. This property is well known to be of practical importance in computer science as well as theoretical importance in logic.

Display logic, due to Belnap, is a general Gentzen-style proof framework whose calculi are characterised by the availability of a "display-equivalence" relation, allowing any proof judgement to be rearranged so that a selected substructure appears alone on the appropriate side of the proof turnstile. Aside from this theoretical elegance, the main appeal of display calculi is their very general cut-elimination theorem which relies on checking eight simple conditions on the proof rules. It has been shown that very many substructural and modal logics can be presented as a cut-free display calculus.

However, in contrast to the situation for sequent calculi, it has been open since their inception 30 years ago whether cut-free display calculi can be used to prove an interpolation result. In this talk I address that question by showing how to obtain Craig interpolation for a substantial class of cut-free display calculi.

This talk is based on a TABLEAUX'11 paper of the same name with Rajeev Goré, ANU Canberra.