Summary: Derived datasets can be defined implicitly or explicitly. An implicit definition (of dataset \(O\) in terms of datasets \(\vec{I}\)) is a logical specification involving two distinguished sets of relational symbols. One set of relations is for the “source data” \(\vec{I}\), and the other is for the “interface data” \(O\). Such a specification is a valid definition of \(O\) in terms of \(\vec{I}\), if any two models of the specification agreeing on \(\vec{I}\) agree on \(O\). In contrast, an explicit definition is a transformation (or “query” below) that produces \(O\) from \(\vec{I}\). Variants of Beth’s theorem [E. W. Beth, Nederl. Akad. Wet., Proc., Ser. A 56 (Indag. Math. 15), 330–339 (1953; Zbl 0053.34402)] state that one can convert implicit definitions to explicit ones. Further, this conversion can be done effectively given a proof witnessing implicit definability in a suitable proof system.
We prove the analogous implicit-to-explicit result for nested relations: implicit definitions, given in the natural logic for nested relations, can be converted to explicit definitions in the nested relational calculus (NRC). We first provide a model-theoretic argument for this result, which makes some additional connections that may be of independent interest, between NRC queries, interpretations, a standard mechanism for defining structure-to-structure translation in logic, and between interpretations and implicit to definability “up to unique isomorphism”. The latter connection uses a variation of a result of Gaifman concerning “relatively categorical” theories. We also provide a a proof-theoretic result that provides an effective argument: from a proof witnessing implicit definability, we can efficiently produce an NRC definition. This will involve introducing the appropriate proof system for reasoning with nested sets, along with some auxiliary Beth-type results for this system. As a consequence, we can effectively extract rewritings of NRC queries in terms of NRC views, given a proof witnessing that the query is determined by the views.