A lower bound for the complexity of Craig's interpolants in sentential logic

For any sentenceα (in sentential logic) letd _α be the delay complexity of the boolean functionf _α represented byα. We prove that for infinitely manyd (and starting with somed<620) there exist valid implicationsα→β withd _α,d _β≦d such that any Craig's interpolantx has its delay complexityd _χ greater thand+(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.