An institution-independent proof of the Beth definability theorem (Q995670)

The authors develop a very general concept of Beth definability within the framework of the so-called `institutions', a categorical abstract model theory which arose within algebraic specification theory, and within this context develop an abstract version of the classical first-order logic proof of the Beth definability theorem in dependence of Craig interpolation. The paper also studies the preservation of Craig interpolation and Beth definability along logic translations, understood as institution comorphisms. Unfortunately the paper seems to contain a series of technical errors (for example it is stated that any commutative square of signature morphisms in classical first-order logic has the interpolation property, which is wrong), but perhaps they can be repaired.