Ground Stratification for a Logic of Definitions with Induction

Basic Information

• Paper ID: 2510.12297
• Title: Ground Stratification for a Logic of Definitions with Induction
• Authors: Nathan Guermond, Gopalan Nadathur (University of Minnesota Twin-Cities)
• Classification: cs.LO cs.PL
• Conference: International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2025)
• Paper Link: https://arxiv.org/abs/2510.12297

Abstract

This paper investigates the stratification of definitions in the underlying logic of the Abella proof assistant. The Abella logic permits the interpretation of atomic predicates through fixed-point definitions and further supports inductive or coinductive reasoning. However, the strict stratification condition in the original logical formulation is overly restrictive for certain applications, such as semantic equivalence methods based on logical relations. Tiu has demonstrated that these restrictions can be relaxed through a weaker concept called "ground stratification," but his results are limited to a version of the logic that does not handle inductive definitions. This paper proves that these results can be extended to cover inductive definitions, while discovering that although ground stratification can be applied to arbitrary fixed-point definitions, weakening the stratification condition to inductive definitions leads to logical inconsistency.

Research Background and Motivation

Problem Background

1. Restrictiveness of Abella Logic: The logic G underlying the Abella proof assistant contains strict stratification conditions requiring that predicate constants cannot appear on the left side of top-level implication symbols in their defining formulas.
2. Practical Application Demands: The logical relations method is widely used in reasoning about programming language properties, with definitions typically indexed by types and assuming self-reference (albeit for structurally smaller types).
3. Insufficiency of Existing Solutions: Tiu's ground stratification approach applies only to logic versions that do not include inductive definitions.

Research Significance

• Theoretical Value: Extends the flexibility of logical definitions while preserving consistency.
• Practical Significance: Supports more programming language verification scenarios, particularly methods based on logical relations.
• Technical Advancement: Provides a foundation for constructing more flexible Abella logic.

Core Contributions

1. Extension of Ground Stratification Theory: Extends Tiu's ground stratification results to logic containing inductive definitions.
2. Identification of Inductive Definition Constraints: Proves that weakening stratification conditions to ground stratification form leads to logical inconsistency for inductive definitions.
3. Proposal of Hybrid Stratification Strategy: Inductive predicates use strict stratification while fixed-point predicates use ground stratification.
4. Consistency Proof: Proves consistency of logic LDμ through reduction to the base logic version.
5. Demonstration of Practical Applications: Shows how to encode reducibility predicates in strong normalization proofs.

Detailed Methodology

Definition of Logic LDμ

Syntactic Structure

• Foundation: Based on intuitionistic first-order logic over Church's simple type theory.
• Type System: Contains base types ι₁,...,ιₙ, function types α→β, and proposition type o.
• Terms: Well-typed terms in the simply-typed λ-calculus.
• Formulas: Terms of type o.

Definition Mechanisms

The logic supports two types of definition clauses:

1. Fixed-point Clauses: H ^∆= B, used for general fixed-point definitions.
2. Inductive Clauses: H ^μ= B, used for inductive definitions (minimal fixed points).

Stratification Conditions

Ground Stratification

A definition D is ground stratified if and only if there exists a level assignment to ground atomic formulas such that for each clause H ^∆= B ∈ D and each X-ground substitution ρ:

lvl(Hρ) ≥ lvl(Bρ)

The level function is defined as follows:

• lvl(⊥) := lvl(⊤) := 0
• lvl(A∧B) := lvl(A∨B) := max(lvl(A), lvl(B))
• lvl(A ⊃ B) := max(lvl(A)+1, lvl(B))
• lvl(∀x:α.C) := lvl(∃x:α.C) := sup{lvl(Ct/x∅) | t ∈ ground(α)}

Strict Stratification

Requires that the level assignment depends only on the predicate head, i.e., for any ground term sequences t₁ and t₂:

lvl(pt₁) = lvl(pt₂)

Hybrid Stratification Strategy

• Inductive Predicates: Must satisfy strict stratification conditions.
• Fixed-point Predicates: May use ground stratification conditions.

Inference Rules

Definition Rules

{range(θ);Γθ,B' ⊢ Cθ | defn(H^∆=B,A,θ,B'), H^∆=B ∈ D}
―――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――
                    Y;Γ,A ⊢ C                                    ∆L

                    Y;Γ ⊢ B'
                ――――――――――――――――――――――――  ∆R
                    Y;Γ ⊢ A

Inductive Rules

x;B Sx ⊢ Sx    X;Γ,St ⊢ C
―――――――――――――――――――――――――――――――――  μL
        X;Γ, pt ⊢ C

        X;Γ ⊢ B pt
        ――――――――――――――  μR  
         X;Γ ⊢ pt

Theoretical Analysis

Inconsistency Proof

Demonstrates that allowing inductive definitions to use ground stratification leads to logical inconsistency. Key example:

Defining the odd predicate:

odd (s X) ^μ= odd X ⊃ ⊥

This definition is legal under ground stratification but leads to contradiction:

1. One can prove for any term t: X;odd t ⊢ ev t and X;odd t ⊢ ev t ⊃ ⊥
2. Therefore X;odd t ⊢ ⊥ for all t
3. In particular, ·;odd z ⊢ ⊥ and ·;odd (s z) ⊢ ⊥ are both derivable
4. This ultimately derives ·;· ⊢ ⊥

Consistency Proof Strategy

Employs an indirect method to prove consistency of LDμ:

1. Base Logic LDμ∞: Defines an infinitary logic version where definitions handle only ground sequences.
2. Cut Elimination: Proves cut elimination property for LDμ∞.
3. Interpretation Mapping: Establishes an interpretation from LDμ to LDμ∞, reducing consistency.

Cut Elimination

Proved through the following steps:

1. Define cut reduction relations.
2. Introduce the concept of normalizable derivations.
3. Prove that reducibility implies normalizability.
4. Establish the reducibility lemma.

Key Unfolding Lemma:

Assume p x ^μ= B p x is an inductive definition in fixed-point form. For any derivation Ψ of ∆ ⊢ D p, where p does not appear in D and appears only positively in D p, there exists a derivation μ(Ψ,ΠS) of ∆ ⊢ D S.

Practical Applications

Strong Normalization Proof

Demonstrates how to encode reducibility predicates in Tait-style strong normalization proofs using ground stratification:

red unit T ^∆= sn T
red (arrow A B) T ^∆= ∀u:tm.(red A u ⊃ red B (app T u))

This definition cannot be strictly stratified (since red appears negatively in its body), but can be ground stratified because in the negatively occurring instance red A u, the type parameter A is a subterm of the head type parameter (arrow A B).

Logical Equivalence Relations

Supports encoding logical equivalence relations asserting that two functions behave identically on equivalent arguments, widely used in programming language semantics research.

Related Work

Relationship to Tiu's Work

• Foundation: Built upon Tiu's ground stratification theory.
• Extension: Extends results to include inductive definitions.
• Limitations: Discovers that inductive definitions require stronger conditions.

Comparison with μNJ

• μNJ: Natural reasoning calculus developed by Baelde and Nadathur, implementing flexible definitions through rewriting rules.
• This Work: Achieves flexibility through stratification conditions, avoiding modification of equational semantics.
• Complementarity: Both approaches have respective advantages and can inform each other.

Conclusions and Discussion

Main Conclusions

1. Theoretical Contribution: Successfully extends ground stratification to logic containing inductive definitions.
2. Practical Guidance: Identifies boundary conditions for safe use of ground stratification.
3. Technical Pathway: Provides intermediate steps for constructing more flexible Abella logic.

Limitations

1. Inductive Definition Constraints: Inductive definitions still require strict stratification.
2. Cut Elimination Proof: Cannot directly prove cut elimination for the complete logic.
3. Missing Features: Does not yet include coinduction, generic quantification, and nominal abstraction.

Future Directions

1. Extended Inductive Handling: Allow predicates in inductive clauses to appear in non-strictly negative positions.
2. Direct Cut Elimination Proof: Develop non-base calculi that can directly prove cut elimination.
3. Higher-order Quantification: Add higher-order quantification capabilities to enhance modularity.
4. Complete Feature Integration: Integrate coinduction, generic quantification, and other features.

In-Depth Evaluation

Strengths

1. Theoretical Rigor: Provides complete consistency proofs with meticulous technical treatment.
2. Practical Relevance: Addresses requirements of important application scenarios such as logical relations.
3. Balanced Design: Achieves appropriate balance between flexibility and safety.
4. Clear Presentation: Well-structured paper with accurate technical exposition.

Weaknesses

1. Application Scope: Restrictions on inductive definitions may impact certain advanced applications.
2. Proof Complexity: Indirect consistency proof increases theoretical complexity.
3. Implementation Gap: Integration with the actual Abella system remains to be addressed.

Impact

1. Theoretical Contribution: Provides important extension to logical definition theory.
2. Practical Value: Supports more formal verification scenarios.
3. Technical Influence: Provides reference for similar logic system design.

Applicable Scenarios

• Formal verification requiring flexible definition mechanisms.
• Program property proofs based on logical relations.
• Formal research on programming language semantics.
• Type systems and strong normalization proofs.

References

The paper cites 17 relevant references covering core areas including logical definitions, inductive reasoning, and cut elimination, particularly McDowell & Miller's (2000) foundational work and Tiu's (2012) ground stratification theory.