On interpolation in existence logics

Abstract

In [2] Gentzen calculi for intuitionistic logic extended with an existence predicate were introduced. Such logics were first introduced by Dana Scott, who provided a proof system for it in Hilbert style. The logic seems particularly useful in settings where non constant domain Kripke models play a role. In this paper it is proved that these systems have interpolation and the Beth definability property. © Springer-Verlag Berlin Heidelberg 2005.