The logic underlying the Abella proof assistant includes mechanisms for interpreting atomic predicates through fixed point definitions that can additionally be treated inductively or co-inductively. However, the original formulation of the logic includes a strict stratification condition on definitions that is too restrictive for some applications such as those that use a logical relations based approach to semantic equivalence. Tiu has shown how this restriction can be eased by utilizing a weaker notion referred to as ground stratification. Tiu's results were limited to a version of the logic that does not treat inductive definitions. We show here that they can be extended to cover such definitions. While our results are obtained by using techniques that have been previously deployed in related ways in this context, their use is sensitive to the particular way in which we generalize the logic. In particular, although ground stratification may be used with arbitrary fixed-point definitions, we show that weakening stratification to this form for inductive definitions leads to inconsistency. The particular generalization we describe accords well with the way logical relations are used in practice. Our results are also a intermediate step to building a more flexible form for definitions into the full logic underlying Abella, which additionally includes co-induction, generic quantification, and a mechanism referred to as nominal abstraction for analyzing occurrences of objects in terms that are governed by generic quantifiers.

翻译：Abella证明助手所基于的逻辑包含通过不动点定义来解释原子谓词的机制，这些定义可进一步被处理为归纳或余归纳定义。然而，该逻辑的原始表述对定义包含严格的分层条件，这对于某些应用（例如使用基于逻辑关系的语义等价方法）而言限制过强。Tiu已证明如何通过采用称为地基分层的较弱概念来放宽此限制。Tiu的结果仅限于该逻辑中不处理归纳定义的版本。我们在此证明这些结果可扩展至涵盖此类定义。虽然我们的结果是利用先前在此背景下以相关方式部署的技术获得的，但这些技术的使用对我们推广该逻辑的具体方式较为敏感。特别地，尽管地基分层可用于任意不动点定义，但我们证明将归纳定义的分层弱化为这种形式会导致不一致性。我们所描述的特定推广方式与实践中的逻辑关系使用方式高度契合。我们的结果也是向Abella所基于的完整逻辑（该逻辑还包含余归纳、泛化量词，以及一种称为名义抽象的机制，用于分析受泛化量词支配的项中对象出现的情况）构建更灵活定义形式的一个中间步骤。