Craig interpolation in displayable logics

Abstract

We give a general proof-theoretic method for establishing Craig interpolation for displayable logics, based upon an analysis of the individual proof rules of their display calculi. Using this uniform method, we establish interpolation for a spectrum of display calculi differing in their structural rules, including those for multiplicative linear logic, mul- tiplicative additive linear logic and ordinary classical logic. Our analysis at the level of proof rules also provides new insights into the reasons why interpolation fails, or seems likely to fail, in many substruc- tural logics. Specifically, we identify contraction as being particularly problematic for interpolation except in special circumstances.