You are not logged in | Log in

not always) easy to spoi

Speaker(s)
Andrzej Tarlecki
Affiliation
MIMUW
Date
Nov. 25, 2022, 12:15 p.m.
Room
room 5820
Seminar
Seminar Semantics, Logic, Verification and its Applications

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 indicate simple situations where particular interpolation
properties turn out stable under any extension of the logical system. I
will then characterise situations where a particular interpolation
property may be spoiled by adding new abstract models, and discuss my
attempt to similarly characterise the (im)possibility of spoiling
interpolation properties by adding new abstract sentences. The results
are preliminary at best, good examples are missing, many questions
remain open (at least to me). Apologies in advance for incomplete and
potentially chaotic presentation.