A LOWER BOUND FOR THE COMPLEXITY OF CRAIG'S INTERPOLANTS IN SENTENTIAL LOGIC

For any sentence α (in sentential logic) let dα be the delay complexity of the boolean function fα represented by α. We prove that for infinitely many d (and starting with some d<620) there exist valid implications α→β with dα, dβ≦d such that any Craig's interpolant x has its delay complexity dχ greater than d+(1/3)·log(d/2). This is the first (non-trivial) known lower bound on the complexity of Craig's interpolants in sentential logic, whose general study may well have an impact on the central problems of computation theory.