Complexity of Craig’s Interpolation
Daniele Mundici · Fundamenta Informaticae · 1982
In this paper we investigate the length ‖ χ ‖ of the shortest interpolant of a valid implication φ → ψ in terms of ‖ φ ‖ + ‖ ψ ‖, both in sentential and in first-order logic. In the case of sentential logic, we give a precise exponential upper bound for ‖ χ ‖. We also show that the information about the growth of ‖ χ ‖ has some implications for computation theory. In the case of first-order logic we exhibit a very short valid implication whose interpolants are all impossibly long.