On Interpolation in Existence Logics

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.

• Type: Conference
• Year: 2005
• Where: LPAR
• Authors: Matthias Baaz, Rosalie Iemhoff
• Keywords: Constant Domain Kripke, Existence Predicate, Intuitionistic Logic, LPAR 2005