Derived datasets can be defined implicitly or explicitly. An implicit definition (of dataset O in terms of datasets I) is a logical specification involving the source data I and the interface data O. It is a valid definition of O in terms of I, if any two models of the specification agreeing on I agree on O. In contrast, an explicit definition is a query that produces O from I. Variants of Beth's theorem 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 mechanisms for defining structure-to-structure translation in logic, and between interpretations and implicit to definability "up to unique isomorphism". The latter connection makes use of a variation of a result of Gaifman concerning "relatively categorical" theories. We also provide 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.

翻译：派生数据集可通过隐式或显式方式定义。数据集O关于数据集I的隐式定义是一个涉及源数据I与接口数据O的逻辑规范。若该规范的所有模型在I上一致时必然在O上一致，则它构成O关于I的有效定义。与之相对，显式定义则是从I生成O的查询。贝特定理的变体表明，隐式定义可转换为显式定义；进一步地，给定在合适证明系统中验证隐式可定义性的证明，这种转换可有效实现。我们针对嵌套关系证明了类似的隐式到显式转换结果：在嵌套关系的自然逻辑中给出的隐式定义，可转换为嵌套关系演算中的显式定义。我们首先通过模型论论证该结果，其中建立的新关联可能具有独立研究价值——包括NRC查询与解释（逻辑中定义结构间翻译的标准机制）之间的关联，以及解释与"至唯一同构"隐式可定义性之间的关联。后者利用了盖夫曼关于"相对范畴性"理论的一个变体。我们还提供了基于证明论的有效性论证：从验证隐式可定义性的证明出发，可高效生成NRC定义。这需要引入适用于嵌套集合推理的恰当证明系统，并建立该系统的辅助贝特型结论。作为推论，给定验证查询由视图决定的证明，我们可以有效提取基于NRC视图的NRC查询重写。