Derived datasets can be defined implicitly or explicitly. An implicit definition (of dataset O in terms of datasets I) is a logical specification involving two distinguished sets of relational symbols. One set of relations is for the "source data" I, and the other is for the "interface data" O. Such a specification 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 transformation (or "query" below) 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 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 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视图的NRC查询重写。