Ground Stratified Inductive Definitions

Abstract

Logics of definitions extend first order intuitionistic logic with fixed-point definitions which associate formulas to atomic predicates. These associated formulas must be constrained for consistency. In the original formulation, predicate symbols were required to be ordered and only predicates lower in the order were allowed to appear negatively in the defining formula. This constraint renders ineligible definitions such as those of logical relations in which the predicate being defined must be allowed to appear negatively, albeit with smaller arguments. Tiu has formalized a weaker constraint called ground stratification that permits such definitions and has shown that it suffices for consistency. Definitions can also be given a least fixed-point interpretation via a special induction rule. We address the question of whether Tiu’s relaxation carries over to such a treatment. We propose a new induction rule for ground stratified inductive definitions that takes into account the fact that the definition of the predicate in question must itself be considered to be stratified by the complexity of its arguments to obtain a least fixed-point interpretation. We establish the consistency of the resulting logic and we illustrate its new capabilities via an example that encodes a strong normalizability proof for the simply typed λ-calculus in which the reducibility predicate is inductively defined by recursion on its arguments.