The modelwise interpolation property of semantic logics

In this paper we introduce the modelwise interpolation property of a logic thatstates that whenever|=φ→ψholds for two formulasφandψ, then for everymodelMthere is an interpolant formulaχformulated in the intersection of thevocabularies ofφandψ, such thatM|=φ→χandM|=χ→ψ, that is, theinterpolant formula in Craig interpolation may vary from model to model. Wecompare the modelwise interpolation property with the standard Craig interpo-lation and with the local interpolation property by discussing examples, mostnotably the finite variable fragments of first order logic, and difference logic. Asan application we connect the modelwise interpolation property with the localBeth definability, and we prove that the modelwise interpolation property of analgebraizable logic can be characterized by a weak form of the superamalgama-tion property of the class of algebras corresponding to the models of the logic.