Searcharxiv⌕ Search

arXiv subjects

Robbe Van den Eede

Publications and source records attributed to Robbe Van den Eede.

2 recordsLinked to original sources
arXiv2026

A Sequent Calculus for Non-Monotone Inductive Definitions

Inductive definitions constitute an important form of knowledge. The logic FO(ID) is an extension of classical first-order logic (FO) with a language construct to express non-monotone inductive definitions. Most existing proof systems for inductive definitions impose syntactic constraints on their definitions such as positivity and stratification, thereby excluding many useful and natural definitions. We obtain a sequent calculus SCFO(ID) for FO(ID) that supports general non-monotone inductive definitions by extending an existing sequent calculus LKID by Brotherston and Simpson, formalizing the principle of mathematical induction. To accommodate for non-monotone inductive definitions, we introduce an induction rule with an asymmetry between positive and negative occurrences of defined atoms. We establish several proof-theoretical properties of SCFO(ID) regarding its underlying first-order principles, soundness, completeness and cut-elimination.

cs.LO↗
arXiv2026

An Infinitary and a Cyclic Sequent Calculus for Non-Monotone Inductive Definitions

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).

cs.LO↗