The logic of definitions is a family of logics for encoding and reasoning about judgments, which are atomic predicates specified by inference rules. A definition associates an atomic predicate with a logical formula, which may itself depend on the predicate being defined. This leads to an apparent circularity which can be resolved by interpreting definitions as monotone fixed-point operators on terms, and which is enforced by imposing a stratification condition on definitions. In many instances, it is useful to consider definitions in which the predicate being defined appears negatively in the body of its definition. In the logic $\mathcal G$, underlying the Abella proof assistant, this is not allowed due to the stratification condition. One such application violating this condition is that of defining logical relations, which is a technique commonly used to prove properties about programming languages. Tiu has shown how to relax this stratification condition to allow for a broader body of definitions including that needed for logical relations. However, he only showed how to extend a core fragment of $\mathcal G$ with the weakened stratification condition, resulting in a logic he called $\mathrm{LD}$. In this work we show that the weakened stratification condition is also compatible with generic (nabla) quantification and general induction. The eventual aim of this work is to justify an extension of the Abella proof assistant allowing for such definitions.

翻译：定义逻辑是一类用于编码和推理判断（即由推理规则指定的原子谓词）的逻辑体系。定义将原子谓词与逻辑公式相关联，而该公式本身可能依赖于正在被定义的谓词。这导致了一种表面上的循环性，可通过将定义解释为项上的单调不动点算子来解决，并通过强加分层条件于定义来强制执行。在许多情况下，考虑被定义谓词在其定义体中负出现（negatively）的定义是有用的。在作为Abella证明助手基础的逻辑$\mathcal G$中，由于分层条件的存在，这是不允许的。违反此条件的一个典型应用是定义逻辑关系——这是一种常用于证明编程语言性质的技巧。Tiu已展示了如何放宽此分层条件，以允许包含逻辑关系所需定义在内的更广泛定义体。然而，他只展示了如何将弱分层条件扩展至$\mathcal G$的一个核心片段，从而得到他称之为$\mathrm{LD}$的逻辑。在本工作中，我们证明弱分层条件同样与泛型（nabla）量化和一般归纳法兼容。此项工作的最终目标是为扩展Abella证明助手以允许此类定义提供理论依据。