Talk "On fragility of interpolation"

by Andrzej Tarlecki

Tue, 25 April 2023 at 11:50 am in Paris, France

Abstract: Many results in foundations of software specification and development depend on interpolation properties of the underlying logical systems. Craig interpolation has been known to hold for first-order logic at least since the late 50ties, with well studied links to other crucial properties, like Beth definability or Robinson consistency. It has been also shown, by various methods, for other logical systems. It is clear though that interpolation is a very delicate property, which may easily be lost under various extensions of the logical system. I have been trying to enhance my own understanding of interpolation by studying how this property may be spoiled when one adds new abstract models and/or sentences to the logical system. Perhaps surprisingly, when we work in the framework of an "entire" logical system formalised as an institution, this is not always possible. In this talk I will recall the notion of institution and the general concept of interpolation for logical systems formalised as institutions. I will give a complete characterisation of the simple situations where particular interpolation properties turn out to be stable under any extension of the logical system. I will also characterise situations where a particular interpolation property may be spoiled by adding new abstract models, and similarly characterise the possibility of spoiling interpolation properties by adding new abstract sentences.