On Gabbay's Proof of the Craig Interpolation Theorem for Intuitionistic Predicate Logic
Michael Makkai · Notre Dame Journal of Formal Logic · 1995
Using the framework of categorical logic, this paper analyzes and streamlines Gabbay's semantical proof of the Craig interpolation theorem for intuitionistic predicate logic. In the process, an apparently new and interesting fact about the relation of coherent and intuitionistic logic is found.