Formalizing infinite descent for complex inductive definitions in logic
An Infinitary and a Cyclic Sequent Calculus for Non-Monotone Inductive Definitions
Logic in Computer Science
Summary
Inductive definitions help computers and mathematicians define concepts step by step, like building blocks. However, many real-world ideas don’t always build up nicely in one direction—they are non-monotone. The authors extended existing math tools that prove things about these definitions, making them work even when the steps can go backward or be more complicated. Their work captures how to handle infinite reasoning and looping proof structures for these tricky cases, ensuring the logic is sound and complete. This helps develop better ways to formally prove properties about complex systems.
What this means in practice
- •For formal methods engineers: Develop verification tools that can handle complex non-monotone inductive definitions using infinite and cyclic proof techniques.
- •For automated reasoning developers: Create theorem provers supporting advanced proof structures for reasoning about programs and systems with non-monotone properties.
A theory result. No direct application yet.
Authors
Robbe Van den Eede
Abstract
Inductive definitions are an important form of knowledge in mathematics and computer science. Two common techniques to prove theorems about inductive definitions are the principle of mathematical induction and the principle of infinite descent. To formalize these principles, Brotherston and Simpson introduced the sequent calculus proof systems LKID, for mathematical induction, and LKIDω and CLKIDω , for infinite descent. LKIDω is an infinitary system, in which proofs are infinite trees, and CLKIDω a cyclic system, in which proofs are finite graphs. However, these calculi restrict to monotone definitions, while inductive definitions are generally non-monotone. The logic FO(ID) extends classical first-order logic with non-monotone inductive definitions. In earlier work, we provided a formalization of the principle of mathematical induction for non-monotone definitions by extending LKID to a sequent calculus SCFO(ID) for FO(ID). In this paper, we provide a formalization of the principle of infinite descent for non-monotone definitions by extending LKIDω and CLKIDω to sequent calculi SCFO(ID)-inf resp. SCFO(ID)-cyc for FO(ID). Furthermore, we extend several proof-theoretic results for LKIDω and CLKIDω to SCFO(ID)-inf and SCFO(ID)-cyc regarding soundness, completeness, cut-elimination and the relation with SCFO(ID).