Generalized Interpolation in First Order Logic

Article type: Research Article

Authors: Borzyszkowski, Tomasz

Affiliations: Institute of Mathematics, University of Gdańsk, Wita Stwosza 57, 80-952 Gdańsk, Poland. t.borzyszkowski@univ.gda.pl

Note: [] Address for correspondence: Institute of Mathematics, University of Gdańsk, Wita Stwosza 57, 80-952 Gdańsk, Poland

Abstract: We consider the Craig Interpolation Property for many sorted first-order logic. The Craig Interpolation Property explored in this paper is inspired by the institution independent generalization of this property presented in [21]. In [3] the author presents the interpolation result for the institution of many sorted first-order logic, with both morphisms in the pushout square being injective on sort names. The author also shows that the Craig Interpolation Property does not hold when both morphisms are certain morphisms which are noninjective on sort names. An open question in that paper was whether the interpolation property holds with only one morphism being injective on sort names. In this paper we give answer to this question. Following the overall structure of the classical proof presented in [7] for single sorted first-order logic, but with new technicalities concerning the many sorted case, we show that many sorted first-order logic has the interpolation property when just one (left or right) morphism is injective on sort names.

Keywords: Formal languages, Formal semantics, Specification languages, specifications, Interpolation property

Journal: Fundamenta Informaticae, vol. 66, no. 3, pp. 199-219, 2005