Towards Weak Stratification for Logics of Definitions

Technical Summary: Towards Weak Stratification for Logics of Definitions

Problem Statement
The logic of definitions is a family of logics used to encode and reason about judgments specified by inference rules, where atomic predicates are associated with logical formulas that may depend on the predicate itself. To resolve the apparent circularity inherent in such definitions, standard approaches impose a stratification condition, ensuring that a predicate does not appear negatively (to the left of an implication) in the body of its own definition. This condition effectively treats definitions as monotone fixed-point operators.

However, many useful specifications, particularly those involving logical relations for proving properties of programming languages, require definitions where the predicate appears negatively. In the logic $\mathcal{G}$, which underlies the Abella proof assistant, such definitions are disallowed. While Tiu [19] previously introduced a logic called $\mathcal{LD}$ that relaxes the stratification condition to weak stratification (allowing negative occurrences provided the level of the head is strictly greater than the level of the negative occurrence), $\mathcal{LD}$ was limited to a core fragment. It lacked support for the nabla quantifier ($\nabla$), essential for reasoning about names and freshness via nominal constants, and general inductive definitions beyond natural number induction. The challenge addressed in this work is to extend the logic of definitions to include weak stratification while maintaining consistency in the presence of $\nabla$ and general inductive definitions.

Methodology
The paper defines a new logic, $\mathcal{LD}\mu\nabla$, which extends Tiu's $\mathcal{LD}$ with nabla quantification and general inductive definitions. The methodology proceeds in three main stages:

1. Syntax and Semantics of $\mathcal{LD}\mu\nabla$:
   The logic is formulated as an extension of first-order sequent calculus with a set of definitions $\mathcal{D}$ and a set of inductive definitions $\mathcal{I}$.

   • Weak Stratification: A definition set $\mathcal{D}$ is weakly stratified if for every clause $H \triangleq_X B$ and grounding substitution $\rho$, $\text{lvl}(H\rho) \ge \text{lvl}(B\rho)$. Crucially, this allows negative occurrences of the defined predicate if the level of the head is strictly greater than the level of the negative occurrence.
   • Strict Stratification for Induction: The paper imposes a stricter condition on inductive definitions $\mathcal{I}$: they must be strictly stratified (the level of a ground atomic predicate must be independent of its arguments). This restriction is necessary to prevent inconsistency when combining induction with weak stratification.
   • Nabla Quantifier: The logic incorporates the $\nabla$ quantifier to handle nominal constants and freshness, distinguishing between generic and specific instances of names.

2. Ground Logic and Interpretation:
   To prove consistency, the authors construct a ground version of the logic, $\mathcal{LD}\mu\nabla_\infty$, where all formulas are ground (no eigenvariables).

   • Grounding Lemma: A key technical step is proving that any derivation in $\mathcal{LD}\mu\nabla$ can be interpreted as a derivation in $\mathcal{LD}\mu\nabla_\infty$ via a grounding substitution. This reduces the consistency problem of the full logic to the consistency of the ground logic.
   • Infinitary Rules: In $\mathcal{LD}\mu\nabla_\infty$, the standard $\forall R$ and $\exists L$ rules are replaced by infinitary rules that quantify over all ground terms, and the $\mu L$ rule for induction is similarly expanded to cover all ground instances.

3. Cut Elimination:
   The core of the consistency proof is the elimination of the cut rule (specifically, the multicut rule) in $\mathcal{LD}\mu\nabla_\infty$.

   • Reduction Relation: A reduction relation is defined on derivations, specifying how cuts can be pushed upwards or eliminated.
   • Reducibility: Following the Tait-Martin-Löf technique adapted by McDowell and Miller, the authors define a notion of reducibility (and normalizability) for derivations. They prove that every derivation in $\mathcal{LD}\mu\nabla_\infty$ is reducible.
   • Inductive Case Handling: A critical aspect of the proof is handling the interaction between weak stratification and induction. The authors show that while weak stratification is sufficient for general definitions, inductive definitions must remain strictly stratified. They provide a counterexample (Section 3.3) demonstrating that allowing weakly stratified inductive definitions leads to inconsistency.

Key Contributions

• Definition of $\mathcal{LD}\mu\nabla$: The paper formally defines a logic that combines weak stratification, nabla quantification, and general inductive definitions.
• Consistency Proof: The primary contribution is the proof that $\mathcal{LD}\mu\nabla$ is consistent. This is achieved by proving cut elimination for the ground logic $\mathcal{LD}\mu\nabla_\infty$ and establishing a grounding interpretation.
• Stratification Constraints: The work clarifies the boundary between permissible and impermissible definitions. It demonstrates that while weak stratification suffices for general definitions (enabling logical relations), inductive definitions require strict stratification to preserve consistency.
• Counterexample: The paper provides a specific counterexample showing that relaxing the stratification condition for inductive definitions leads to logical inconsistency, justifying the restriction imposed on $\mathcal{I}$.

Results

• Consistency: The logic $\mathcal{LD}\mu\nabla$ is proven consistent. Consequently, the logic $\mathcal{LD}\mu\nabla_\infty$ admits cut-free derivations for all provable sequents.
• Inversion Properties: The paper establishes meta-theoretic properties for $\mathcal{LD}\mu\nabla_\infty$, including the invertibility of various introduction rules (e.g., $\wedge R$, $\vee L$, $\nabla R$) and specific partial invertibility for $\vee R$, $\exists R$, and definition rules ($\Delta R$) when the context is empty. These properties are crucial for proof search procedures.
• Limitations: The cut elimination theorem is established only for the ground logic $\mathcal{LD}\mu\nabla_\infty$. The paper notes that extending this result to the full logic $\mathcal{LD}\mu\nabla$ (with eigenvariables) remains an open challenge.

Significance
The significance of this work lies in its potential to extend the capabilities of the Abella proof assistant. Abella is based on the logic $\mathcal{G}$, which currently restricts definitions to be strictly stratified. By justifying the inclusion of weakly stratified definitions, this research paves the way for Abella to natively support logical relations, a fundamental technique for proving semantic properties of programming languages (such as type safety and compiler correctness).

The paper positions this work as a foundational step toward a broader extension of $\mathcal{G}$. While the current result handles weak stratification with $\nabla$ and induction, the authors note that a full justification for Abella would require further extensions to include co-induction and nominal abstraction. The work also highlights the necessity of maintaining strict stratification for inductive definitions, a constraint that prevents the inconsistencies that would otherwise arise from mixing weak stratification with induction.