A generalization of Beth definability, proof-theoretically
Cecilia Pradic (Swansea University)
Beth definability states that whenever we have a FO formula A(R) that determines uniquely R over some base signature, then R is actually FO-definable. Furthermore this can be done proof-theoretically using Craig's interpolation theorem which gives a polytime algorithm extracting definitions from analytic proofs of functionality of A. This has applications in e.g. databases where this can be used to rewrite queries with respect to views.
I will discuss joint work with Michael Benedikt and Christoph Wernhard about another a stronger version of Beth definability generalization which is about defining maps between nested sets. I will also discuss a simple model-theoretic approach, which goes through a more general result that amounts essentially to Gaifman coordinisation. I will also explain how this coordinisation statement can be phrased effectively, although I do not know any reasonable complexity bound on the underlying algorithm. I will then discuss a (more challenging) proof-theoretic approach to this theorem, which has the benefit of extracting definitions in polynomial time from focused proofs.